Skip to content

Showing Replacement, Separation, and Pairing hold in WF #5027

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Oct 4, 2025
Merged

Showing Replacement, Separation, and Pairing hold in WF #5027

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9023c27
Showing Replace, Separation, and Pairing hold in WF
EricSchmidt-119 Sep 30, 2025
28369a0
Fix comment formatting
EricSchmidt-119 Sep 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions mmset.raw.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5607,6 +5607,7 @@
Introduction to Independence Proofs,</I> Elsevier Science B.V.,
Amsterdam (1980) [QA248.K75].
</LI>
<LI>
<A NAME="Kunen2"></A> [Kunen2] Kunen, Kenneth, <I>Set Theory,</I> revised
edition, College Publications, London (2013) [QA248 .K86 2013].
</LI>
Expand Down
251 changes: 239 additions & 12 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -745091,6 +745091,18 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
Mathbox for Eric Schmidt
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

${
$d x B $.
rspesbcd.1 $e |- ( ph -> A e. B ) $.
rspesbcd.2 $e |- ( ph -> [. A / x ]. ps ) $.
$( Restricted quantifier version of ~ spesbcd . (Contributed by Eric
Schmidt, 29-Sep-2025.) $)
rspesbcd $p |- ( ph -> E. x e. B ps ) $=
( cv wcel wa wex wrex wsbc sbcel1v sylibr sbcan sylanbrc spesbcd df-rex )
ACHEIZBJZCKBCELAUACDATCDMZBCDMUACDMADEIUBFCDENOGTBCDPQRBCESO $.
$}

$( The class of well-founded sets is transitive. (Contributed by Eric
Schmidt, 9-Sep-2025.) $)
trwf $p |- Tr U. ( R1 " On ) $=
Expand All @@ -745113,18 +745125,6 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
QRUTULVCJZVDUJUSVFUQUJUSULVCUJULUSVCDVBURTOPUARUTVDUBUCUIUDUEABCUFUGUH $.
$}

${
$d x y z $.
$( The class of well-founded sets models the axiom of Extensionality
~ ax-ext . Part of Corollaray II.2.5 of [Kunen2] p. 112. (Contributed
by Eric Schmidt, 11-Sep-2025.) $)
wfaxext $p |- A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On )
( A. z e. U. ( R1 " On ) ( z e. x <-> z e. y ) -> x = y ) $=
( cr1 con0 cima cuni wtr wel wb wral weq wi trwf traxext ax-mp ) DEFGZHCA
ICBIJCQKABLMBQKAQKNABCQOP $.
$( $j usage 'wfaxext' avoids 'ax-reg'; $)
$}

$( The Cartesian product of two well-founded sets is well-founded.
(Contributed by Eric Schmidt, 12-Sep-2025.) $)
xpwf $p |- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) ->
Expand All @@ -745150,6 +745150,233 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
UFMANOUBUDPQR $.
$( $j usage 'rnwf' avoids 'ax-reg'; $)

