Add mathbox for Eric Schmidt (#5011)

* Add mathbox for Eric Schmidt with some initial theorems

* Add bibliographic references, use M for 'model' in traxext

* Minor formatting change

* Fix markup mistakes

* Add $j statements for avoiding ax-ref

* Fix typo

* Remove duplicate lines

Author: EricSchmidt-119

mmset.raw.html

@@ -5607,6 +5607,9 @@
 Introduction to Independence Proofs,</I> Elsevier Science B.V.,
 Amsterdam (1980) [QA248.K75].
 </LI>
+<A NAME="Kunen2"></A> [Kunen2] Kunen, Kenneth, <I>Set Theory,</I> revised
+edition, College Publications, London (2013) [QA248 .K86 2013].
+</LI>
 <LI>
 <A NAME="KuratowskiMostowski"></A> [KuratowskiMostowski] Kuratowski, K.
 and A. Mostowski, <I>Set Theory: with an Introduction to

set.mm

@@ -744672,6 +744672,76 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
 $( End $[ set-mbox-as.mm $] $)
 
 
+$( Begin $[ set-mbox-es.mm $] $)
+$( Skip $[ set-main.mm $] $)
+$(
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+  Mathbox for Eric Schmidt
+#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
+$)
+  $( The class of well-founded sets is transitive.  (Contributed by Eric
+     Schmidt, 9-Sep-2025.) $)
+  trwf $p |- Tr U. ( R1 " On ) $=
+    ( vx cr1 con0 cima cuni wtr cv wss wral r1elssi rgen dftr3 mpbir ) BCDEZFAG
+    ZNHZANIPANOJKANLM $.
+    $( $j usage 'trwf' avoids 'ax-reg'; $)
+
+  ${
+    $d x y z M $.
+
+    $( A transitive class models the Axiom of Extensionality ~ ax-ext .  Lemma
+       II.2.4(1) of [Kunen2] p. 111.  (Contributed by Eric Schmidt,
+       11-Sep-2025.) $)
+    traxext $p |- ( Tr M -> A. x e. M A. y e. M
+        ( A. z e. M ( z e. x <-> z e. y ) -> x = y ) ) $=
+      ( wtr wel wb wral weq wi cv wcel wa df-ral ancomsd expdimp adantrr adantr
+      wal trel adantrl simpr pm5.21ndd alimdv biimtrid ax-ext syl6 ralrimivva
+      ex ) DEZCAFZCBFZGZCDHZABIZJABDDUJAKZDLZBKZDLZMMZUNUMCSZUOUNCKZDLZUMJZCSUT
+      VAUMCDNUTVDUMCUTVDUMUTVDMVCUKULUTUKVCJZVDUJUQVEUSUJUQUKVCUJUKUQVCDVBUPTOP
+      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 ) ) ->
+      ( A X. B ) e. U. ( R1 " On ) ) $=
+    ( cr1 con0 cima cuni wcel wa cun cpw cxp unwf pwwf 3bitri xpsspw sswf mpan2
+    wss sylbi ) ACDEFZGBTGHZABIZJZJZTGZABKZTGZUAUBTGUCTGUEABLUBMUCMNUEUFUDRUGAB
+    OUDUFPQS $.
+  $( $j usage 'xpwf' avoids 'ax-reg'; $)
+
+  $( The domain of a well-founded set is well-founded.  (Contributed by Eric
+     Schmidt, 12-Sep-2025.) $)
+  dmwf $p |- ( A e. U. ( R1 " On ) -> dom A e. U. ( R1 " On ) ) $=
+    ( cr1 con0 cima cuni wcel cdm uniwf bitri wss crn cun ssun1 dmrnssfld sstri
+    sswf mpan2 sylbi ) ABCDEZFZAEZEZSFZAGZSFZTUASFUCAHUAHIUCUDUBJUEUDUDAKZLUBUD
+    UFMANOUBUDPQR $.
+  $( $j usage 'dmwf' avoids 'ax-reg'; $)
+
+  $( The range of a well-founded set is well-founded.  (Contributed by Eric
+     Schmidt, 12-Sep-2025.) $)
+  rnwf $p |- ( A e. U. ( R1 " On ) -> ran A e. U. ( R1 " On ) ) $=
+    ( cr1 con0 cima cuni wcel crn uniwf bitri wss cdm cun ssun2 dmrnssfld sstri
+    sswf mpan2 sylbi ) ABCDEZFZAEZEZSFZAGZSFZTUASFUCAHUAHIUCUDUBJUEUDAKZUDLUBUD
+    UFMANOUBUDPQR $.
+  $( $j usage 'rnwf' avoids 'ax-reg'; $)
+
+$( (End of Eric Schmidt's mathbox.) $)
+$( End $[ set-mbox-es.mm $] $)
+
+
 $( Begin $[ set-mbox-gs.mm $] $)
 $( Skip $[ set-main.mm $] $)
 $(