Revise 2onn

discouraged

@@ -14332,6 +14332,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 "2onnOLD" 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).
@@ -19600,6 +19601,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 "2onnOLD" 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).

set.mm

@@ -85951,8 +85951,17 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so
     ( 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.  (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'; $)
+
+  $( Obsolete version of ~ 2onn as of 1-Dec-2024.  (Contributed by NM,
+     28-Sep-2004.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  2onnOLD $p |- 2o e. _om $=
     ( c2o c1o csuc com df-2o wcel 1onn peano2 ax-mp eqeltri ) ABCZDEBDFKDFGBHIJ
     $.