Skip to content

Commit

Permalink
Add exel (from mathbox sn-el), exex, exneq (from proof of dtru), and …
Browse files Browse the repository at this point in the history 
…update dtru and comments.
  • Loading branch information
benoit.jubin committed Jan 2, 2025
1 parent acb76a5 commit 13cba53
Show file tree
Hide file tree
Showing 2 changed files with 95 additions and 69 deletions.
8 changes: 4 additions & 4 deletions discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down Expand Up @@ -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).
Expand Down
156 changes: 91 additions & 65 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -51077,18 +51077,91 @@ 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,
3-Apr-2019.) $)
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 ,
Expand All @@ -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
Expand Down Expand Up @@ -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 ) $.
Expand Down Expand Up @@ -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'; $)
$}

${
Expand Down

0 comments on commit 13cba53

Please sign in to comment.