diff --git a/discouraged b/discouraged
index 7ba3fb6032..e971a2a1a8 100644
--- a/discouraged
+++ b/discouraged
@@ -17683,6 +17683,7 @@ New usage of "omlsi" is discouraged (1 uses).
 New usage of "omlsii" is discouraged (4 uses).
 New usage of "omlsilem" is discouraged (1 uses).
 New usage of "omlspjN" is discouraged (2 uses).
+New usage of "omsindsOLD" is discouraged (0 uses).
 New usage of "ondomon" is discouraged (0 uses).
 New usage of "onfrALT" is discouraged (0 uses).
 New usage of "onfrALTVD" is discouraged (0 uses).
@@ -18005,6 +18006,7 @@ New usage of "poml5N" is discouraged (1 uses).
 New usage of "poml6N" is discouraged (1 uses).
 New usage of "prcdnq" is discouraged (14 uses).
 New usage of "prclisacycgr" is discouraged (0 uses).
+New usage of "predonOLD" is discouraged (0 uses).
 New usage of "preleqALT" is discouraged (0 uses).
 New usage of "prlem934" is discouraged (3 uses).
 New usage of "prlem936" is discouraged (1 uses).
@@ -20097,6 +20099,7 @@ Proof modification of "nsnlpligALT" is discouraged (110 steps).
 Proof modification of "nsyl2OLD" is discouraged (12 steps).
 Proof modification of "o2p2e4OLD" is discouraged (67 steps).
 Proof modification of "odfvalALT" is discouraged (181 steps).
+Proof modification of "omsindsOLD" is discouraged (89 steps).
 Proof modification of "ondomon" is discouraged (287 steps).
 Proof modification of "onfrALT" is discouraged (88 steps).
 Proof modification of "onfrALTVD" is discouraged (152 steps).
@@ -20138,6 +20141,7 @@ Proof modification of "pm2.43bgbi" is discouraged (16 steps).
 Proof modification of "pm2.43cbi" is discouraged (34 steps).
 Proof modification of "pm2.61iOLD" is discouraged (13 steps).
 Proof modification of "poclOLD" is discouraged (270 steps).
+Proof modification of "predonOLD" is discouraged (29 steps).
 Proof modification of "preleqALT" is discouraged (115 steps).
 Proof modification of "prmdvdssqOLD" is discouraged (62 steps).
 Proof modification of "prmgaplcm" is discouraged (247 steps).
diff --git a/iset.mm b/iset.mm
index 239874febe..c01545412f 100644
--- a/iset.mm
+++ b/iset.mm
@@ -158588,9 +158588,9 @@ with definitions ( ` B ` is the definiendum that one wants to prove
     $d x A $.  $d x B $.
     $( Equality property for ` Ind ` .  (Contributed by BJ, 30-Nov-2019.) $)
     bj-indeq $p |- ( A = B -> ( Ind A <-> Ind B ) ) $=
-      ( vx wind c0 wcel cv csuc wral wa wceq df-bj-ind eleq2 raleqbi1dv anbi12d
-      bicomd bitr2id syl5bb ) ADEAFZCGHZAFZCAIZJZABKZBDZCALUEEBFZTBFZCBIZJUDUCC
-      BLUDUFSUHUBUDSUFABEMPUDUBUHUAUGCABABTMNPOQR $.
+      ( vx wceq c0 wcel cv csuc wral wa wind eleq2 raleqbi1dv anbi12d df-bj-ind
+      3bitr4g ) ABDZEAFZCGHZAFZCAIZJEBFZSBFZCBIZJAKBKQRUBUAUDABELTUCCABABSLMNCA
+      OCBOP $.
   $}
 
   ${
diff --git a/set.mm b/set.mm
index a47b777b72..1662a16d21 100644
--- a/set.mm
+++ b/set.mm
@@ -58418,7 +58418,7 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
   cpred $a class Pred ( R , A , X ) $.
 
   $( Define the predecessor class of a binary relation.  This is the class of
-     all elements ` y ` of ` A ` such that ` y R X ` (see ~ elpred ) .
+     all elements ` y ` of ` A ` such that ` y R X ` (see ~ elpred ).
      (Contributed by Scott Fenton, 29-Jan-2011.) $)
   df-pred $a |- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) ) $.
 
@@ -73444,8 +73444,15 @@ be a set (so instead it is a proper class).  Here we prove the denial of
     ( con0 wcel word wss eloni ordsson syl ) ABCADABEAFAGH $.
 
   $( The predecessor of an ordinal under ` _E ` and ` On ` is itself.
-     (Contributed by Scott Fenton, 27-Mar-2011.) $)
+     (Contributed by Scott Fenton, 27-Mar-2011.)  (Proof shortened by BJ,
+     16-Oct-2024.) $)
   predon $p |- ( A e. On -> Pred ( _E , On , A ) = A ) $=
+    ( con0 wtr wcel cep cpred wceq tron trpred mpan ) BCABDBEAFAGHBAIJ $.
+
+  $( Obsolete version of ~ predon as of 16-Oct-2024.  (Contributed by Scott
+     Fenton, 27-Mar-2011.)  (Proof modification is discouraged.)
+     (New usage is discouraged.) $)
+  predonOLD $p |- ( A e. On -> Pred ( _E , On , A ) = A ) $=
     ( con0 wcel cep cpred cin predep wss wceq onss sseqin2 sylib eqtrd ) ABCZBD
     AEBAFZABBAGNABHOAIAJABKLM $.
 