$( A relation is a well-founded set iff its domain and range are.
(Contributed by Eric Schmidt, 29-Sep-2025.) $)
relwf $p |- ( Rel R -> ( R e. U. ( R1 " On ) <->
( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) ) ) $=
( wrel cr1 con0 cima cuni wcel cdm crn dmwf rnwf jca cxp xpwf wss relssdmrn
wa sswf sylan2 expcom syl5 impbid2 ) ABZACDEFZGZAHZUDGZAIZUDGZQZUEUGUIAJAKL
UJUFUHMZUDGZUCUEUFUHNULUCUEUCULAUKOUEAPUKARSTUAUB $.
$( $j usage 'relwf' avoids 'ax-reg'; $)

${
modelaxreplem.1 $e |- ( ps -> x C_ M ) $.
modelaxreplem.2 $e |- ( ps -> A. f ( ( Fun f /\ dom f e. M /\ ran f C_ M )
-> ran f e. M ) ) $.
modelaxreplem.3 $e |- ( ps -> (/) e. M ) $.
modelaxreplem.4 $e |- ( ps -> x e. M ) $.

${
$d f M $. $d g x $. $d A g $. $d f g $. $d g ps $. $d g M $.
modelaxreplem1.5 $e |- A C_ x $.
$( Lemma for ~ modelaxrep . We show that ` M ` is closed under taking
subsets. (Contributed by Eric Schmidt, 29-Sep-2025.) $)
modelaxreplem1 $p |- ( ps -> A e. M ) $=
( vg wcel c0 wceq eleq1 syl5ibrcom cv wbr wss wa wne wfo wex csdm ssexi
vex 0sdom cdom cvv ssdomg mp2 fodomr mpan2 wfn crn df-fo wfun cdm df-fn
sylbir anim2d biimtrid sstrid sseq1 w3a df-3an wi wal funeq dmeq eleq1d
weq rneq sseq1d 3anbi123d imbi12d spvv syl biimtrrid syl2and wb exlimdv
adantl mpbidi syl5 pm2.61dne ) ACELZCMAWGCMNMELHCMEOPCMUAZBQZCKQZUBZKUC
ZAWGWHMCUDRZWLCCWIBUFZJUEUGWMCWIUHRZWLWIUILCWISWOWNJCWIUIUJUKWICKULUMUT
AWKWGKWKWJWIUNZWJUOZCNZTZAWGWICWJUPWSWQELZWGAAWPWJUQZWJURZELZTZWRWQESZW
TWPXAXBWINZTAXDWJWIUSAXFXCXAAXCXFWIELIXBWIEOPVAVBAXEWRCESACWIEJFVCWQCEV
DPXDXETXAXCXEVEZAWTXAXCXEVFADQZUQZXHURZELZXHUOZESZVEZXLELZVGZDVHXGWTVGZ
GXPXQDKDKVLZXNXGXOWTXRXIXAXKXCXMXEXHWJVIXRXJXBEXHWJVJVKXRXLWQEXHWJVMZVN
VOXRXLWQEXSVKVPVQVRVSVTWRWTWGWAWPWQCEOWCWDVBWBWEWF $.
$}

${
$d y z w M $. $d f F $. $d f M $. $d x y z w $.
modelaxreplem2.5 $e |- F/ w ps $.
modelaxreplem2.6 $e |- F/ z ps $.
modelaxreplem2.7 $e |- F/_ z F $.
modelaxreplem2.8 $e |- F = { <. w , z >. | ( w e. x /\
( z e. M /\ A. y ph ) ) } $.
modelaxreplem2.9 $e |- ( ps -> ( w e. M -> E. y e. M A. z e. M
( A. y ph -> z = y ) ) ) $.
$( Lemma for ~ modelaxrep . We define a class ` F ` and show that the
antecedent of Replacement implies that ` F ` is a function. We use
Replacement (in the form of ~ funex ) to show that ` F ` exists. Then
we show that, under our hypotheses, the range of ` F ` is a member of
` M ` . (Contributed by Eric Schmidt, 29-Sep-2025.) $)
modelaxreplem2 $p |- ( ps -> ran F e. M ) $=
( wcel cv wfun cdm crn wss wel wal wa wmo sseld weq wral wrex wrmo nfa1
rmo2i df-rmo sylib syl6 syld moanimv sylibr alrimi copab funeqi funopab
wi bitri dmeqi dmopabss eqsstri modelaxreplem1 an12 opabbii eqtri rneqi
rnopabss a1i cvv w3a funex wceq funeq dmeq eleq1d rneq sseq1d 3anbi123d
syl2anc imbi12d spcgv sylc mp3and ) BHUAZHUBZISZHUCZIUDZWPISZBFCUEZETIS
ZADUFZUGZUGZEUHZFUFZWMBXDFNBWSXBEUHZVFXDBWSFTZISZXFBCTZIXGJUIBXHXAEDUJV
FEIUKDIULZXFRXJXAEIUMXFXAEDIADUNUOXAEIUPUQURUSWSXBEUTVAVBWMXCFEVCZUAXEH
XKQVDXCFEVEVGVAZBCWNGIJKLMWNXKUBXIHXKQVHXBFEXIVIVJVKZWQBWPWTWSXAUGZUGZF
EVCZUCIHXPHXKXPQXCXOFEWSWTXAVLVMVNVOXNFEIVPVJVQBHVRSZGTZUAZXRUBZISZXRUC
ZIUDZVSZYBISZVFZGUFWMWOWQVSZWRVFZBWMWOXQXLXMIHVTWHKYFYHGHVRXRHWAZYDYGYE
WRYIXSWMYAWOYCWQXRHWBYIXTWNIXRHWCWDYIYBWPIXRHWEZWFWGYIYBWPIYJWDWIWJWKWL
$.

$( Lemma for ~ modelaxrep . We show that the consequent of Replacement
is satisfied with ` ran F ` as the value of ` y ` . (Contributed by
Eric Schmidt, 29-Sep-2025.) $)
modelaxreplem3 $p |- ( ps -> E. y e. M A. z e. M
( z e. y <-> E. w e. M ( w e. x /\ A. y ph ) ) ) $=
( wa wb wel wal wrex wral crn modelaxreplem2 wsbc cv wex sseld pm4.71rd
wcel anbi1d an12 anass anbi2i bitri bitrdi exbid copab cab rneqi rnopab
eqtri eqabri df-rex 19.42v bitr4i 3bitr4g baibd wnfc nfrn sbcralt mpan2
ralrimia nfel1 sbcbig sbcel2gv nfcv nfv nfa1 nfrexw sbcgf bibi12d bitrd
nfan ralbid syl mpbird rspesbcd ) BEDUAZFCUAZADUBZSZFIUCZTZEIUDZDHUEZIA
BCDEFGHIJKLMNOPQRUFZBWQDWRUGZEUHZWRULZWOTZEIUDZBXCEIOBXBXAIULZWOBWLXEWM
SZSZFUIZXEFUHZIULZWNSZSZFUIZXBXEWOSZBXGXLFNBXGXJWLSZXFSZXLBWLXOXFBWLXJB
CUHIXIJUJUKUMXPXEXOWMSZSXLXOXEWMUNXQXKXEXJWLWMUOUPUQURUSXHEWRWRXGFEUTZU
EXHEVAHXRQVBXGFEVCVDVEXNXEXKFUIZSXMWOXSXEWNFIVFUPXEXKFVGVHVIVJVOBWRIULZ
WTXDTWSXTWTWPDWRUGZEIUDZXDXTEWRVKWTYBTEHPVLZWPDEWRIIVMVNXTYAXCEIEWRIYCV
PXTYAWKDWRUGZWODWRUGZTXCWKWODWRIVQXTYDXBYEWODXAWRIVRWODWRIWNDFIDIVSWLWM
DWLDVTADWAWFWBWCWDWEWGWEWHWIWJ $.
$}

$}

${
$d x y z w g M $. $d f g M $. $d g ph $.
modelaxrep.1 $e |- ( ps -> Tr M ) $.
modelaxrep.2 $e |- ( ps -> A. f ( ( Fun f /\ dom f e. M /\ ran f C_ M )
-> ran f e. M ) ) $.
modelaxrep.3 $e |- ( ps -> (/) e. M ) $.
$( Conditions which guarantee that a class models the Axiom of Replacement
~ ax-rep . Similar to Lemma II.2.4(6) of [Kunen2] p. 111. The first
two hypotheses are those in Kunen. The reason for the third hypothesis
that our version of Replacement is different from Kunen's (which is
~ zfrep6 ). If we assumed Regularity, we could eliminate this extra
hypothesis, since under Regularity, the empty set is a member of every
non-empty transitive class.

Note that, to obtain the relativization of an instance of Replacement to
` M ` , the formula ` A. y ph ` would need to be replaced with
` A. y e. M ch ` , where ` ch ` is ` ph ` with all quantifiers
relativized to ` M ` . However, we can obtain this by using
` y e. M /\ ch ` for ` ph ` in this theorem, so it does establish that
all instances of Replacement hold in ` M ` . (Contributed by Eric
Schmidt, 29-Sep-2025.) $)
modelaxrep $p |- ( ps -> A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y
ph -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x
/\ A. y ph ) ) ) ) $=
( vg cv wcel wss wi wal wral wrex wa wtr wfun cdm crn w3a c0 weq wb funeq
wel dmeq eleq1d rneq sseq1d 3anbi123d imbi12d cbvalvw sylib trss ad5ant14
copab imp simp-4r simpllr simplr nfv nfan nfcv nfrexw nfralw nfopab2 eqid
nfra1 rsp adantl modelaxreplem3 ex ralrimiva syl21anc ) BHUAZLMZUBZWAUCZH
NZWAUDZHOZUEZWEHNZPZLQZUFHNZADQZEDUGPZEHRZDHSZFHRZEDUJFCUJZWLTFHSUHEHRDHS
ZPZCHRIBGMZUBZWTUCZHNZWTUDZHOZUEZXDHNZPZGQWJJXHWIGLGLUGZXFWGXGWHXIXAWBXCW
DXEWFWTWAUIXIXBWCHWTWAUKULXIXDWEHWTWAUMZUNUOXIXDWEHXJULUPUQURKVTWJTZWKTZW
SCHXLCMZHNZTZWPWRAXOWPTCDEFLWQEMHNWLTTZFEVAZHVTXNXMHOZWJWKWPVTXNXRHXMUSVB
UTVTWJWKXNWPVCXKWKXNWPVDXLXNWPVEXOWPFXOFVFWOFHVMVGXOWPEXOEVFWOEFHEHVHZWNE
DHXSWMEHVMVIVJVGXPFEVKXQVLWPFMHNWOPXOWOFHVNVOVPVQVRVS $.
$}

