Skip to content

Commit

Permalink
Reduce ax-un usage (#4284)
Browse files Browse the repository at this point in the history 
* Prove breng

* Shorten bren

* Revise en0

* Revise ensn1

* Revise en1

* Prove eqsnuniex

* Revise en1b

* Revise en1uniel

* Revise en2sn

* Fix tag for bren
  • Loading branch information
@BTernaryTau
BTernaryTau authored Oct 16, 2024
1 parent 8ad8596 commit 4c826c5
Show file tree
Hide file tree
Showing 2 changed files with 126 additions and 14 deletions.
18 changes: 16 additions & 2 deletions discouraged
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14805,6 +14805,7 @@ New usage of "bralnfn" is discouraged (2 uses).
New usage of "bramul" is discouraged (1 uses).
New usage of "branmfn" is discouraged (1 uses).
New usage of "braval" is discouraged (10 uses).
New usage of "brenOLD" is discouraged (0 uses).
New usage of "brfi1indALT" is discouraged (0 uses).
New usage of "c-bnj14" is discouraged (131 uses).
New usage of "c-bnj18" is discouraged (59 uses).
Expand Down Expand Up @@ -16004,7 +16005,12 @@ New usage of "elunirnALT" is discouraged (0 uses).
New usage of "elunop" is discouraged (7 uses).
New usage of "elunop2" is discouraged (0 uses).
New usage of "en0OLD" is discouraged (0 uses).
New usage of "en0OLDOLD" is discouraged (0 uses).
New usage of "en1OLD" is discouraged (0 uses).
New usage of "en1bOLD" is discouraged (0 uses).
New usage of "en1unielOLD" is discouraged (0 uses).
New usage of "en2snOLD" is discouraged (0 uses).
New usage of "en2snOLDOLD" is discouraged (0 uses).
New usage of "en3lpVD" is discouraged (0 uses).
New usage of "en3lplem1VD" is discouraged (1 uses).
New usage of "en3lplem2VD" is discouraged (1 uses).
Expand All @@ -16019,6 +16025,7 @@ New usage of "enrbreq" is discouraged (3 uses).
New usage of "enreceq" is discouraged (9 uses).
New usage of "enrer" is discouraged (8 uses).
New usage of "enrex" is discouraged (9 uses).
New usage of "ensn1OLD" is discouraged (0 uses).
New usage of "ensucne0OLD" is discouraged (0 uses).
New usage of "eq0ALT" is discouraged (0 uses).
New usage of "eq0OLDOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -19240,6 +19247,7 @@ Proof modification of "bj-xpima1snALT" is discouraged (25 steps).
Proof modification of "bj-xpima2sn" is discouraged (23 steps).
Proof modification of "bj-xpnzex" is discouraged (71 steps).
Proof modification of "bj-zfauscl" is discouraged (65 steps).
Proof modification of "brenOLD" is discouraged (130 steps).
Proof modification of "brfi1indALT" is discouraged (741 steps).
Proof modification of "brfvidRP" is discouraged (93 steps).
Proof modification of "c0exALT" is discouraged (15 steps).
Expand Down Expand Up @@ -19573,13 +19581,19 @@ Proof modification of "elpwi2OLD" is discouraged (21 steps).
Proof modification of "elrabiOLD" is discouraged (55 steps).
Proof modification of "elrefsymrels3" is discouraged (65 steps).
Proof modification of "elunirnALT" is discouraged (38 steps).
Proof modification of "en0OLD" is discouraged (62 steps).
Proof modification of "en2snOLD" is discouraged (35 steps).
Proof modification of "en0OLD" is discouraged (86 steps).
Proof modification of "en0OLDOLD" is discouraged (62 steps).
Proof modification of "en1OLD" is discouraged (164 steps).
Proof modification of "en1bOLD" is discouraged (83 steps).
Proof modification of "en1unielOLD" is discouraged (39 steps).
Proof modification of "en2snOLD" is discouraged (56 steps).
Proof modification of "en2snOLDOLD" is discouraged (35 steps).
Proof modification of "en3lpVD" is discouraged (147 steps).
Proof modification of "en3lplem1VD" is discouraged (95 steps).
Proof modification of "en3lplem2VD" is discouraged (267 steps).
Proof modification of "enfiOLD" is discouraged (42 steps).
Proof modification of "enfiiOLD" is discouraged (14 steps).
Proof modification of "ensn1OLD" is discouraged (47 steps).
Proof modification of "ensucne0OLD" is discouraged (82 steps).
Proof modification of "eq0ALT" is discouraged (31 steps).
Proof modification of "eq0OLDOLD" is discouraged (6 steps).
Expand Down
122 changes: 110 additions & 12 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49590,6 +49590,13 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc]
unisn un0 uneq1i 3eqtri ) ABCZDZEZBAEZFZUBBFUBUASAFZEZSEZUBFUCTSFZEUAUFFZUE
UATSGUDUGUGASFUDASHASIJKUHUABFUAUFBUABLOZMUAPJNSAGUFBUBUIQRBUBIUBPR $.

