diff --git a/mmset.raw.html b/mmset.raw.html
index ab4a5fa200..cae675976c 100644
--- a/mmset.raw.html
+++ b/mmset.raw.html
@@ -5607,6 +5607,7 @@
Introduction to Independence Proofs, Elsevier Science B.V.,
Amsterdam (1980) [QA248.K75].
+
[Kunen2] Kunen, Kenneth, Set Theory, revised
edition, College Publications, London (2013) [QA248 .K86 2013].
diff --git a/set.mm b/set.mm
index 2c57dab044..f3176465e3 100644
--- a/set.mm
+++ b/set.mm
@@ -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 ) $=
@@ -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 ) ) ->
@@ -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 $] $)