${
$d x y z $. $d ph y z $. $d y M $.

$( A class that is closed under subsets models the Axiom of Separation
~ ax-sep . Lemma II.2.4(3) of [Kunen2] p. 111.

Note that, to obtain the relativization of an instance of Separation to
` M ` , the formula ` ph ` would need to be replaced with its
relativization to ` M ` . However, this new formula is a valid
substitution for ` ph ` , so this theorem does establish that all
instances of Separation hold in ` M ` . (Contributed by Eric Schmidt,
29-Sep-2025.) $)
ssclaxsep $p |- ( A. z e. M ~P z C_ M -> A. z e. M E. y e. M A. x e. M
( x e. y <-> ( x e. z /\ ph ) ) ) $=
( cv cpw wss wel wa wb wral wrex wcel wex wal ax-sep wi biimp simpl alimi
syl6 velpw df-ss bitr2i sylib ssel syl5 alral eximdv df-rex sylibr ralimi
jca2 mpi ) DFZGZEHZBCIZBDIZAJZKZBELZCEMZDEURCFZENZVCJZCOZVDURVBBPZCOVHABC
DQURVIVGCURVIVFVCVIVEUQNZURVFVIUSUTRZBPZVJVBVKBVBUSVAUTUSVASUTATUBUAVJVEU
PHVLCUPUCBVEUPUDUEUFUQEVEUGUHVBBEUIUNUJUOVCCEUKULUM $.
$}

