Reduce ax-un usage (#4466)

* Prove ord1eln01

* Prove ord2eln012

* Prove nlim1

* Prove nlim2

* Prove 1ellim

* Prove 2ellim

* Revise 1onn

* Revise 2onn

* Prove f1cdmsn

* Revise snnen2oOLD

* Keep ALT proofs for 1onn and 2onn

discouraged

@@ -14299,6 +14299,7 @@ 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 "1onnALT" 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).
@@ -14340,6 +14341,7 @@ 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 "2onnALT" 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).
@@ -19109,6 +19111,7 @@ New usage of "sn-wcdeq" is discouraged (0 uses).
 New usage of "snatpsubN" is discouraged (3 uses).
 New usage of "snelpwrVD" is discouraged (0 uses).
 New usage of "snexALT" is discouraged (1 uses).
+New usage of "snnen2oOLD" is discouraged (0 uses).
 New usage of "snssiALT" is discouraged (0 uses).
 New usage of "snssiALTVD" is discouraged (0 uses).
 New usage of "snssl" is discouraged (0 uses).
@@ -19598,6 +19601,7 @@ 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 "1onnALT" is discouraged (16 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).
@@ -19610,6 +19614,7 @@ 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 "2onnALT" is discouraged (16 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).
@@ -21224,6 +21229,7 @@ Proof modification of "sn-00id" is discouraged (50 steps).
 Proof modification of "snelpwrVD" is discouraged (37 steps).
 Proof modification of "snex" is discouraged (64 steps).
 Proof modification of "snexALT" is discouraged (48 steps).
+Proof modification of "snnen2oOLD" is discouraged (116 steps).
 Proof modification of "snssiALT" is discouraged (40 steps).
 Proof modification of "snssiALTVD" is discouraged (64 steps).
 Proof modification of "snssl" is discouraged (18 steps).

set.mm

@@ -68555,6 +68555,19 @@ more bytes (305 versus 282).  (Contributed by AV, 3-Feb-2021.)
       UOUPURWFVBCVIHZWHWFWIVBWFWIEBCULUMUNUOUQ $.
   $}
 
