Verification fixes

discouraged

@@ -20914,6 +20914,7 @@ Proof modification of "ttglemOLD" is discouraged (273 steps).
 Proof modification of "ttgplusgOLD" is discouraged (25 steps).
 Proof modification of "ttgvscaOLD" is discouraged (25 steps).
 Proof modification of "tuslemOLD" is discouraged (304 steps).
+Proof modification of "tz6.26OLD" is discouraged (96 steps).
 Proof modification of "umgr2adedgwlkonALT" is discouraged (294 steps).
 Proof modification of "un0.1" is discouraged (21 steps).
 Proof modification of "un01" is discouraged (18 steps).
@@ -20990,6 +20991,9 @@ Proof modification of "vtoclALT" is discouraged (11 steps).
 Proof modification of "vtocldOLD" is discouraged (21 steps).
 Proof modification of "vtoclgOLD" is discouraged (11 steps).
 Proof modification of "vtxdusgr0edgnelALT" is discouraged (94 steps).
+Proof modification of "wfiOLD" is discouraged (227 steps).
+Proof modification of "wfis2fgOLD" is discouraged (51 steps).
+Proof modification of "wfisgOLD" is discouraged (204 steps).
 Proof modification of "wl-cases2-dnf" is discouraged (85 steps).
 Proof modification of "wl-dfclab" is discouraged (73 steps).
 Proof modification of "wl-embant" is discouraged (12 steps).

set.mm

@@ -59362,8 +59362,9 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
   ${
     $d x y A $.  $d x y B $.  $d x y R $.
     $( Obsolete proof of ~ tz6.26 as of 17-Nov-2024.
-       (New usage is discouraged.)  (Contributed by Scott Fenton, 29-Jan-2011.)
-       (Revised by Mario Carneiro, 26-Jun-2015.) $)
+       (New usage is discouraged.)  (Proof modification is discouraged.)
+       (Contributed by Scott Fenton, 29-Jan-2011.)  (Revised by Mario Carneiro,
+       26-Jun-2015.) $)
     tz6.26OLD $p |- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) ->
                     E. y e. B Pred ( R , B , y ) = (/) ) $=
       ( vx wwe wse wa wss c0 wne cv wbr wn wral wrex cpred wceq wreu wereu2 syl
@@ -59408,8 +59409,8 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
   ${
     $d A y $.  $d B y $.  $d R y $.
     $( Obsolete proof of ~ wfi as of 17-Nov-2024.  (New usage is discouraged.)
-       (Contributed by Scott Fenton, 29-Jan-2011.)  (Revised by Mario Carneiro,
-       26-Jun-2015.) $)
+       (Proof modification is discouraged.)  (Contributed by Scott Fenton,
+       29-Jan-2011.)  (Revised by Mario Carneiro, 26-Jun-2015.) $)
     wfiOLD $p |- ( ( ( R We A /\ R Se A ) /\
                     ( B C_ A /\
                       A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) )
@@ -59465,8 +59466,8 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
     wfisgOLD.1 $e |- ( y e. A ->
                        ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) $.
     $( Obsolete proof of ~ wfisg as of 17-Nov-2024.
-       (New usage is discouraged.)  (Contributed by Scott Fenton,
-       11-Feb-2011.) $)
+       (New usage is discouraged.)  (Proof modification is discouraged.)
+       (Contributed by Scott Fenton, 11-Feb-2011.) $)
     wfisgOLD $p |- ( ( R We A /\ R Se A ) -> A. y e. A ph ) $=
       ( vw wa wceq wral wss cv cpred wcel wi wsbc nfcv elrabsf nfsbc1v nfim wwe
       wse crab ssrab2 dfss3 simprbi ralimi sylbi nfralw predeq3 raleqdv sbceq1a
@@ -59512,8 +59513,8 @@ singleton of the first member (with no sethood assumptions on ` B ` ).
     wfis2fgOLD.2 $e |- ( y = z -> ( ph <-> ps ) ) $.
     wfis2fgOLD.3 $e |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) ) $.
     $( Obsolete proof of ~ wfis2fg as of 17-Nov-2024.
-       (New usage is discouraged.)  (Contributed by Scott Fenton,
-       11-Feb-2011.) $)
+       (New usage is discouraged.)  (Proof modification is discouraged.)
+       (Contributed by Scott Fenton, 11-Feb-2011.) $)
     wfis2fgOLD $p |- ( ( R We A /\ R Se A ) -> A. y e. A ph ) $=
       ( cv wsbc cpred wral wcel wsb sbsbc sbiev bitr3i ralbii syl5bi wfisg ) AC
       DEFACDJKZDEFCJZLZMBDUDMUCENAUBBDUDUBACDOBACDPABCDGHQRSITUA $.