Add some cross-links in comments. (#4517)

Co-authored-by: benoit.jubin <>

set.mm

@@ -16998,9 +16998,9 @@ variables and no wff metavariables (see ~ ax12wdemo for an example of
   ${
     $d y z $.  $d x y $.  $d z ph $.  $d y ps $.
     alcomiw.1 $e |- ( y = z -> ( ph <-> ps ) ) $.
-    $( Weak version of ~ alcom .  Uses only Tarski's FOL axiom schemes.
-       (Contributed by NM, 10-Apr-2017.)  (Proof shortened by Wolf Lammen,
-       28-Dec-2023.) $)
+    $( Weak version of ~ ax-11 .  See ~ alcomw for the biconditional form.
+       Uses only Tarski's FOL axiom schemes.  (Contributed by NM, 10-Apr-2017.)
+       (Proof shortened by Wolf Lammen, 28-Dec-2023.) $)
     alcomiw $p |- ( A. x A. y ph -> A. y A. x ph ) $=
       ( wal cbvalvw biimpi alimi ax-5 wi weq biimprd equcoms spimvw 2alimi 3syl
       ) ADGZCGBEGZCGZUADGACGDGSTCSTABDEFHIJUADKTADCBAEDBALDEDEMABFNOPQR $.
@@ -17013,8 +17013,9 @@ variables and no wff metavariables (see ~ ax12wdemo for an example of
     $d w x $.
     alcomw.1 $e |- ( x = w -> ( ph <-> ps ) ) $.
     alcomw.2 $e |- ( y = z -> ( ph <-> ch ) ) $.
-    $( Weak version of ~ alcom .  Uses only Tarski's FOL axiom schemes.
-       (Contributed by BTernaryTau, 28-Dec-2024.) $)
+    $( Weak version of ~ alcom and biconditional form of ~ alcomiw .  Uses only
+       Tarski's FOL axiom schemes.  (Contributed by BTernaryTau,
+       28-Dec-2024.) $)
     alcomw $p |- ( A. x A. y ph <-> A. y A. x ph ) $=
       ( wal alcomiw impbii ) AEJDJADJEJACDEFIKABEDGHKL $.
     $( $j usage 'alcomw' avoids 'ax-8' 'ax-9' 'ax-10' 'ax-11' 'ax-12'
@@ -18385,7 +18386,8 @@ scheme is logically redundant (see ~ ax10w ) but is used as an auxiliary
      preprint).  Also appears as Lemma 12 of [Monk2] p. 109 and Axiom C5-3 of
      [Monk2] p. 113.  This axiom scheme is logically redundant (see ~ ax11w )
      but is used as an auxiliary axiom scheme to achieve metalogical
-     completeness.  (Contributed by NM, 12-Mar-1993.) $)
+     completeness.  Use its weak version ~ alcomiw when it allows to avoid
+     dependence on ~ ax-11 .  (Contributed by NM, 12-Mar-1993.) $)
   ax-11 $a |- ( A. x A. y ph -> A. y A. x ph ) $.
 
   ${
@@ -18395,7 +18397,9 @@ scheme is logically redundant (see ~ ax10w ) but is used as an auxiliary
       ( wal ax-11 syl ) ACFDFADFCFBADCGEH $.
   $}
 
-  $( Theorem 19.5 of [Margaris] p. 89.  (Contributed by NM, 30-Jun-1993.) $)
+  $( Theorem 19.5 of [Margaris] p. 89.  Use its weak version ~ alcomw when it
+     allows to avoid dependence on ~ ax-11 .  (Contributed by NM,
+     30-Jun-1993.) $)
   alcom $p |- ( A. x A. y ph <-> A. y A. x ph ) $=
     ( wal ax-11 impbii ) ACDBDABDCDABCEACBEF $.
 
@@ -49121,16 +49125,17 @@ although the definition does not require it (see ~ dfid2 for a case
   $( Define the transitive class predicate.  Not to be confused with a
      transitive relation (see ~ cotr ).  Definition of [Enderton] p. 71
      extended to arbitrary classes.  For alternate definitions, see ~ dftr2
-     (which is suggestive of the word "transitive"), ~ dftr3 , ~ dftr4 ,
-     ~ dftr5 , and (when ` A ` is a set) ~ unisuc .  The term "complete" is
-     used instead of "transitive" in Definition 3 of [Suppes] p. 130.
-     (Contributed by NM, 29-Aug-1993.) $)
+     (which is suggestive of the word "transitive"), ~ dftr2c , ~ dftr3 ,
+     ~ dftr4 , ~ dftr5 , and (when ` A ` is a set) ~ unisuc .  The term
+     "complete" is used instead of "transitive" in Definition 3 of [Suppes]
+     p. 130.  (Contributed by NM, 29-Aug-1993.) $)
   df-tr $a |- ( Tr A <-> U. A C_ A ) $.
 
   ${
     $d x y A $.
     $( An alternate way of defining a transitive class.  Exercise 7 of
-       [TakeutiZaring] p. 40.  (Contributed by NM, 24-Apr-1994.) $)
+       [TakeutiZaring] p. 40.  Using ~ dftr2c instead may avoid dependences on
+       ~ ax-11 .  (Contributed by NM, 24-Apr-1994.) $)
     dftr2 $p |- ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) ) $=
       ( cuni wss cv wcel wi wal wa dfss2 df-tr 19.23v eluni imbi1i bitr4i albii
       wtr wex 3bitr4i ) CDZCEAFZUAGZUBCGZHZAICRUBBFZGUFCGJZUDHBIZAIAUACKCLUHUEA