From 4b610805cb0068923bfb09fb3c729508f248d047 Mon Sep 17 00:00:00 2001
From: Benoit <41090811+benjub@users.noreply.github.com>
Date: Sun, 10 Nov 2024 17:37:20 +0100
Subject: [PATCH] iset: fix typo in ~ifelpwund and ~ifexd. (#4381)

* iset: fix typo in ~ifelpwund and ~ifexd.

* Edit comment of ~dfid(2|3).
---
 iset.mm |  8 ++++----
 set.mm  | 55 ++++++++++++++++++++++++++++++-------------------------
 2 files changed, 34 insertions(+), 29 deletions(-)

diff --git a/iset.mm b/iset.mm
index 8ea2bec77..49a5765f0 100644
--- a/iset.mm
+++ b/iset.mm
@@ -39764,8 +39764,8 @@ rather than an implication (but the two are equivalent by ~ bm1.3ii ),
     ifelpwund.2 $e |- ( ph -> B e. W ) $.
     $( Existence of a conditional class, quantitative version (deduction form).
        (Contributed by BJ, 15-Aug-2024.) $)
-    ifelpwund $p |- ( ph -> if ( ph , A , B ) e. ~P ( A u. B ) ) $=
-      ( wcel cif cun cpw ifelpwung syl2anc ) ABDHCEHABCIBCJKHFGABCDELM $.
+    ifelpwund $p |- ( ph -> if ( ps , A , B ) e. ~P ( A u. B ) ) $=
+      ( wcel cif cun cpw ifelpwung syl2anc ) ACEIDFIBCDJCDKLIGHBCDEFMN $.
   $}
 
   ${
@@ -39782,8 +39782,8 @@ rather than an implication (but the two are equivalent by ~ bm1.3ii ),
     ifexd.2 $e |- ( ph -> B e. W ) $.
     $( Existence of a conditional class (deduction form).  (Contributed by BJ,
        15-Aug-2024.) $)
-    ifexd $p |- ( ph -> if ( ph , A , B ) e. _V ) $=
-      ( cif cun cpw ifelpwund elexd ) AABCHBCIJABCDEFGKL $.
+    ifexd $p |- ( ph -> if ( ps , A , B ) e. _V ) $=
+      ( cif cun cpw ifelpwund elexd ) ABCDICDJKABCDEFGHLM $.
   $}
 
 
diff --git a/set.mm b/set.mm
index 5ed5a36cc..a7a01d5e4 100644
--- a/set.mm
+++ b/set.mm
@@ -52397,17 +52397,39 @@ 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.  (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 +52443,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.) $)