Add trfr and tcfr theorems (#5072)

Author: EricSchmidt-119

set.mm

@@ -747824,6 +747824,37 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5
     FGBEHMEHIJMBEEFKL $.
   $( $j usage 'wffr' avoids 'ax-reg'; $)
 
+  ${
+    $d y z A $.
+
+    $( A transitive class well-founded by ` e. ` is a subclass of the class of
+       well-founded sets.  Part of Lemma I.9.21 of [Kunen2] p. 53.
+       (Contributed by Eric Schmidt, 26-Oct-2025.) $)
+    trfr $p |- ( ( Tr A /\ _E Fr A ) -> A C_ U. ( R1 " On ) ) $=
+      ( vy vz cep wfr wtr cr1 con0 cima cuni wss cv wcel wral wi wse epse dfss3
+      r19.21v bitr4di cpred wa wb trpred raleq vex r1elss syl biimpd expcom a2d
+      wceq biimtrid weq eleq1w imbi2d frins2 mpan2 sylib imbitrrdi impcom ) ADE
+      ZAFZAGHIJZKZVBVCBLZVDMZBANZVEVBVCVGOZBANZVCVHOVBADPVJAQVIVCCLVDMZOZBCADVL
+      CADVFUAZNVCVKCVMNZOVFAMZVIVCVKCVMSVOVCVNVGVCVOVNVGOVCVOUBZVNVGVPVMVFULZVN
+      VGUCAVFUDVQVNVFVDKZVGVQVNVKCVFNVRVKCVMVFUECVFVDRTVFBUFUGTUHUIUJUKUMBCUNVG
+      VKVCBCVDUOUPUQURVCVGBASUSBAVDRUTVA $.
+    $( $j usage 'trfr' avoids 'ax-reg'; $)
+  $}
+
+  ${
+    tcfr.1 $e |- A e. _V $.
+    $( A set is well-founded if and only if its transitive closure is
+       well-founded by ` e. ` .  This characterization of well-founded sets is
+       that in Definition I.9.20 of [Kunen2] p. 53.  (Contributed by Eric
+       Schmidt, 26-Oct-2025.) $)
+    tcfr $p |- ( A e. U. ( R1 " On ) <-> _E Fr ( TC ` A ) ) $=
+      ( cr1 con0 cima cuni wcel ctc cfv cep wfr wss tcwf r1elssi wffr frss 3syl
+      mpi cvv tcid ax-mp wtr tctr trfr mpan sstrid r1elss sylibr impbii ) ACDEF
+      ZGZAHIZJKZUKULUJGULUJLZUMAMULNUNUJJKUMOULUJJPRQUMAUJLUKUMAULUJASGAULLBAST
+      UAULUBUMUNAUCULUDUEUFABUGUHUI $.
+    $( $j usage 'tcfr' avoids 'ax-reg'; $)
+  $}
+
   $( The Cartesian product of two well-founded sets is well-founded.
      (Contributed by Eric Schmidt, 12-Sep-2025.) $)
   xpwf $p |- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) ->