Reduce ax-un usage (#4465)

* Revise peano1 * Revise epweon * Prove sucexeloni * Shorten suceloni * Move df*o* and *oex theorems * Revise 1on * Revise 2on * Update sucexeloni desc
metamath · Dec 4, 2024 · 9927704 · 9927704
1 parent 49bf401
commit 9927704
Show file tree

Hide file tree

Showing 2 changed files with 117 additions and 40 deletions.
diff --git a/discouraged b/discouraged
@@ -14289,6 +14289,7 @@ New usage of "1ne0sr" is discouraged (1 uses).
 New usage of "1nq" is discouraged (9 uses).
 New usage of "1nqenq" is discouraged (1 uses).
 New usage of "1oexOLD" is discouraged (0 uses).
+New usage of "1onOLD" is discouraged (0 uses).
 New usage of "1p1e2apr1" is discouraged (0 uses).
 New usage of "1p2e3ALT" is discouraged (0 uses).
 New usage of "1pi" is discouraged (11 uses).
@@ -14329,6 +14330,7 @@ New usage of "2lplnmN" is discouraged (0 uses).
 New usage of "2moex" is discouraged (1 uses).
 New usage of "2moswap" is discouraged (1 uses).
 New usage of "2oexOLD" is discouraged (0 uses).
+New usage of "2onOLD" is discouraged (0 uses).
 New usage of "2pm13.193" is discouraged (3 uses).
 New usage of "2pm13.193VD" is discouraged (0 uses).
 New usage of "2pmaplubN" is discouraged (1 uses).
@@ -16550,6 +16552,7 @@ New usage of "enrer" is discouraged (8 uses).
 New usage of "enrex" is discouraged (9 uses).
 New usage of "ensn1OLD" is discouraged (0 uses).
 New usage of "ensucne0OLD" is discouraged (0 uses).
+New usage of "epweonOLD" is discouraged (0 uses).
 New usage of "eq0ALT" is discouraged (0 uses).
 New usage of "eq0OLDOLD" is discouraged (0 uses).
 New usage of "eq0rdvALT" is discouraged (0 uses).
@@ -18372,6 +18375,7 @@ New usage of "pclssidN" is discouraged (3 uses).
 New usage of "pclun2N" is discouraged (0 uses).
 New usage of "pclunN" is discouraged (1 uses).
 New usage of "pclvalN" is discouraged (6 uses).
+New usage of "peano1OLD" is discouraged (0 uses).
 New usage of "peano5OLD" is discouraged (0 uses).
 New usage of "permsetexOLD" is discouraged (1 uses).
 New usage of "perpdragALT" is discouraged (0 uses).
@@ -19246,6 +19250,7 @@ New usage of "strlem4" is discouraged (1 uses).
 New usage of "strlem5" is discouraged (1 uses).
 New usage of "strlem6" is discouraged (1 uses).
 New usage of "strndxid" is discouraged (2 uses).
+New usage of "suceloniOLD" is discouraged (0 uses).
 New usage of "sucidALT" is discouraged (0 uses).
 New usage of "sucidALTVD" is discouraged (0 uses).
 New usage of "sucidVD" is discouraged (0 uses).
@@ -19580,6 +19585,7 @@ Proof modification of "19.41rgVD" is discouraged (127 steps).
 Proof modification of "19.43OLD" is discouraged (72 steps).
 Proof modification of "1div0apr" is discouraged (77 steps).
 Proof modification of "1oexOLD" is discouraged (4 steps).
+Proof modification of "1onOLD" is discouraged (9 steps).
 Proof modification of "1p1e2apr1" is discouraged (7 steps).
 Proof modification of "1p2e3ALT" is discouraged (7 steps).
 Proof modification of "1strbasOLD" is discouraged (22 steps).
@@ -19591,6 +19597,7 @@ Proof modification of "2falsedOLD" is discouraged (14 steps).
 Proof modification of "2irrexpqALT" is discouraged (90 steps).
 Proof modification of "2logb9irrALT" is discouraged (141 steps).
 Proof modification of "2oexOLD" is discouraged (9 steps).
+Proof modification of "2onOLD" is discouraged (9 steps).
 Proof modification of "2pm13.193" is discouraged (91 steps).
 Proof modification of "2pm13.193VD" is discouraged (223 steps).
 Proof modification of "2ralorOLD" is discouraged (109 steps).
@@ -20354,6 +20361,7 @@ Proof modification of "enfiALT" is discouraged (42 steps).
 Proof modification of "enfiiOLD" is discouraged (14 steps).
 Proof modification of "ensn1OLD" is discouraged (47 steps).
 Proof modification of "ensucne0OLD" is discouraged (82 steps).
+Proof modification of "epweonOLD" is discouraged (86 steps).
 Proof modification of "eq0ALT" is discouraged (31 steps).
 Proof modification of "eq0OLDOLD" is discouraged (6 steps).
 Proof modification of "eq0rdvALT" is discouraged (25 steps).
@@ -20966,6 +20974,7 @@ Proof modification of "ordelordALT" is discouraged (128 steps).
 Proof modification of "ordelordALTVD" is discouraged (202 steps).
 Proof modification of "orim12dALT" is discouraged (34 steps).
 Proof modification of "p0exALT" is discouraged (2 steps).
+Proof modification of "peano1OLD" is discouraged (9 steps).
 Proof modification of "peano5OLD" is discouraged (304 steps).
 Proof modification of "perfectALTV" is discouraged (528 steps).
 Proof modification of "permsetexOLD" is discouraged (42 steps).
@@ -21239,6 +21248,7 @@ Proof modification of "ssralv2VD" is discouraged (147 steps).
 Proof modification of "sstrALT2" is discouraged (81 steps).
 Proof modification of "sstrALT2VD" is discouraged (84 steps).
 Proof modification of "stdpc5t" is discouraged (23 steps).
+Proof modification of "suceloniOLD" is discouraged (160 steps).
 Proof modification of "sucidALT" is discouraged (28 steps).
 Proof modification of "sucidALTVD" is discouraged (28 steps).
 Proof modification of "sucidVD" is discouraged (24 steps).

diff --git a/set.mm b/set.mm
@@ -74361,16 +74361,33 @@ result of an operator (deduction version).  (Contributed by Paul
 $)
 
   ${
-    $d x y $.
+    $d x y z $.
     $( The membership relation well-orders the class of ordinal numbers.  This
        proof does not require the axiom of regularity.  Proposition 4.8(g) of
-       [Mendelson] p. 244.  (Contributed by NM, 1-Nov-2003.) $)
+       [Mendelson] p. 244.  (Contributed by NM, 1-Nov-2003.)  Avoid ~ ax-un .
+       (Revised by BTernaryTau, 30-Nov-2024.) $)
     epweon $p |- _E We On $=
+      ( vx vy vz con0 cep wwe wfr wor cv wbr w3o wral wn wa wcel wel word eloni
+      epel mpbir2an onfr wpo weq df-po ordirr syl sylnibr ontr1 anbi12i 3imtr4g
+      anim12i ralrimiva ralrimivw mprgbir ordtri3or biid 3orbi123i sylibr rgen2
+      wi syl2an df-so df-we ) DEFDEGDEHZUAVDDEUBZAIZBIZEJZABUCZVGVFEJZKZBDLADLV
+      EVFVFEJZMZVHVGCIZEJZNZVFVNEJZUTZNZCDLZBDLADABCDEUDVFDOZVTBDWAVSCDWAVMVNDO
+      ZVRWAAAPZVLWAVFQZWCMVFRZVFUEUFAVFSUGWBABPZBCPZNACPVPVQVFVGVNUHVHWFVOWGBVF
+      SZCVGSUICVFSUJUKULUMUNVKABDDWAWDVGQZVKVGDOWEVGRWDWINWFVIBAPZKVKVFVGUOVHWF
+      VIVIVJWJWHVIUPAVGSUQURVAUSABDEVBTDEVCT $.
+    $( $j usage 'epweon' avoids 'ax-un' 'ax-reg'; $)
+  $}
+
+  ${
+    $d x y $.
+    $( Obsolete version of ~ epweon as of 30-Nov-2024.  (Contributed by NM,
+       1-Nov-2003.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    epweonOLD $p |- _E We On $=
       ( vx vy con0 cep wwe wfr cv wbr weq w3o wral onfr wcel eloni wa ordtri3or
       word wel epel biid 3orbi123i sylibr syl2an rgen2 dfwe2 mpbir2an ) CDECDFA
       GZBGZDHZABIZUHUGDHZJZBCKACKLULABCCUGCMUGQZUHQZULUHCMUGNUHNUMUNOABRZUJBARZ
       JULUGUHPUIUOUJUJUKUPBUGSUJTAUHSUAUBUCUDABCDUEUF $.
-    $( $j usage 'epweon' avoids 'ax-reg'; $)
   $}
 
   $( The class of all ordinal numbers is ordinal.  Proposition 7.12 of
@@ -74650,11 +74667,35 @@ be a set (so instead it is a proper class).  Here we prove the denial of
       DVGUJUKULUMUNUOVBVFVISZVAVBVDTJVRAUPBVDVETUQUTURUS $.
   $}
 
+  ${
+    $d A x $.
+    $( If the successor of an ordinal number exists, it is an ordinal number.
+       This variation of ~ suceloni does not require ~ ax-un .  (Contributed by
+       BTernaryTau, 30-Nov-2024.) $)
+    sucexeloni $p |- ( ( A e. On /\ suc A e. V ) -> suc A e. On ) $=
+      ( vx con0 wcel csuc wa word wtr wss cv wral csn wo onelss wi velsn eqimss
+      wceq sylbi a1i orim12d cun df-suc eleq2i elun oridm 3imtr3g sssucid sstr2
+      bitr2i syl6mpi ralrimiv dftr3 sylibr onss snssi unssd eqsstrid ordon 3exp
+      trssord mpii sylc adantr wb elong adantl mpbird ) ADEZAFZBEZGVKDEZVKHZVJV
+      NVLVJVKIZVKDJZVNVJCKZVKJZCVKLVOVJVRCVKVJVQVKEZVQAJZAVKJVRVJVQAEZVQAMZEZNZ
+      VTVTNVSVTVJWAVTWCVTAVQOWCVTPVJWCVQASVTCAQVQARTUAUBVSVQAWBUCZEWDVKWEVQAUDZ
+      UEVQAWBUFUKVTUGUHAUIVQAVKUJULUMCVKUNUOVJVKWEDWFVJAWBDAUPADUQURUSVOVPDHZVN
+      UTVOVPWGVNVKDVBVAVCVDVEVLVMVNVFVJVKBVGVHVI $.
+    $( $j usage 'sucexeloni' avoids 'ax-un'; $)
+  $}
+
+  $( The successor of an ordinal number is an ordinal number.  Proposition 7.24
+     of [TakeutiZaring] p. 41.  (Contributed by NM, 6-Jun-1994.)  (Proof
+     shortened by BTernaryTau, 30-Nov-2024.) $)
+  suceloni $p |- ( A e. On -> suc A e. On ) $=
+    ( con0 wcel csuc cvv sucexg sucexeloni mpdan ) ABCADZECIBCABFAEGH $.
+
   ${
     $d x A $.
-    $( The successor of an ordinal number is an ordinal number.  Proposition
-       7.24 of [TakeutiZaring] p. 41.  (Contributed by NM, 6-Jun-1994.) $)
-    suceloni $p |- ( A e. On -> suc A e. On ) $=
+    $( Obsolete version of ~ suceloni as of 30-Nov-2024.  (Contributed by NM,
+       6-Jun-1994.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    suceloniOLD $p |- ( A e. On -> suc A e. On ) $=
       ( vx con0 wcel csuc word wtr wss cv wral csn wo onelss velsn eqimss sylbi
       wi wceq a1i cvv orim12d cun df-suc eleq2i elun bitr2i oridm 3imtr3g sstr2
       sssucid syl6mpi ralrimiv dftr3 sylibr onss snssi unssd ordon trssord 3exp
@@ -75566,10 +75607,18 @@ also define a subset of the complex numbers ( ~ df-nn ) with analogous
      Proposition 7.30(1) of [TakeutiZaring] p. 42.  Note:  Unlike most
      textbooks, our proofs of ~ peano1 through ~ peano5 do not use the Axiom of
      Infinity.  Unlike Takeuti and Zaring, they also do not use the Axiom of
-     Regularity.  (Contributed by NM, 15-May-1994.) $)
+     Regularity.  (Contributed by NM, 15-May-1994.)  Avoid ~ ax-un .  (Revised
+     by BTernaryTau, 29-Nov-2024.) $)
   peano1 $p |- (/) e. _om $=
+    ( vx c0 com wcel con0 cv wlim wi wal 0elon 0ellim ax-gen elom mpbir2an ) BC
+    DBEDAFZGBODHZAIJPAOKLABMN $.
+  $( $j usage 'peano1' avoids 'ax-un' 'ax-inf' 'ax-inf2' 'ax-reg'; $)
+
+  $( Obsolete version of ~ peano1 as of 29-Nov-2024.  (Contributed by NM,
+     15-May-1994.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  peano1OLD $p |- (/) e. _om $=
     ( com wlim c0 wcel limom 0ellim ax-mp ) ABCADEAFG $.
-  $( $j usage 'peano1' avoids 'ax-inf' 'ax-inf2' 'ax-reg'; $)
 
   $( The successor of any natural number is a natural number.  One of Peano's
      five postulates for arithmetic.  Proposition 7.30(2) of [TakeutiZaring]
@@ -83548,13 +83597,61 @@ other applications (for instance in intuitionistic set theory) need it.
                  ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) ) $.
   $}
 
-  $( Ordinal 1 is an ordinal number.  (Contributed by NM, 29-Oct-1995.) $)
+  $( Expanded value of the ordinal number 1.  (Contributed by NM,
+     4-Nov-2002.) $)
+  df1o2 $p |- 1o = { (/) } $=
+    ( c1o c0 csuc csn df-1o suc0 eqtri ) ABCBDEFG $.
+
+  $( Expanded value of the ordinal number 2.  (Contributed by Mario Carneiro,
+     14-Aug-2015.) $)
+  df2o3 $p |- 2o = { (/) , 1o } $=
+    ( c2o c1o csuc csn cun c0 cpr df-2o df-suc df1o2 uneq1i df-pr eqtr4i 3eqtri
+    ) ABCBBDZEZFBGZHBIPFDZOEQBROJKFBLMN $.
+
+  $( Expanded value of the ordinal number 2.  (Contributed by NM,
+     29-Jan-2004.) $)
+  df2o2 $p |- 2o = { (/) , { (/) } } $=
+    ( c2o c0 c1o cpr csn df2o3 df1o2 preq2i eqtri ) ABCDBBEZDFCJBGHI $.
+
+  $( Ordinal 1 is a set.  (Contributed by BJ, 6-Apr-2019.)  (Proof shortened by
+     AV, 1-Jul-2022.)  Remove dependency on ~ ax-10 , ~ ax-11 , ~ ax-12 ,
+     ~ ax-un .  (Revised by Zhi Wang, 19-Sep-2024.) $)
+  1oex $p |- 1o e. _V $=
+    ( c1o c0 csn cvv df1o2 snex eqeltri ) ABCDEBFG $.
+  $( $j usage '1oex' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-un'; $)
+
+  $( ` 2o ` is a set.  (Contributed by BJ, 6-Apr-2019.)  Remove dependency on
+     ~ ax-10 , ~ ax-11 , ~ ax-12 , ~ ax-un .  (Proof shortened by Zhi Wang,
+     19-Sep-2024.) $)
+  2oex $p |- 2o e. _V $=
+    ( c2o c0 c1o cpr cvv df2o3 prex eqeltri ) ABCDEFBCGH $.
+  $( $j usage '2oex' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-un'; $)
+
+  $( Ordinal 1 is an ordinal number.  (Contributed by NM, 29-Oct-1995.)  Avoid
+     ~ ax-un .  (Revised by BTernaryTau, 30-Nov-2024.) $)
   1on $p |- 1o e. On $=
+    ( c1o csuc con0 df-1o wcel cvv 0elon 1oex eqeltrri sucexeloni mp2an eqeltri
+    c0 ) AMBZCDMCENFENCEGANFDHIMFJKL $.
+  $( $j usage '1on' avoids 'ax-un'; $)
+
+  $( Obsolete version of ~ 1on as of 30-Nov-2024.  (Contributed by NM,
+     29-Oct-1995.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  1onOLD $p |- 1o e. On $=
     ( c1o c0 csuc con0 df-1o 0elon onsuci eqeltri ) ABCDEBFGH $.
 
   $( Ordinal 2 is an ordinal number.  (Contributed by NM, 18-Feb-2004.)  (Proof
-     shortened by Andrew Salmon, 12-Aug-2011.) $)
+     shortened by Andrew Salmon, 12-Aug-2011.)  Avoid ~ ax-un .  (Revised by
+     BTernaryTau, 30-Nov-2024.) $)
   2on $p |- 2o e. On $=
+    ( c2o c1o csuc con0 df-2o wcel cvv 2oex eqeltrri sucexeloni mp2an eqeltri
+    1on ) ABCZDEBDFNGFNDFMANGEHIBGJKL $.
+  $( $j usage '2on' avoids 'ax-un'; $)
+
+  $( Obsolete version of ~ 2on as of 30-Nov-2024.  (Contributed by NM,
+     18-Feb-2004.)  (Proof shortened by Andrew Salmon, 12-Aug-2011.)
+     (Proof modification is discouraged.)  (New usage is discouraged.) $)
+  2onOLD $p |- 2o e. On $=
     ( c2o c1o csuc con0 df-2o 1on onsuci eqeltri ) ABCDEBFGH $.
 
   $( Ordinal two is not zero.  (Contributed by Scott Fenton, 17-Jun-2011.) $)
@@ -83571,42 +83668,12 @@ other applications (for instance in intuitionistic set theory) need it.
   4on $p |- 4o e. On $=
     ( c4o c3o csuc con0 df-4o 3on onsuci eqeltri ) ABCDEBFGH $.
 
-  $( Expanded value of the ordinal number 1.  (Contributed by NM,
-     4-Nov-2002.) $)
-  df1o2 $p |- 1o = { (/) } $=
-    ( c1o c0 csuc csn df-1o suc0 eqtri ) ABCBDEFG $.
-
-  $( Ordinal 1 is a set.  (Contributed by BJ, 6-Apr-2019.)  (Proof shortened by
-     AV, 1-Jul-2022.)  Remove dependency on ~ ax-10 , ~ ax-11 , ~ ax-12 ,
-     ~ ax-un .  (Revised by Zhi Wang, 19-Sep-2024.) $)
-  1oex $p |- 1o e. _V $=
-    ( c1o c0 csn cvv df1o2 snex eqeltri ) ABCDEBFG $.
-    $( $j usage '1oex' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-un'; $)
-
   $( Obsolete version of ~ 1oex as of 19-Sep-2024.  (Contributed by BJ,
      6-Apr-2019.)  (Proof shortened by AV, 1-Jul-2022.)
      (Proof modification is discouraged.)  (New usage is discouraged.) $)
   1oexOLD $p |- 1o e. _V $=
     ( c1o con0 1on elexi ) ABCD $.
 
-  $( Expanded value of the ordinal number 2.  (Contributed by Mario Carneiro,
-     14-Aug-2015.) $)
-  df2o3 $p |- 2o = { (/) , 1o } $=
-    ( c2o c1o csuc csn cun c0 cpr df-2o df-suc df1o2 uneq1i df-pr eqtr4i 3eqtri
-    ) ABCBBDZEZFBGZHBIPFDZOEQBROJKFBLMN $.
-
-  $( Expanded value of the ordinal number 2.  (Contributed by NM,
-     29-Jan-2004.) $)
-  df2o2 $p |- 2o = { (/) , { (/) } } $=
-    ( c2o c0 c1o cpr csn df2o3 df1o2 preq2i eqtri ) ABCDBBEZDFCJBGHI $.
-
-  $( ` 2o ` is a set.  (Contributed by BJ, 6-Apr-2019.)  Remove dependency on
-     ~ ax-10 , ~ ax-11 , ~ ax-12 , ~ ax-un .  (Proof shortened by Zhi Wang,
-     19-Sep-2024.) $)
-  2oex $p |- 2o e. _V $=
-    ( c2o c0 c1o cpr cvv df2o3 prex eqeltri ) ABCDEFBCGH $.
-    $( $j usage '2oex' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-un'; $)
-
   $( Obsolete version of ~ 2oex as of 19-Sep-2024.  (Contributed by BJ,
      6-Apr-2019.)  (Proof modification is discouraged.)
      (New usage is discouraged.) $)