${
$d x z w $. $d y z w $. $d z M $.

$( A class that is closed under the pairing operation models the Axiom of
Pairing ~ ax-pr . Lemma II.2.4(4) of [Kunen2] p. 111. (Contributed by
Eric Schmidt, 29-Sep-2025.) $)
prclaxpr $p |- ( A. x e. M A. y e. M { x , y } e. M ->
A. x e. M A. y e. M E. z e. M A. w e. M
( ( w = x \/ w = y ) -> w e. z ) ) $=
( cv cpr wcel weq wo wel wi wral wrex vex elpr biimpri rgenw wceq eleq2
imbi2d ralbidv rspcev mpan2 2ralimi ) AFZBFZGZEHZDAIDBIJZDCKZLZDEMZCENZAB
EEUIUJDFZUHHZLZDEMZUNUQDEUPUJUOUFUGDOPQRUMURCUHECFZUHSZULUQDEUTUKUPUJUSUH
UOTUAUBUCUDUE $.
$}

${
wfax.1 $e |- W = U. ( R1 " On ) $.

${
$d x y z W $.

$( The class of well-founded sets models the axiom of Extensionality
~ ax-ext . Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed
by Eric Schmidt, 11-Sep-2025.) (Revised by Eric Schmidt,
29-Sep-2025.) $)
wfaxext $p |- A. x e. W A. y e. W
( A. z e. W ( z e. x <-> z e. y ) -> x = y ) $=
( wtr wel wb wral weq wi cr1 con0 cima cuni trwf wceq treq ax-mp mpbir
traxext ) DFZCAGCBGHCDIABJKBDIADIUBLMNOZFZPDUCQUBUDHEDUCRSTABCDUAS $.
$( $j usage 'wfaxext' avoids 'ax-reg'; $)
$}

${
$d x y z w W $. $d f W $.

$( The class of well-founded sets models the Axiom of Replacement
~ ax-rep . Actually, our statement is stronger, since it is an
instance of Replacement only when all quantifiers in ` A. y ph ` are
relativized to ` W ` . Essentially part of Corollary II.2.5 of
[Kunen2] p. 112, but note that our Replacement is different from
Kunen's. (Contributed by Eric Schmidt, 29-Sep-2025.) $)
wfaxrep $p |- A. x e. W ( A. w e. W E. y e. W A. z e. W ( A. y
ph -> z = y ) -> E. y e. W A. z e. W ( z e. y <-> E. w e. W ( w e. x
/\ A. y ph ) ) ) $=
( vf cr1 con0 wal wi wral wrex wel wtr mpbiri wcel wss c0 cima cuni weq
wceq wa wb trwf treq cv wfun cdm crn w3a vex rnex r1elss biimpri sseq2i
eleq2i 3imtr4i 3ad2ant3 ax-gen onwf 0elon sselii eleq2 modelaxrep ax-mp
a1i ) FIJUAUBZUDZACKZDCUCLDFMCFNEFMDCOEBOVLUEEFNUFDFMCFNLBFMGAVKBCDEHFV
KFPVJPUGFVJUHQHUIZUJZVMUKFRZVMULZFSZUMVPFRZLZHKVKVSHVQVNVRVOVPVJSZVPVJR
ZVQVRWAVTVPVMHUNUOUPUQFVJVPGURFVJVPGUSUTVAVBVIVKTFRTVJRJVJTVCVDVEFVJTVF
QVGVH $.
$( $j usage 'wfaxrep' avoids 'ax-reg'; $)
$}

${
$d x y z $. $d ph y z $. $d y W $.

$( The class of well-founded sets models the Axiom of Separation
~ ax-sep . Actually, our statement is stronger, since it is an
instance of Separation only when all quantifiers in ` ph ` are
relativized to ` W ` . Part of Corollary II.2.5 of [Kunen2] p. 112.
(Contributed by Eric Schmidt, 29-Sep-2025.) $)
wfaxsep $p |- A. z e. W E. y e. W A. x e. W
( x e. y <-> ( x e. z /\ ph ) ) $=
( cv cpw wss wel wa wb wral wrex ssclaxsep cr1 con0 cima cuni wcel pwwf
r1elssi sylbi eleq2i sseq2i 3imtr4i mprg ) DGZHZEIZBCJBDJAKLBEMCENDEMDE
ABCDEOUHPQRSZTZUIUKIZUHETUJULUIUKTUMUHUAUIUBUCEUKUHFUDEUKUIFUEUFUG $.
$( $j usage 'wfaxsep' avoids 'ax-reg'; $)
$}

${
$d x y z w $. $d y z W $.

$( The class of well-founded sets models the Axiom of Pairing ~ ax-pr .
Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric
Schmidt, 29-Sep-2025.) $)
wfaxpr $p |- A. x e. W A. y e. W E. z e. W A. w e. W
( ( w = x \/ w = y ) -> w e. z ) $=
( cv cpr wcel wral weq wo wel wi wrex cr1 con0 cima wa eleq2i cuni prwf
anbi12i 3imtr4i rgen2 prclaxpr ax-mp ) AGZBGZHZEIZBEJAEJDAKDBKLDCMNDEJC
EOBEJAEJUKABEEUHPQRUAZIZUIULIZSUJULIUHEIZUIEIZSUKUHUIUBUOUMUPUNEULUHFTE
ULUIFTUCEULUJFTUDUEABCDEUFUG $.
$( $j usage 'wfaxpr' avoids 'ax-reg'; $)
$}
$}

$( (End of Eric Schmidt's mathbox.) $)
$( End $[ set-mbox-es.mm $] $)

Expand Down