From 13cba53463c62f41fe8a7fa4f7dd36399707ab1b Mon Sep 17 00:00:00 2001
From: "benoit.jubin" <>
Date: Thu, 2 Jan 2025 01:35:51 +0100
Subject: [PATCH] Add exel (from mathbox sn-el), exex, exneq (from proof of
 dtru), and update dtru and comments.

---
 discouraged |   8 +--
 set.mm      | 156 ++++++++++++++++++++++++++++++----------------------
 2 files changed, 95 insertions(+), 69 deletions(-)

diff --git a/discouraged b/discouraged
index 4c2889c988..56d19308a0 100644
--- a/discouraged
+++ b/discouraged
@@ -14872,7 +14872,6 @@ New usage of "bj-csbsnlem" is discouraged (1 uses).
 New usage of "bj-currypeirce" is discouraged (0 uses).
 New usage of "bj-denot" is discouraged (0 uses).
 New usage of "bj-dfid2ALT" is discouraged (0 uses).
-New usage of "bj-dtru" is discouraged (0 uses).
 New usage of "bj-elabd2ALT" is discouraged (0 uses).
 New usage of "bj-elissetALT" is discouraged (0 uses).
 New usage of "bj-equsalhv" is discouraged (0 uses).
@@ -16258,6 +16257,7 @@ New usage of "drsb1" is discouraged (3 uses).
 New usage of "dsndx" is discouraged (20 uses).
 New usage of "dtruALT" is discouraged (0 uses).
 New usage of "dtruALT2" is discouraged (6 uses).
+New usage of "dtruOLD" is discouraged (0 uses).
 New usage of "dtrucor2" is discouraged (0 uses).
 New usage of "dummylink" is discouraged (0 uses).
 New usage of "dvadiaN" is discouraged (1 uses).
@@ -19131,7 +19131,7 @@ New usage of "smfval" is discouraged (17 uses).
 New usage of "smgrpassOLD" is discouraged (1 uses).
 New usage of "smgrpismgmOLD" is discouraged (1 uses).
 New usage of "smgrpmgm" is discouraged (1 uses).
-New usage of "sn-elALT2" is discouraged (0 uses).
+New usage of "sn-exelALT" is discouraged (0 uses).
 New usage of "sn-wcdeq" is discouraged (0 uses).
 New usage of "snatpsubN" is discouraged (3 uses).
 New usage of "snelpwrVD" is discouraged (0 uses).
@@ -19905,7 +19905,6 @@ Proof modification of "bj-dfnnf3" is discouraged (34 steps).
 Proof modification of "bj-disj2r" is discouraged (88 steps).
 Proof modification of "bj-disjsn01" is discouraged (18 steps).
 Proof modification of "bj-drnf2v" is discouraged (10 steps).
-Proof modification of "bj-dtru" is discouraged (146 steps).
 Proof modification of "bj-dtrucor2v" is discouraged (31 steps).
 Proof modification of "bj-dvelimdv" is discouraged (64 steps).
 Proof modification of "bj-dvelimdv1" is discouraged (63 steps).
@@ -20204,6 +20203,7 @@ Proof modification of "drnfc2" is discouraged (59 steps).
 Proof modification of "drnfc2OLD" is discouraged (52 steps).
 Proof modification of "dtruALT" is discouraged (79 steps).
 Proof modification of "dtruALT2" is discouraged (161 steps).
+Proof modification of "dtruOLD" is discouraged (157 steps).
 Proof modification of "dummylink" is discouraged (1 steps).
 Proof modification of "dveel2ALT" is discouraged (22 steps).
 Proof modification of "dveeq1-o" is discouraged (20 steps).
@@ -21282,7 +21282,7 @@ Proof modification of "slotsbhcdifOLD" is discouraged (96 steps).
 Proof modification of "smgrpassOLD" is discouraged (54 steps).
 Proof modification of "smgrpismgmOLD" is discouraged (22 steps).
 Proof modification of "sn-00id" is discouraged (50 steps).