$( If a class is equal to the singleton of its union, then its union exists.
(Contributed by BTernaryTau, 24-Sep-2024.) $)
eqsnuniex $p |- ( A = { U. A } -> U. A e. _V ) $=
( cuni csn wceq c0 wn wcel wa unieq uni0 eqtrdi sylan9eq sneqd 0inp0 adantl
cvv pm2.65da snprc bicomi con2bii sylibr ) AABZCZDZUCEDZFUBPGZUDUEUCECDZUDU
EHUBEUDUEUBUCBZEAUCIUEUHEBEUCEIJKLMUEUGFUDUCNOQUEUFUFFUEUBRSTUA $.

${
$d x A $.
$( An indexed intersection of the empty set, with a nonempty index set, is
Expand Down Expand Up @@ -87199,8 +87206,26 @@ the first case of his notation (simple exponentiation) and subscript it

${
$d f x y A $. $d f x y B $. $d y C $.
$( Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) $)
$( Equinumerosity relation. This variation of ~ bren does not require the
Axiom of Union. (Contributed by BTernaryTau, 23-Sep-2024.) $)
breng $p |- ( ( A e. V /\ B e. W ) ->
( A ~~ B <-> E. f f : A -1-1-onto-> B ) ) $=
( vx vy cv wf1o wex cen wceq f1oeq2 exbidv f1oeq3 df-en brabg ) FHZGHZCHZ
IZCJASTIZCJABTIZCJFGABDEKRALUAUBCRASTMNSBLUBUCCSBATONFGCPQ $.
$( $j usage 'breng' avoids 'ax-un'; $)

$( Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) (Proof
shortened by BTernaryTau, 23-Sep-2024.) $)
bren $p |- ( A ~~ B <-> E. f f : A -1-1-onto-> B ) $=
( cen wbr cvv wcel wa wf1o wex encv wfn f1ofn cdm fndm vex dmex eqeltrrdi
cv syl crn wfo wceq f1ofo forn rnex jca exlimiv breng pm5.21nii ) ABDEAFG
ZBFGZHZABCSZIZCJABKUOUMCUOUKULUOUNALZUKABUNMUPAUNNFAUNOUNCPZQRTUOBUNUAZFU
OABUNUBURBUCABUNUDABUNUETUNUQUFRUGUHABCFFUIUJ $.

$( Obsolete version of ~ bren as of 23-Sep-2024. (Contributed by NM,
15-Jun-1998.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
brenOLD $p |- ( A ~~ B <-> E. f f : A -1-1-onto-> B ) $=
( vx vy cen wbr cvv wcel wa cv wf1o wex encv wfn f1ofn eqeltrrdi syl wceq
exbidv cdm fndm vex dmex crn wfo f1ofo forn rnex jca exlimiv f1oeq2 df-en
f1oeq3 brabg pm5.21nii ) ABFGAHIZBHIZJZABCKZLZCMZABNVAUSCVAUQURVAUTAOZUQA
Expand Down Expand Up @@ -87667,32 +87692,59 @@ the first case of his notation (simple exponentiation) and subscript it
$d A f $.
$( The empty set is equinumerous only to itself. Exercise 1 of
[TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid
~ ax-pow . (Revised by BTernaryTau, 31-Jul-2024.) $)
~ ax-pow . (Revised by BTernaryTau, 31-Jul-2024.) Avoid ~ ax-un .
(Revised by BTernaryTau, 23-Sep-2024.) $)
en0 $p |- ( A ~~ (/) <-> A = (/) ) $=
( vf c0 cen wbr wceq cv wf1o wex cvv wcel wa wb encv breng syl ibi f1ocnv
ccnv 0ex f1o00 simprbi exlimiv f1oeq1 ceqsexv2d mp2an mpbir mpbiri impbii
f1o0 breq1 ) ACDEZACFZULACBGZHZBIZUMULUPULAJKCJKZLULUPMACNACBJJOPQUOUMBUO
CAUNSZHZUMACUNRUSURCFUMAURUAUBPUCPUMULCCDEZUTCCUNHZBIZVACCCHBCTCCUNCUDUJU
EUQUQUTVBMTTCCBJJOUFUGACCDUKUHUI $.
$( $j usage 'en0' avoids 'ax-pow' 'ax-un'; $)
$}

${
$d A f $.
$( Obsolete version of ~ en0 as of 23-Sep-2024. (Contributed by NM,
27-May-1998.) Avoid ~ ax-pow . (Revised by BTernaryTau, 31-Jul-2024.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
en0OLD $p |- ( A ~~ (/) <-> A = (/) ) $=
( vf c0 cen wbr wceq cv wf1o wex bren ccnv f1ocnv f1o00 simprbi syl sylbi
exlimiv 0ex f1oeq1 f1o0 ceqsexv2d mpbir breq1 mpbiri impbii ) ACDEZACFZUF
ACBGZHZBIUGACBJUIUGBUICAUHKZHZUGACUHLUKUJCFUGAUJMNOQPUGUFCCDEZULCCUHHZBIU
MCCCHBCRCCUHCSTUACCBJUBACCDUCUDUE $.
$( $j usage 'en0' avoids 'ax-pow'; $)
$}

${
$d f A $.
$( Obsolete version of ~ en0 as of 31-Jul-2024. (Contributed by NM,
27-May-1998.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
en0OLD $p |- ( A ~~ (/) <-> A = (/) ) $=
en0OLDOLD $p |- ( A ~~ (/) <-> A = (/) ) $=
( vf c0 cen wbr wceq cv wf1o wex bren ccnv f1ocnv f1o00 simprbi syl sylbi
exlimiv 0ex enref breq1 mpbiri impbii ) ACDEZACFZUCACBGZHZBIUDACBJUFUDBUF
CAUEKZHZUDACUELUHUGCFUDAUGMNOQPUDUCCCDECRSACCDTUAUB $.
$}

${
$d f A $.
$d A f $.
ensn1.1 $e |- A e. _V $.
$( A singleton is equinumerous to ordinal one. (Contributed by NM,
4-Nov-2002.) $)
4-Nov-2002.) Avoid ~ ax-un . (Revised by BTernaryTau, 23-Sep-2024.) $)
ensn1 $p |- { A } ~~ 1o $=
( vf csn c0 c1o cen wbr wf1o wex cop snex f1oeq1 0ex f1osn ceqsexv2d wcel
cv cvv wb breng mp2an mpbir df1o2 breqtrri ) ADZEDZFGUFUGGHZUFUGCRZIZCJZU
JUFUGAEKZDZICUMULLUFUGUIUMMAEBNOPUFSQUGSQUHUKTALELUFUGCSSUAUBUCUDUE $.
$( $j usage 'ensn1' avoids 'ax-un'; $)
$}

${
$d f A $.
ensn1OLD.1 $e |- A e. _V $.
$( Obsolete version of ~ ensn1 as of 23-Sep-2024. (Contributed by NM,
4-Nov-2002.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
ensn1OLD $p |- { A } ~~ 1o $=
( vf csn c0 c1o cen wbr wf1o wex cop snex f1oeq1 0ex f1osn ceqsexv2d bren
cv mpbir df1o2 breqtrri ) ADZEDZFGUBUCGHUBUCCRZIZCJUEUBUCAEKZDZICUGUFLUBU
CUDUGMAEBNOPUBUCCQSTUA $.
Expand All @@ -87714,8 +87766,23 @@ the first case of his notation (simple exponentiation) and subscript it
${
$d x f y A $. $d y ph $.
$( A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by NM, 25-Jul-2004.) $)
(Contributed by NM, 25-Jul-2004.) Avoid ~ ax-un . (Revised by
BTernaryTau, 23-Sep-2024.) $)
en1 $p |- ( A ~~ 1o <-> E. x A = { x } ) $=
( vf c1o cen wbr cv csn wceq wex c0 wf1o df1o2 breq2i cvv syl crn exlimiv
wcel 0ex wa wb encv breng ibi sylbi ccnv cfv f1ocnv wfo f1ofo forn cop wf
f1of fsn2 simprbi rneqd rnsnop eqtrdi eqtr3d fvex sneq eqeq2d spcev ensn1
3syl vex breq1 mpbiri impbii ) BDEFZBAGZHZIZAJZVLBKHZCGZLZCJZVPVLBVQEFZVT
DVQBEMNWAVTWABOSVQOSUAWAVTUBBVQUCBVQCOOUDPUEUFVSVPCVSVQBVRUGZLZBKWBUHZHZI
ZVPBVQVRUIWCWBQZBWEWCVQBWBUJWGBIVQBWBUKVQBWBULPWCWGKWDUMHZQWEWCWBWHWCVQBW
BUNZWBWHIZVQBWBUOWIWDBSWJKBWBTUPUQPURKWDTUSUTVAVOWFAWDKWBVBVMWDIVNWEBVMWD
VCVDVEVGRPVOVLAVOVLVNDEFVMAVHVFBVNDEVIVJRVK $.
$( $j usage 'en1' avoids 'ax-un'; $)

$( Obsolete version of ~ en1 as of 23-Sep-2024. (Contributed by NM,
25-Jul-2004.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
en1OLD $p |- ( A ~~ 1o <-> E. x A = { x } ) $=
( vf c1o cen wbr cv csn wceq wex wf1o df1o2 breq2i bren bitri crn syl 0ex
c0 exlimiv ccnv cfv f1ocnv wfo f1ofo forn wf f1of wcel fsn2 simprbi rneqd
rnsnop eqtrdi eqtr3d fvex sneq eqeq2d spcev 3syl sylbi ensn1 breq1 mpbiri
Expand All @@ -87725,8 +87792,19 @@ the first case of his notation (simple exponentiation) and subscript it
VKWAAVSSVQUPVIVSIVJVTBVIVSUQURUSUTTVAVKVHAVKVHVJDEFVIAVFVBBVJDEVCVDTVG $.

$( A set is equinumerous to ordinal one iff it is a singleton.
(Contributed by Mario Carneiro, 17-Jan-2015.) $)
(Contributed by Mario Carneiro, 17-Jan-2015.) Avoid ~ ax-un . (Revised
by BTernaryTau, 24-Sep-2024.) $)
en1b $p |- ( A ~~ 1o <-> A = { U. A } ) $=
( vx c1o cen wbr cuni csn wceq cv wex en1 id unieq vex unisn eqtrdi sneqd
eqtr4d exlimiv cvv sylbi wcel eqsnuniex ensn1g syl eqbrtrd impbii ) ACDEZ
AAFZGZHZUHABIZGZHZBJUKBAKUNUKBUNAUMUJUNLUNUIULUNUIUMFULAUMMULBNOPQRSUAUKA
UJCDUKLUKUITUBUJCDEAUCUITUDUEUFUG $.
$( $j usage 'en1b' avoids 'ax-un'; $)

$( Obsolete version of ~ en1b as of 24-Sep-2024. (Contributed by Mario
Carneiro, 17-Jan-2015.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
en1bOLD $p |- ( A ~~ 1o <-> A = { U. A } ) $=
( vx c1o cen wbr cuni csn wceq cv wex en1 id unieq vex unisn eqtrdi sneqd
eqtr4d exlimiv cvv sylbi wcel snex eqeltrdi uniexd ensn1g eqbrtrd impbii
syl ) ACDEZAAFZGZHZUJABIZGZHZBJUMBAKUPUMBUPAUOULUPLUPUKUNUPUKUOFUNAUOMUNB
Expand All @@ -87752,8 +87830,16 @@ the first case of his notation (simple exponentiation) and subscript it
$}

$( A singleton contains its sole element. (Contributed by Stefan O'Rear,
16-Aug-2015.) $)
16-Aug-2015.) Avoid ~ ax-un . (Revised by BTernaryTau, 24-Sep-2024.) $)
en1uniel $p |- ( S ~~ 1o -> U. S e. S ) $=
( c1o cen wbr cuni csn wcel wceq en1b eqsnuniex sylbi snidg biimpi eleqtrrd
cvv syl ) ABCDZAEZRFZAQROGZRSGQASHZTAIZAJKROLPQUAUBMN $.
$( $j usage 'en1uniel' avoids 'ax-un'; $)

$( Obsolete version of ~ en1uniel as of 24-Sep-2024. (Contributed by Stefan
O'Rear, 16-Aug-2015.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
en1unielOLD $p |- ( S ~~ 1o -> U. S e. S ) $=
( c1o cen wbr cuni csn cvv wcel relen brrelex1i uniexg snidg 3syl wceq en1b
biimpi eleqtrrd ) ABCDZAEZSFZARAGHSGHSTHABCIJAGKSGLMRATNAOPQ $.

Expand Down Expand Up @@ -87888,20 +87974,32 @@ the first case of his notation (simple exponentiation) and subscript it
${
$d A f $. $d B f $.
$( Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.)
Avoid ~ ax-pow . (Revised by BTernaryTau, 31-Jul-2024.) $)
Avoid ~ ax-pow . (Revised by BTernaryTau, 31-Jul-2024.) Avoid
~ ax-un . (Revised by BTernaryTau, 25-Sep-2024.) $)
en2sn $p |- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } ) $=
( vf wcel wa csn wf1o wex cen wbr cop cvv snex f1osng f1oeq1 spcegv mpsyl
cv wb breng mp2an sylibr ) ACFBDFGZAHZBHZETZIZEJZUFUGKLZABMZHZNFUEUFUGUMI
ZUJULOABCDPUIUNEUMNUFUGUHUMQRSUFNFUGNFUKUJUAAOBOUFUGENNUBUCUD $.
$( $j usage 'en2sn' avoids 'ax-pow' 'ax-un'; $)
$}

${
$d A f $. $d B f $.
$( Obsolete version of ~ en2sn as of 25-Sep-2024. (Contributed by NM,
9-Nov-2003.) Avoid ~ ax-pow . (Revised by BTernaryTau, 31-Jul-2024.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
en2snOLD $p |- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } ) $=
( vf wcel wa csn wf1o wex cen wbr cop cvv snex f1osng f1oeq1 spcegv mpsyl
cv bren sylibr ) ACFBDFGZAHZBHZETZIZEJZUDUEKLABMZHZNFUCUDUEUJIZUHUIOABCDP
UGUKEUJNUDUEUFUJQRSUDUEEUAUB $.
$( $j usage 'en2sn' avoids 'ax-pow'; $)
$}

${
$d x y A $. $d x y B $. $d x y C $. $d x y D $.
$( Obsolete version of ~ en2sn as of 31-Jul-2024. (Contributed by NM,
9-Nov-2003.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
en2snOLD $p |- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } ) $=
en2snOLDOLD $p |- ( ( A e. C /\ B e. D ) -> { A } ~~ { B } ) $=
( wcel csn c1o cen wbr ensn1g ensymd entr syl2an ) ACEAFZGHIGBFZHINOHIBDE
ZACJPOGBDJKNGOLM $.

Expand Down

0 comments on commit 4c826c5

Please sign in to comment.