@@ -74424,23 +74431,28 @@ also define a subset of the complex numbers ( ~ df-nn ) with analogous
 
   ${
     $d x y z $.
-    $( Omega is ordinal.  Theorem 7.32 of [TakeutiZaring] p. 43.  (Contributed
-       by NM, 18-Oct-1995.)  (Proof shortened by Andrew Salmon,
+    $( The class of finite ordinals ` _om ` is a transitive class.
+       (Contributed by NM, 18-Oct-1995.)  (Proof shortened by Andrew Salmon,
        27-Aug-2011.) $)
-    ordom $p |- Ord _om $=
-      ( vy vx vz com wtr con0 wss word wel cv wcel wa wi wal wlim onelon expcom
-      dftr2 limord elom ordtr trel 3syl com12 a2d alimdv anim12d 3imtr4g ax-gen
-      expd imp mpgbir omsson ordon trssord mp3an ) DEZDFGFHDHUQABIZBJZDKZLAJZDK
-      ZMZBNAABDRVCBURUTVBURUSFKZCJZOZBCIZMZCNZLVAFKZVFACIZMZCNZLUTVBURVDVJVIVMV
-      DURVJUSVAPQURVHVLCURVFVGVKVFURVGVKMVFURVGVKVFVEHVEEURVGLVKMVESVEUAVEVAUSU
-      BUCUJUDUEUFUGCUSTCVATUHUKUIULUMUNDFUOUP $.
+    trom $p |- Tr _om $=
+      ( vy vx vz com wtr wel cv wcel wa wi dftr2 con0 wlim onelon expcom limord
+      wal word ordtr elom trel 3syl com12 a2d alimdv anim12d 3imtr4g imp ax-gen
+      expd mpgbir ) DEABFZBGZDHZIAGZDHZJZBQAABDKUQBULUNUPULUMLHZCGZMZBCFZJZCQZI
+      UOLHZUTACFZJZCQZIUNUPULURVDVCVGURULVDUMUONOULVBVFCULUTVAVEUTULVAVEJUTULVA
+      VEUTUSRUSEULVAIVEJUSPUSSUSUOUMUAUBUJUCUDUEUFCUMTCUOTUGUHUIUK $.
   $}
 
+  $( The class of finite ordinals ` _om ` is ordinal.  Theorem 7.32 of
+     [TakeutiZaring] p. 43.  (Contributed by NM, 18-Oct-1995.)  (Proof
+     shortened by Andrew Salmon, 27-Aug-2011.) $)
+  ordom $p |- Ord _om $=
+    ( com wtr con0 wss word trom omsson ordon trssord mp3an ) ABACDCEAEFGHACIJ
+    $.
+
   $( A member of a natural number is a natural number.  (Contributed by NM,
      21-Jun-1998.) $)
   elnn $p |- ( ( A e. B /\ B e. _om ) -> A e. _om ) $=
-    ( com word wtr wcel wa wi ordom ordtr trel mp2b ) CDCEABFBCFGACFHICJCABKL
-    $.
+    ( com wtr wcel wa wi trom trel ax-mp ) CDABEBCEFACEGHCABIJ $.
 
   $( The class of natural numbers ` _om ` is either an ordinal number (if we
      accept the Axiom of Infinity) or the proper class of all ordinal numbers
@@ -74526,13 +74538,23 @@ also define a subset of the complex numbers ( ~ df-nn ) with analogous
     omsinds.2 $e |- ( x = A -> ( ph <-> ch ) ) $.
     omsinds.3 $e |- ( x e. _om -> ( A. y e. x ps -> ph ) ) $.
     $( Strong (or "total") induction principle over the finite ordinals.
-       (Contributed by Scott Fenton, 17-Jul-2015.) $)
+       (Contributed by Scott Fenton, 17-Jul-2015.)  (Proof shortened by BJ,
+       16-Oct-2024.) $)
     omsinds $p |- ( A e. _om -> ch ) $=
+      ( com cep con0 wss wwe omsson epweon wess mp2 epse wral cv wcel cpred wtr
+      wceq trom trpred mpan raleqdv sylbid wfis3 ) ABCDEJFKJLMLKNJKNOPJLKQRJSGH
+      DUAZJUBZBEJKULUCZTBEULTAUMBEUNULJUDUMUNULUEUFJULUGUHUIIUJUK $.
+
+    $( Obsolete version of ~ omsinds as of 16-Oct-2024.  (Contributed by Scott
+       Fenton, 17-Jul-2015.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    omsindsOLD $p |- ( A e. _om -> ch ) $=
       ( com cep con0 wss wwe omsson epweon wess mp2 epse wral cv wcel cpred cin
       predep wceq word wtr wi ordom ordtr trss mp2b sseqin2 sylib eqtrd raleqdv
       sylbid wfis3 ) ABCDEJFKJLMLKNJKNOPJLKQRJSGHDUAZJUBZBEJKUTUCZTBEUTTAVABEVB
       UTVAVBJUTUDZUTJJUTUEVAUTJMZVCUTUFJUGJUHVAVDUIUJJUKJUTULUMUTJUNUOUPUQIURUS
       $.
+
   $}