Edit comment of ~dfid(2|3).

benjub · Nov 10, 2024 · 80798d5 · 80798d5
1 parent 2142f9d
commit 80798d5
Showing 1 changed file with 31 additions and 25 deletions.
diff --git a/set.mm b/set.mm
@@ -52397,17 +52397,40 @@ necessary if all involved classes exist as sets (i.e. are not proper
       OABFTQR $.
   $}
 
+  ${
+    $d x y z u $.
+    $( Alternate definition of the identity relation.  Instance of ~ dfid3 not
+       requiring auxiliary axioms.  (Contributed by NM, 15-Mar-2007.)  Reduce
+       axiom usage.  (Revised by Gino Giotto, 4-Nov-2024.)  (Proof shortened by
+       BJ, 5-Nov-2024.)
+
+       Use ~ df-id instead to make the semantics of the constructor ~ df-opab
+       clearer (in usages, ` x , y ` will typically be dummy variables, so can
+       be assumed disjoint).  (New usage is discouraged.) $)
+    dfid2 $p |- _I = { <. x , x >. | x = x } $=
+      ( vy vz vu cid weq copab df-id cv cop wceq wa wex cab opeq2d eqeq2d exbii
+      equcomi bitri df-opab pm5.32ri ax6evr mpbiran2 pm4.71i id opeq12d eqeq12d
+      19.42v eqidd anbi12d exexw abbii 3eqtr4i eqtri ) EABFZABGZAAFZAAGZABHCIZA
+      IZBIZJZKZUOLZBMZAMZCNUSUTUTJZKZUQLZAMZAMZCNUPURVFVKCVFVJVKVEVIAVEVHVIVEVH
+      UOLZBMZVHVDVLBUOVCVHUOVBVGUSUOVAUTUTABROPUAQVMVHUOBMBAUBVHUOBUHUCSVHUQVHU
+      TUIUDSQVIUSDIZVNJZKZDDFZLADADFZVHVPUQVQVRVGVOUSVRUTVNUTVNVRUEZVSUFPVRUTVN
+      UTVNVSVSUGUJUKSULUOABCTUQAACTUMUN $.
+    $( $j usage 'dfid2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
   ${
     $d w z x $.  $d w z y $.
     $( A stronger version of ~ df-id that does not require ` x ` and ` y ` to
-       be disjoint.  This is not the "official" definition since our definition
-       soundness check without this requirement would be much more complex.
-       The proof can be instructive in showing how disjoint variable
-       requirements may be eliminated, a task that is not necessarily obvious.
-       (Contributed by NM, 5-Feb-2008.)  (Revised by Mario Carneiro,
-       18-Nov-2016.)  Use directly Definition ~ df-id when sufficient, since
-       the derivation of ~ dfid3 is nontrivial and uses auxiliary axioms
-       ~ ax-10 to ~ ax-13 .  (New usage is discouraged.) $)
+       be disjoint.  This is not the definition since, in order to pass our
+       definition soundness test, a definition has to have disjoint dummy
+       variables, see ~ conventions .  The proof can be instructive in showing
+       how disjoint variable conditions may be eliminated, a task that is not
+       necessarily obvious.  (Contributed by NM, 5-Feb-2008.)  (Revised by
+       Mario Carneiro, 18-Nov-2016.)
+
+       Use ~ df-id instead to make the semantics of the constructor ~ df-opab
+       clearer (in usages, ` x , y ` will typically be dummy variables, so can
+       be assumed disjoint).  (New usage is discouraged.) $)
     dfid3 $p |- _I = { <. x , y >. | x = y } $=
       ( vz vw weq copab cv cop wa wex cab wb exbii opeq2 eqeq2d equequ2 anbi12d
       wceq nfnae nfcvd cid df-id wal equcom anbi1ci equsexvw equid biantru nfe1
@@ -52421,23 +52444,6 @@ necessary if all involved classes exist as sets (i.e. are not proper
       VOVQWCVPNOCBAPQVBVDVEVFVGVKACDVHVMABDVHVIVJ $.
   $}
 
-  ${
-    $d x y z u $.
-    $( Alternate definition of the identity relation.  (Contributed by NM,
-       15-Mar-2007.)  Use ~ df-id when sufficient (see comment at ~ dfid3 ).
-       (New usage is discouraged.)  Reduce axiom usage.  (Revised by Gino
-       Giotto, 4-Nov-2024.)  (Proof shortened by BJ, 5-Nov-2024.) $)
-    dfid2 $p |- _I = { <. x , x >. | x = x } $=
-      ( vy vz vu cid weq copab df-id cv cop wceq wa wex cab opeq2d eqeq2d exbii
-      equcomi bitri df-opab pm5.32ri ax6evr mpbiran2 pm4.71i id opeq12d eqeq12d
-      19.42v eqidd anbi12d exexw abbii 3eqtr4i eqtri ) EABFZABGZAAFZAAGZABHCIZA
-      IZBIZJZKZUOLZBMZAMZCNUSUTUTJZKZUQLZAMZAMZCNUPURVFVKCVFVJVKVEVIAVEVHVIVEVH
-      UOLZBMZVHVDVLBUOVCVHUOVBVGUSUOVAUTUTABROPUAQVMVHUOBMBAUBVHUOBUHUCSVHUQVHU
-      TUIUDSQVIUSDIZVNJZKZDDFZLADADFZVHVPUQVQVRVGVOUSVRUTVNUTVNVRUEZVSUFPVRUTVN
-      UTVNVSVSUGUJUKSULUOABCTUQAACTUMUN $.
-    $( $j usage 'dfid2' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
-  $}
-
   $( Obsolete version of ~ dfid2 as of 4-Nov-2024.  (Contributed by NM,
      15-Mar-2007.)  (Proof modification is discouraged.)
      (New usage is discouraged.) $)