+  ${
+    $d A x y $.  $d A y z $.  $d B y z $.  $d F y z $.
+    $( If a one-to-one function with a nonempty domain has a singleton as its
+       codomain, its domain must also be a singleton.  (Contributed by
+       BTernaryTau, 1-Dec-2024.) $)
+    f1cdmsn $p |- ( ( F : A -1-1-> { B } /\ A =/= (/) ) -> E. x A = { x } ) $=
+      ( vy vz csn wf1 c0 wne wa cv wceq wral wrex wex wcel w3a cfv fvconst issn
+      wf f1f 3adant3 3adant2 eqtr4d syl3an1 f1veqaeq 3impb mpd 3expia reximdva0
+      wi ralrimiv syl ) BCGZDHZBIJKELZFLZMZFBNZEBOBALGMAPUQVAEBUQURBQZKUTFBUQVB
+      USBQZUTUQVBVCRURDSZUSDSZMZUTUQBUPDUBZVBVCVFBUPDUCVGVBVCRVDCVEVGVBVDCMVCBC
+      URDTUDVGVCVECMVBBCUSDTUEUFUGUQVBVCVFUTUMBUPURUSDUHUIUJUKUNULEFABUAUO $.
+  $}
+
   ${
     $d A f x $.  $d D f x $.  $d V f x $.  $d f ps $.  $d ph x $.
     $( TODO: there must be a more elegant way to prove this theorem using
@@ -83724,6 +83737,21 @@ other applications (for instance in intuitionistic set theory) need it.
   1n0 $p |- 1o =/= (/) $=
     ( c1o c0 csn df1o2 0ex snnz eqnetri ) ABCBDBEFG $.
 
+  $( 1 is not a limit ordinal.  (Contributed by BTernaryTau, 1-Dec-2024.) $)
+  nlim1 $p |- -. Lim 1o $=
+    ( c1o wlim word c0 wne cuni wceq w3a csn 1n0 0ex unisn neeqtrri unieqi neii
+    df1o2 simp3 mto df-lim mtbir ) ABACZADEZAAFZGZHZUEUDAUCADIZFZUCADUGJDKLMAUF
+    PNMOUAUBUDQRAST $.
+  $( $j usage 'nlim1' avoids 'ax-un'; $)
+
+  $( 2 is not a limit ordinal.  (Contributed by BTernaryTau, 1-Dec-2024.) $)
+  nlim2 $p |- -. Lim 2o $=
+    ( c2o wlim word c0 wne cuni wceq w3a c1o wcel cpr 1oex prid2 df2o3 eleqtrri
+    1on onirri eleq2 mtbiri mt2 neir cun unieqi 0ex unipr 3eqtri neeqtrri simp3
+    0un neii mto df-lim mtbir ) ABACZADEZAAFZGZHZURUQAUPAIUPAIAIGZIAJZIDIKZADIL
+    MNOUSUTIIJIPQAIIRSTUAUPVAFDIUBIAVANUCDIUDLUEIUIUFUGUJUNUOUQUHUKAULUM $.
+  $( $j usage 'nlim2' avoids 'ax-un'; $)
+
   $( Cartesian products with the singletons of ordinals 0 and 1 are disjoint.
      (Contributed by NM, 2-Jun-2007.) $)
   xp01disj $p |- ( ( A X. { (/) } ) i^i ( C X. { 1o } ) ) = (/) $=
@@ -83752,6 +83780,42 @@ other applications (for instance in intuitionistic set theory) need it.
     ( c1o wcel c0 csn wceq df1o2 eleq2i 0ex elsn2 bitri ) ABCADEZCADFBLAGHADIJK
     $.
 
+  $( An ordinal that is not 0 or 1 contains 1.  (Contributed by BTernaryTau,
+     1-Dec-2024.) $)
+  ord1eln01 $p |- ( Ord A -> ( 1o e. A <-> ( A =/= (/) /\ A =/= 1o ) ) ) $=
+    ( word c1o wcel c0 wne wa ne0i wceq 1on onirri eleq2 mtbiri necon2ai jca wo
+    wn el1o biimpi necon3ai nesym anim12ci pm4.56 sylib wb ordtri2 mpan syl5ibr
+    onordi impbid2 ) ABZCADZAEFZACFZGZULUMUNACHULACACIULCCDCJKACCLMNOUOULUKCAIZ
+    ACDZPQZUOUPQZUQQZGURUMUTUNUSUQAEUQAEIARSTUNUSACUASUBUPUQUCUDCBUKULURUECJUIC
+    AUFUGUHUJ $.
+  $( $j usage 'ord1eln01' avoids 'ax-un'; $)
+
+  $( An ordinal that is not 0, 1, or 2 contains 2.  (Contributed by
+     BTernaryTau, 1-Dec-2024.) $)
+  ord2eln012 $p |- ( Ord A ->
+      ( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) ) $=
+    ( word c2o wcel c0 wne c1o w3a ne0i wceq 2on0 nemtbir eleq2 mtbiri necon2ai
+    el1o 2on onirri 3jca wn wo wa nesym biimpi 3ad2ant3 cpr simp1 nelprd eleq2i
+    simp2 df2o3 sylnibr jca pm4.56 sylib wb onordi ordtri2 mpan syl5ibr impbid2
+    ) ABZCADZAEFZAGFZACFZHZVCVDVEVFACIVCAGAGJVCCGDZVHCEKCPLAGCMNOVCACACJVCCCDCQ
+    RACCMNOSVGVCVBCAJZACDZUATZVGVITZVJTZUBVKVGVLVMVFVDVLVEVFVLACUCUDUEVGAEGUFZD
+    VJVGAEGVDVEVFUGVDVEVFUJUHCVNAUKUIULUMVIVJUNUOCBVBVCVKUPCQUQCAURUSUTVA $.
+  $( $j usage 'ord2eln012' avoids 'ax-un'; $)
+
+  $( A limit ordinal contains 1.  (Contributed by BTernaryTau, 1-Dec-2024.) $)
+  1ellim $p |- ( Lim A -> 1o e. A ) $=
+    ( wlim c1o wcel c0 wceq nlim0 limeq mtbiri necon2ai nlim1 word wa wb limord
+    wne ord1eln01 syl mpbir2and ) ABZCADZAEPZACPZTAEAEFTEBGAEHIJTACACFTCBKACHIJ
+    TALUAUBUCMNAOAQRS $.
+  $( $j usage '1ellim' avoids 'ax-un'; $)
+
+  $( A limit ordinal contains 2.  (Contributed by BTernaryTau, 1-Dec-2024.) $)
+  2ellim $p |- ( Lim A -> 2o e. A ) $=
+    ( wlim c2o wcel c0 wne c1o wceq nlim0 limeq mtbiri necon2ai nlim1 nlim2 w3a
+    word wb limord ord2eln012 syl mpbir3and ) ABZCADZAEFZAGFZACFZUBAEAEHUBEBIAE
+    JKLUBAGAGHUBGBMAGJKLUBACACHUBCBNACJKLUBAPUCUDUEUFOQARASTUA $.
+  $( $j usage '2ellim' avoids 'ax-un'; $)
+
   $( Two ways to say that ` A ` is a nonzero number of the set ` B ` .
      (Contributed by Mario Carneiro, 21-May-2015.) $)
   dif1o $p |- ( A e. ( B \ 1o ) <-> ( A e. B /\ A =/= (/) ) ) $=
@@ -85925,13 +85989,33 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so
       VASURVEVNVHNVFVEVMVHADWDVJVLVHWDVJFWBVLVHWDVJWBWHUSWCUTVBVCSVD $.
   $}
 
-  $( One is a natural number.  (Contributed by NM, 29-Oct-1995.) $)
+  $( The ordinal 1 is a natural number.  For a shorter proof using Peano's
+     postulates that depends on ~ ax-un , see ~ 1onnALT .  (Contributed by NM,
+     29-Oct-1995.)  Avoid ~ ax-un .  (Revised by BTernaryTau, 1-Dec-2024.) $)
   1onn $p |- 1o e. _om $=
+    ( vx c1o com wcel con0 cv wlim wi wal 1on 1ellim ax-gen elom mpbir2an ) BCD
+    BEDAFZGBODHZAIJPAOKLABMN $.
+  $( $j usage '1onn' avoids 'ax-un'; $)
+
+  $( Shorter proof of ~ 1onn using Peano's postulates that depends on ~ ax-un .
+     (Contributed by NM, 29-Oct-1995.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  1onnALT $p |- 1o e. _om $=
     ( c1o c0 csuc com df-1o wcel peano1 peano2 ax-mp eqeltri ) ABCZDEBDFKDFGBHI
     J $.
 
-  $( The ordinal 2 is a natural number.  (Contributed by NM, 28-Sep-2004.) $)
+  $( The ordinal 2 is a natural number.  For a shorter proof using Peano's
+     postulates that depends on ~ ax-un , see ~ 2onnALT .  (Contributed by NM,
+     28-Sep-2004.)  Avoid ~ ax-un .  (Revised by BTernaryTau, 1-Dec-2024.) $)
   2onn $p |- 2o e. _om $=
+    ( vx c2o com wcel con0 cv wlim wi wal 2on 2ellim ax-gen elom mpbir2an ) BCD
+    BEDAFZGBODHZAIJPAOKLABMN $.
+  $( $j usage '2onn' avoids 'ax-un'; $)
+
+  $( Shorter proof of ~ 2onn using Peano's postulates that depends on ~ ax-un .
+     (Contributed by NM, 28-Sep-2004.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  2onnALT $p |- 2o e. _om $=
     ( c2o c1o csuc com df-2o wcel 1onn peano2 ax-mp eqeltri ) ABCZDEBDFKDFGBHIJ
     $.
 
@@ -92536,16 +92620,6 @@ proved without using the Axiom of Power Sets (unlike ~ domsdomtr ).
     $( $j usage 'phpeqd' avoids 'ax-pow'; $)
   $}
 
-  $( A singleton ` { A } ` is never equinumerous with the ordinal number 2.
-     This holds for proper singletons ( ` A e. _V ` ) as well as for singletons
-     being the empty set ( ` A e/ _V ` ).  (Contributed by AV, 6-Aug-2019.) $)
-  snnen2o $p |- -. { A } ~~ 2o $=
-    ( cvv wcel csn c2o cen wbr wn c1o csuc com 1onn php5 ax-mp ensn1g wi ensymb
-    df-2o c0 wceq eqcomi breq2i entr ex sylbi con3rr3 sylnbi mpsyl 2on0 nemtbir
-    en0 bitri snprc biimpi breq1d mtbiri pm2.61i ) ABCZADZEFGZHZIIJZFGZHZURUSIF
-    GZVAIKCVDLIMNABOVCIEFGZVEVAPVBEIFEVBRUAUBVEUTVFVEIUSFGZUTVFPUSIQVGUTVFIUSEU
-    CUDUEUFUGUHURHZUTSEFGZVIESUIVIESFGESTSEQEUKULUJVHUSSEFVHUSSTAUMUNUOUPUQ $.
-
   $( Cardinal ordering agrees with ordinal number ordering when the smaller
      number is a natural number.  Compare with ~ nndomo when both are natural
      numbers.  (Contributed by NM, 17-Jun-1998.)  Generalize from ~ nndomo .
@@ -92731,6 +92805,16 @@ being the empty set ( ` A e/ _V ` ).  (Contributed by AV, 6-Aug-2019.) $)
     UTABNOABPSQUMARZBRZUQUSTUNAUJBUKVAVBFZUQBADZKUSABUAVCVDURVBVAVDURTBAUBUCUDU
     LUEUFUNUQUPLUMABEUGUHUI $.
 
+  $( Obsolete version of ~ snnen2o as of 18-Nov-2024.  (Contributed by AV,
+     6-Aug-2019.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  snnen2oOLD $p |- -. { A } ~~ 2o $=
+    ( cvv wcel csn c2o cen wbr wn c1o csuc com 1onn php5 ax-mp ensn1g wi ensymb
+    df-2o c0 wceq eqcomi breq2i entr ex sylbi con3rr3 sylnbi mpsyl 2on0 nemtbir
+    en0 bitri snprc biimpi breq1d mtbiri pm2.61i ) ABCZADZEFGZHZIIJZFGZHZURUSIF
+    GZVAIKCVDLIMNABOVCIEFGZVEVAPVBEIFEVBRUAUBVEUTVFVEIUSFGZUTVFPUSIQVGUTVFIUSEU
+    CUDUEUFUGUHURHZUTSEFGZVIESUIVIESFGESTSEQEUKULUJVHUSSEFVHUSSTAUMUNUOUPUQ $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -92854,6 +92938,23 @@ Finite sets (cont.)
       EWFXMXTFXSXPXRWGXHWSXLXSWHWIWNXHWSFERWJWKWLWMWOWPWQWR $.
   $}
 
+  ${
+    $d A f $.
+    $( A singleton ` { A } ` is never equinumerous with the ordinal number 2.
+       This holds for proper singletons ( ` A e. _V ` ) as well as for
+       singletons being the empty set ( ` A e/ _V ` ).  (Contributed by AV,
+       6-Aug-2019.)  Avoid ~ ax-pow , ~ ax-un .  (Revised by BTernaryTau,
+       1-Dec-2024.) $)
+    snnen2o $p |- -. { A } ~~ 2o $=
+      ( vf vx csn c2o cen wbr cv wf1o wex ccnv wf1 wceq c0 c1o cvv wcel wne nex
+      mto cpr df2o3 0ex 1oex 1n0 necomi prnesn mp3an eqnetri neii f1cdmsn mpan2
+      2on0 f1ocnv f1of1 syl wb snex 2oex breng mp2an mtbir ) ADZEFGZVCEBHZIZBJZ
+      VFBVFEVCVEKZLZVIECHZDZMZCJZVLCEVKENOUAZVKUBNPQOPQNORVNVKRUCUDONUEUFNOVJPP
+      UGUHUIUJSVIENRVMUMCEAVHUKULTVFEVCVHIVIVCEVEUNEVCVHUOUPTSVCPQEPQVDVGUQAURU
+      SVCEBPPUTVAVB $.
+    $( $j usage 'snnen2o' avoids 'ax-pow' 'ax-un'; $)
+  $}
+
   ${
     $d F w z $.  $d a b m n s t w x z $.
     unxpdomlem1.1 $e |- F = ( x e. ( a u. b ) |-> G ) $.