-Proof modification of "sn-elALT2" is discouraged (52 steps).
+Proof modification of "sn-exelALT" is discouraged (52 steps).
 Proof modification of "snelpwrVD" is discouraged (37 steps).
 Proof modification of "snex" is discouraged (64 steps).
 Proof modification of "snexALT" is discouraged (48 steps).
diff --git a/set.mm b/set.mm
index 593630312a..e593e07ad2 100644
--- a/set.mm
+++ b/set.mm
@@ -50271,10 +50271,10 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc]
   ${
     $d w x y z $.
     $( Alternate proof of ~ dtru using ~ ax-pow instead of ~ ax-pr .
-       (Contributed by NM, 7-Nov-2006.)  Avoid ~ ax-13 .  (Revised by Gino
-       Giotto, 5-Sep-2023.)  Avoid ~ ax-12 .  (Revised by Rohan Ridenour,
-       9-Oct-2024.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
+       (Contributed by NM, 7-Nov-2006.)  Avoid ~ ax-13 .  (Revised by BJ,
+       31-May-2019.)  (Revised by Gino Giotto, 5-Sep-2023.)  Avoid ~ ax-12 .
+       (Revised by Rohan Ridenour, 9-Oct-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
     dtruALT2 $p |- -. A. x x = y $=
       ( vw vz cv wceq wn wex wal wel wcel elALT2 ax-nul elequ1 notbid spw ax7v1
       wa con3d spimevw eximii exdistrv mpbir2an ax9v2 com12 con3dimp 2eximi weq
@@ -51077,6 +51077,78 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with
       ERUGBPEABUBBSTUFRUGAPEABUCASTUD $.
   $}
 
+  ${
+    $d x y z $.
+    $( There exist two sets, one a member of the other.
+
+       This theorem looks similar to ~ el , but its meaning is different.  It
+       only depends on the axioms ~ ax-mp to ~ ax-4 , ~ ax-6 , and ~ ax-pr .
+       This theorem does not exclude that these two sets could actually be one
+       single set containing itself.  That two different sets exist is proved
+       by ~ exex .  (Contributed by SN, 23-Dec-2024.) $)
+    exel $p |- E. y E. x x e. y $=
+      ( vz weq wo wel wi wal wex ax-pr ax6ev pm2.07 eximii exim mpi ) ACDZPEZAB
+      FZGAHZRAIZBCCBAJSQAITPQAACKPLMQRANOM $.
+    $( $j usage 'exel' avoids 'ax-5' 'ax-7' 'ax-8' 'ax-9' 'ax-10 'ax-11'
+       'ax-12' 'ax-13''ax-ext' 'ax-sep' 'ax-nul' 'ax-pow'; $)
+  $}
+
+  ${
+    $d x y z $.
+    $( There exist two different sets.  (Contributed by NM, 7-Nov-2006.)  Avoid
+       ~ ax-13 .  (Revised by BJ, 31-May-2019.)  (Revised by Gino Giotto,
+       5-Sep-2023.)  Avoid ~ ax-8 .  (Revised by SN, 21-Sep-2023.)  Avoid
+       ~ ax-12 .  (Revised by Rohan Ridenour, 9-Oct-2024.)  Use ~ ax-pr instead
+       of ~ ax-pow .  (Revised by BTernaryTau, 3-Dec-2024.)  Extract this
+       result from the proof from ~ dtru .  (Revised by BJ, 2-Jan-2025.) $)
+    exex $p |- E. x E. y -. x = y $=
+      ( vz wel wex wn wal wa weq ax-nul exdistrv mpbir2an wi ax9v1 eximdv df-ex
+      exel syl6ib imnan sylib con2i 2eximi ax-mp ) CADZCEZCBDZFCGZHZBEAEZABIZFZ
+      BEAEUIUEAEUGBECAQBCJUEUGABKLUHUKABUJUHUJUEUGFZMUHFUJUEUFCEULUJUDUFCABCNOU
+      FCPRUEUGSTUAUBUC $.
+    $( $j usage 'exex' avoids 'ax-7' 'ax-8' 'ax-10 'ax-11' 'ax-12' 'ax-13'
+       'ax-ext' 'ax-sep' 'ax-pow'; $)
+  $}
+
+  ${
+    $d w x y z $.
+    $( Given any set (the " ` y ` " in the statement), there exists a set not
+       equal to it.
+
+       The same statement without disjoint variable condition is false, since
+       we do not have ` E. x -. x = x ` .  This theorem is proved directly from
+       set theory axioms (no class definitions) and does not depend on
+       ~ ax-ext , ~ ax-sep , or ~ ax-pow nor auxiliary logical axiom schemes
+       ~ ax-10 to ~ ax-13 .  See ~ dtruALT for a shorter proof using more
+       axioms, and ~ dtruALT2 for a proof using ~ ax-pow instead of ~ ax-pr .
+       (Contributed by NM, 7-Nov-2006.)  Avoid ~ ax-13 .  (Revised by BJ,
+       31-May-2019.)  (Revised by Gino Giotto, 5-Sep-2023.)  Avoid ~ ax-8 .
+       (Revised by SN, 21-Sep-2023.)  Avoid ~ ax-12 .  (Revised by Rohan
+       Ridenour, 9-Oct-2024.)  Use ~ ax-pr instead of ~ ax-pow .  (Revised by
+       BTernaryTau, 3-Dec-2024.)  Extract this result from the proof of
+       ~ dtru .  (Revised by BJ, 2-Jan-2025.) $)
+    exneq $p |- E. x -. x = y $=
+      ( vz vw weq wn wex exex wi equeuclr con3d ax7v1 spimevw syl6 a1d exlimivv
+      pm2.61i ax-mp ) CDEZFZDGCGABEZFZAGZCDHTUCCDDBEZTUCIUDTCBEZFZUCUDUESDCBJKU
+      FUBACACEUAUEACBLKMNUDFZUCTUGUBADADEUAUDADBLKMOQPR $.
+    $( $j usage 'exneq' avoids 'ax-8' 'ax-10 'ax-11' 'ax-12' 'ax-13' 'ax-ext'
+       'ax-sep' 'ax-pow' 'df-clab' 'df-cleq' 'df-clel'; $)
+  $}
+
+  ${
+    $d x y $.
+    $( Given any set (the " ` y ` " in the statement), not all sets are equal
+       to it.  The same statement without disjoint variable condition is false
+       since it contradicts ~ stdpc6 .  The same comments and revision history
+       concerning axiom usage as in ~ exneq apply.  (Contributed by NM,
+       7-Nov-2006.)  Extract ~ exneq as an intermediate result.  (Revised by
+       BJ, 2-Jan-2025.) $)
+    dtru $p |- -. A. x x = y $=
+      ( weq wn wex wal exneq exnal mpbi ) ABCZDAEJAFDABGJAHI $.
+    $( $j usage 'dtru' avoids 'ax-8' 'ax-10 'ax-11' 'ax-12' 'ax-13' 'ax-ext'
+       'ax-sep' 'ax-pow' 'df-clab' 'df-cleq' 'df-clel'; $)
+  $}
+
   ${
     $d x A $.
     $( If a class is a set, then it is a member of a set.  (Contributed by BJ,
@@ -51084,11 +51156,12 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with
     sels $p |- ( A e. V -> E. x A e. x ) $=
       ( wcel csn cv wex snidg snex eleq2 spcev syl ) BCDBBEZDZBAFZDZAGBCHPNAMBI
       OMBJKL $.
+    $( $j usage 'sels' avoids 'ax-pow'; $)
   $}
 
   ${
     $d x y z $.
-    $( Every set is an element of some other set.  See ~ elALT for a shorter
+    $( Any set is an element of some other set.  See ~ elALT for a shorter
        proof using more axioms, and see ~ elALT2 for a proof that uses ~ ax-9
        and ~ ax-pow instead of ~ ax-pr .  (Contributed by NM, 4-Jan-2002.)
        (Proof shortened by Andrew Salmon, 25-Jul-2011.)  Avoid ~ ax-9 ,
@@ -51108,36 +51181,24 @@ That theorem bundles the theorems ( ` |- E. x ( x = y -> z e. x ) ` with
     elALT $p |- E. y x e. y $=
       ( cv csn wcel wex vex snid snex eleq2 spcev ax-mp ) ACZMDZEZMBCZEZBFMAGHQ
       OBNMIPNMJKL $.
+    $( $j usage 'elALT' avoids 'ax-pow'; $)
   $}
 
   ${
     $d w x y z $.
-    $( At least two sets exist (or in terms of first-order logic, the universe
-       of discourse has two or more objects).  Note that we may not substitute
-       the same variable for both ` x ` and ` y ` (as indicated by the distinct
-       variable requirement), for otherwise we would contradict ~ stdpc6 .
-
-       This theorem is proved directly from set theory axioms (no set theory
-       definitions) and does not use ~ ax-ext , ~ ax-sep , or ~ ax-pow .  See
-       ~ dtruALT for a shorter proof using these axioms, and see ~ dtruALT2 for
-       a proof that uses ~ ax-pow instead of ~ ax-pr .
-
-       The proof makes use of dummy variables ` z ` and ` w ` which do not
-       appear in the final theorem.  They must be distinct from each other and
-       from ` x ` and ` y ` .  In other words, if we were to substitute ` x `
-       for ` z ` throughout the proof, the proof would fail.  (Contributed by
-       NM, 7-Nov-2006.)  Avoid ~ ax-13 .  (Revised by Gino Giotto, 5-Sep-2023.)
-       Avoid ~ ax-12 .  (Revised by Rohan Ridenour, 9-Oct-2024.)  Use ~ ax-pr
-       instead of ~ ax-pow .  (Revised by BTernaryTau, 3-Dec-2024.) $)
-    dtru $p |- -. A. x x = y $=
+    $( Obsolete proof of ~ dtru as of 01-Jan-2025.  (Contributed by NM,
+       7-Nov-2006.)  Avoid ~ ax-13 .  (Revised by BJ, 31-May-2019.)  (Revised
+       by Gino Giotto, 5-Sep-2023.)  Avoid ~ ax-12 .  (Revised by Rohan
+       Ridenour, 9-Oct-2024.)  Use ~ ax-pr instead of ~ ax-pow .  (Revised by
+       BTernaryTau, 3-Dec-2024.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    dtruOLD $p |- -. A. x x = y $=
       ( vw vz weq wn wex wal wel wa el ax-nul elequ1 notbid spw eximii exdistrv
       ax7v1 con3d spimevw mpbir2an ax9v2 con3dimp 2eximi equequ2 syl6bi pm2.61i
       com12 wi a1d exlimivv mp2b exnal mpbi ) ABEZFZAGZUOAHFACIZADIZFZJZDGCGZCD
       EZFZDGCGUQVBURCGUTDGACKUTAHUTDDALUTCDIZFACACEZUSVEACDMNOPURUTCDQUAVAVDCDU
       RVCUSVCURUSCDAUBUHUCUDVDUQCDDBEZVDUQUIVGVDCBEZFZUQVGVCVHDBCUENVIUPACVFUOV
       HACBRSTUFVGFZUQVDVJUPADADEUOVGADBRSTUJUGUKULUOAUMUN $.
-    $( $j usage 'dtru' avoids 'ax-10 'ax-11' 'ax-12' 'ax-13' 'ax-ext' 'ax-sep'
-       'ax-pow'; $)
   $}
 
   $( A singleton of a set belongs to the power class of a class containing the
@@ -553001,25 +553062,6 @@ universe has at least two objects (see ~ dtru ).  (Contributed by BJ,
       ( cv cab wcel hbab1 nf5i ) CDABEFBABCGH $.
   $}
 
-  ${
-    $d w x y z $.
-    $( Remove dependency on ~ ax-13 from ~ dtru .  (Contributed by BJ,
-       31-May-2019.)
-
-       TODO:  This predates the removal of ~ ax-13 in ~ dtru .  But actually,
-       ~ sn-dtru is better than either, so move it to Main with ~ sn-el (and
-       determine whether ~ bj-dtru should be kept as ALT or deleted).
-
-       (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    bj-dtru $p |- -. A. x x = y $=
-      ( vw vz weq wn wex wal wel wa el ax-nul sp eximii exdistrv mpbir2an ax-mp
-      ax7 con3d spimevw ax9 com12 con3dimp 2eximi equequ2 notbid syl6bi pm2.61i
-      wi a1d exlimivv exnal mpbi ) ABEZFZAGZUNAHFCDEZFZDGCGZUPACIZADIZFZJZDGCGZ
-      USVDUTCGVBDGACKVBAHVBDDALVBAMNUTVBCDOPVCURCDUTUQVAUQUTVACDAUAUBUCUDQURUPC
-      DDBEZURUPUIVEURCBEZFZUPVEUQVFDBCUEUFVGUOACACEUNVFACBRSTUGVEFZUPURVHUOADAD
-      EUNVEADBRSTUJUHUKQUNAULUM $.
-  $}
-
   ${
     $d x y $.
     bj-dtrucor2v.1 $e |- ( x = y -> x =/= y ) $.
@@ -654099,30 +654141,14 @@ D Fn ( I ... ( M - 1 ) ) /\
 
   ${
     $d w x y z $.
-    $( A version of ~ el with an inner existential quantifier on ` x ` , which
-       only uses ~ ax-mp to ~ ax-4 , ~ ax-6 , and ~ ax-pr .  (Contributed by
-       SN, 23-Dec-2024.) $)
-    sn-el $p |- E. y E. x x e. y $=
-      ( vz weq wo wel wi wal wex ax-pr ax6ev pm2.07 eximii exim mpi ) ACDZPEZAB
-      FZGAHZRAIZBCCBAJSQAITPQAACKPLMQRANOM $.
-
-    $( A version of ~ elALT2 with an inner existential quantifier on ` x ` ,
-       which avoids ~ ax-8 .  (Contributed by SN, 18-Sep-2023.)
+    $( Alternate proof of ~ exel , avoiding ~ ax-pr but requiring ~ ax-5 ,
+       ~ ax-9 , and ~ ax-pow .  (Contributed by SN, 18-Sep-2023.)
        (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    sn-elALT2 $p |- E. y E. x x e. y $=
+    sn-exelALT $p |- E. y E. x x e. y $=
       ( vw vz wel wi wal wex ax-pow weq ax6ev ax9v1 alrimiv eximii exim mpi ) C
       AECDEFZCGZABEZFAGZSAHZBDBACITRAHUAADJZRAADKUBQCADCLMNRSAOPN $.
-    $( $j usage 'sn-elALT2' avoids 'ax-8'; $)
-
-    $( ~ dtru without ~ ax-8 .  (Contributed by SN, 21-Sep-2023.) $)
-    sn-dtru $p |- -. A. x x = y $=
-      ( vw vz weq wn wex wal wel wa sn-el ax-nul exdistrv mpbir2an ax9v1 eximdv
-      wi con3d ax7v1 spimevw df-ex syl6ib imnan sylib con2i 2eximi equeuclr a1d
-      syl6 pm2.61i exlimivv mp2b exnal mpbi ) ABEZFZAGZUOAHFACIZAGZADIZFAHZJZDG
-      CGZCDEZFZDGCGUQVCUSCGVADGACKDALUSVACDMNVBVECDVDVBVDUSVAFZQVBFVDUSUTAGVFVD
-      URUTACDAOPUTAUAUBUSVAUCUDUEUFVEUQCDDBEZVEUQQVGVECBEZFZUQVGVHVDDCBUGRVIUPA
-      CACEUOVHACBSRTUIVGFZUQVEVJUPADADEUOVGADBSRTUHUJUKULUOAUMUN $.
-    $( $j usage 'sn-dtru' avoids 'ax-8'; $)
+    $( $j usage 'sn-exelALT' avoids 'ax-7' 'ax-8' 'ax-ext' 'ax-sep' 'ax-nul'
+       'ax-pr'; $)
   $}
 
   ${