Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reduce ax-un usage #4466

Merged
merged 11 commits into from
Dec 8, 2024
Merged

Reduce ax-un usage #4466

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
84c6dbd
Prove ord1eln01
BTernaryTau Dec 1, 2024
8b726ce
Prove ord2eln012
BTernaryTau Dec 1, 2024
358e179
Prove nlim1
BTernaryTau Dec 1, 2024
2d69c6e
Prove nlim2
BTernaryTau Dec 1, 2024
279fa5a
Prove 1ellim
BTernaryTau Dec 1, 2024
0115fc6
Prove 2ellim
BTernaryTau Dec 1, 2024
c7acd26
Revise 1onn
BTernaryTau Dec 1, 2024
3cddfaf
Revise 2onn
BTernaryTau Dec 1, 2024
debba84
Prove f1cdmsn
BTernaryTau Dec 2, 2024
997629a
Revise snnen2oOLD
BTernaryTau Dec 2, 2024
c695052
Keep ALT proofs for 1onn and 2onn
BTernaryTau Dec 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14290,6 +14290,7 @@ New usage of "1nq" is discouraged (9 uses).
New usage of "1nqenq" is discouraged (1 uses).
New usage of "1oexOLD" is discouraged (0 uses).
New usage of "1onOLD" is discouraged (0 uses).
New usage of "1onnALT" is discouraged (0 uses).
New usage of "1p1e2apr1" is discouraged (0 uses).
New usage of "1p2e3ALT" is discouraged (0 uses).
New usage of "1pi" is discouraged (11 uses).
Expand Down Expand Up @@ -14331,6 +14332,7 @@ New usage of "2moex" is discouraged (1 uses).
New usage of "2moswap" is discouraged (1 uses).
New usage of "2oexOLD" is discouraged (0 uses).
New usage of "2onOLD" is discouraged (0 uses).
New usage of "2onnALT" is discouraged (0 uses).
New usage of "2pm13.193" is discouraged (3 uses).
New usage of "2pm13.193VD" is discouraged (0 uses).
New usage of "2pmaplubN" is discouraged (1 uses).
Expand Down Expand Up @@ -19097,6 +19099,7 @@ 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).
New usage of "snexALT" is discouraged (1 uses).
New usage of "snnen2oOLD" is discouraged (0 uses).
New usage of "snssiALT" is discouraged (0 uses).
New usage of "snssiALTVD" is discouraged (0 uses).
New usage of "snssl" is discouraged (0 uses).
Expand Down Expand Up @@ -19586,6 +19589,7 @@ Proof modification of "19.43OLD" is discouraged (72 steps).
Proof modification of "1div0apr" is discouraged (77 steps).
Proof modification of "1oexOLD" is discouraged (4 steps).
Proof modification of "1onOLD" is discouraged (9 steps).
Proof modification of "1onnALT" is discouraged (16 steps).
Proof modification of "1p1e2apr1" is discouraged (7 steps).
Proof modification of "1p2e3ALT" is discouraged (7 steps).
Proof modification of "1strbasOLD" is discouraged (22 steps).
Expand All @@ -19598,6 +19602,7 @@ Proof modification of "2irrexpqALT" is discouraged (90 steps).
Proof modification of "2logb9irrALT" is discouraged (141 steps).
Proof modification of "2oexOLD" is discouraged (9 steps).
Proof modification of "2onOLD" is discouraged (9 steps).
Proof modification of "2onnALT" is discouraged (16 steps).
Proof modification of "2pm13.193" is discouraged (91 steps).
Proof modification of "2pm13.193VD" is discouraged (223 steps).
Proof modification of "2ralorOLD" is discouraged (109 steps).
Expand Down Expand Up @@ -21210,6 +21215,7 @@ Proof modification of "sn-00id" is discouraged (50 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).
Proof modification of "snnen2oOLD" is discouraged (116 steps).
Proof modification of "snssiALT" is discouraged (40 steps).
Proof modification of "snssiALTVD" is discouraged (64 steps).
Proof modification of "snssl" is discouraged (18 steps).
Expand Down
125 changes: 113 additions & 12 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68516,6 +68516,19 @@ more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.)
UOUPURWFVBCVIHZWHWFWIVBWFWIEBCULUMUNUOUQ $.
$}

${
$d A x y $. $d A y z $. $d B y z $. $d F y z $.
$( If a one-to-one function with a nonempty domain has a singleton as its
codomain, its domain must also be a singleton. (Contributed by
BTernaryTau, 1-Dec-2024.) $)
f1cdmsn $p |- ( ( F : A -1-1-> { B } /\ A =/= (/) ) -> E. x A = { x } ) $=
( vy vz csn wf1 c0 wne wa cv wceq wral wrex wex wcel w3a cfv fvconst issn
wf f1f 3adant3 3adant2 eqtr4d syl3an1 f1veqaeq 3impb mpd 3expia reximdva0
wi ralrimiv syl ) BCGZDHZBIJKELZFLZMZFBNZEBOBALGMAPUQVAEBUQURBQZKUTFBUQVB
USBQZUTUQVBVCRURDSZUSDSZMZUTUQBUPDUBZVBVCVFBUPDUCVGVBVCRVDCVEVGVBVDCMVCBC
URDTUDVGVCVECMVBBCUSDTUEUFUGUQVBVCVFUTUMBUPURUSDUHUIUJUKUNULEFABUAUO $.
$}

${
$d A f x $. $d D f x $. $d V f x $. $d f ps $. $d ph x $.
$( TODO: there must be a more elegant way to prove this theorem using
Expand Down Expand Up @@ -83685,6 +83698,21 @@ other applications (for instance in intuitionistic set theory) need it.
1n0 $p |- 1o =/= (/) $=
( c1o c0 csn df1o2 0ex snnz eqnetri ) ABCBDBEFG $.

$( 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) $)
nlim1 $p |- -. Lim 1o $=
( c1o wlim word c0 wne cuni wceq w3a csn 1n0 0ex unisn neeqtrri unieqi neii
df1o2 simp3 mto df-lim mtbir ) ABACZADEZAAFZGZHZUEUDAUCADIZFZUCADUGJDKLMAUF
PNMOUAUBUDQRAST $.
$( $j usage 'nlim1' avoids 'ax-un'; $)

$( 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) $)
nlim2 $p |- -. Lim 2o $=
( c2o wlim word c0 wne cuni wceq w3a c1o wcel cpr 1oex prid2 df2o3 eleqtrri
1on onirri eleq2 mtbiri mt2 neir cun unieqi 0ex unipr 3eqtri neeqtrri simp3
0un neii mto df-lim mtbir ) ABACZADEZAAFZGZHZURUQAUPAIUPAIAIGZIAJZIDIKZADIL
MNOUSUTIIJIPQAIIRSTUAUPVAFDIUBIAVANUCDIUDLUEIUIUFUGUJUNUOUQUHUKAULUM $.
$( $j usage 'nlim2' avoids 'ax-un'; $)

$( Cartesian products with the singletons of ordinals 0 and 1 are disjoint.
(Contributed by NM, 2-Jun-2007.) $)
xp01disj $p |- ( ( A X. { (/) } ) i^i ( C X. { 1o } ) ) = (/) $=
Expand Down Expand Up @@ -83713,6 +83741,42 @@ other applications (for instance in intuitionistic set theory) need it.
( c1o wcel c0 csn wceq df1o2 eleq2i 0ex elsn2 bitri ) ABCADEZCADFBLAGHADIJK
$.

$( An ordinal that is not 0 or 1 contains 1. (Contributed by BTernaryTau,
1-Dec-2024.) $)
ord1eln01 $p |- ( Ord A -> ( 1o e. A <-> ( A =/= (/) /\ A =/= 1o ) ) ) $=
( word c1o wcel c0 wne wa ne0i wceq 1on onirri eleq2 mtbiri necon2ai jca wo
wn el1o biimpi necon3ai nesym anim12ci pm4.56 sylib wb ordtri2 mpan syl5ibr
onordi impbid2 ) ABZCADZAEFZACFZGZULUMUNACHULACACIULCCDCJKACCLMNOUOULUKCAIZ
ACDZPQZUOUPQZUQQZGURUMUTUNUSUQAEUQAEIARSTUNUSACUASUBUPUQUCUDCBUKULURUECJUIC
AUFUGUHUJ $.
$( $j usage 'ord1eln01' avoids 'ax-un'; $)

$( An ordinal that is not 0, 1, or 2 contains 2. (Contributed by
BTernaryTau, 1-Dec-2024.) $)
ord2eln012 $p |- ( Ord A ->
( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) ) $=
( word c2o wcel c0 wne c1o w3a ne0i wceq 2on0 nemtbir eleq2 mtbiri necon2ai
el1o 2on onirri 3jca wn wo wa nesym biimpi 3ad2ant3 cpr simp1 nelprd eleq2i
simp2 df2o3 sylnibr jca pm4.56 sylib wb onordi ordtri2 mpan syl5ibr impbid2
) ABZCADZAEFZAGFZACFZHZVCVDVEVFACIVCAGAGJVCCGDZVHCEKCPLAGCMNOVCACACJVCCCDCQ
RACCMNOSVGVCVBCAJZACDZUATZVGVITZVJTZUBVKVGVLVMVFVDVLVEVFVLACUCUDUEVGAEGUFZD
VJVGAEGVDVEVFUGVDVEVFUJUHCVNAUKUIULUMVIVJUNUOCBVBVCVKUPCQUQCAURUSUTVA $.
$( $j usage 'ord2eln012' avoids 'ax-un'; $)

$( A limit ordinal contains 1. (Contributed by BTernaryTau, 1-Dec-2024.) $)
1ellim $p |- ( Lim A -> 1o e. A ) $=
( wlim c1o wcel c0 wceq nlim0 limeq mtbiri necon2ai nlim1 word wa wb limord
wne ord1eln01 syl mpbir2and ) ABZCADZAEPZACPZTAEAEFTEBGAEHIJTACACFTCBKACHIJ
TALUAUBUCMNAOAQRS $.
$( $j usage '1ellim' avoids 'ax-un'; $)

$( A limit ordinal contains 2. (Contributed by BTernaryTau, 1-Dec-2024.) $)
2ellim $p |- ( Lim A -> 2o e. A ) $=
( wlim c2o wcel c0 wne c1o wceq nlim0 limeq mtbiri necon2ai nlim1 nlim2 w3a
word wb limord ord2eln012 syl mpbir3and ) ABZCADZAEFZAGFZACFZUBAEAEHUBEBIAE
JKLUBAGAGHUBGBMAGJKLUBACACHUBCBNACJKLUBAPUCUDUEUFOQARASTUA $.
$( $j usage '2ellim' avoids 'ax-un'; $)

$( Two ways to say that ` A ` is a nonzero number of the set ` B ` .
(Contributed by Mario Carneiro, 21-May-2015.) $)
dif1o $p |- ( A e. ( B \ 1o ) <-> ( A e. B /\ A =/= (/) ) ) $=
Expand Down Expand Up @@ -85886,13 +85950,33 @@ general ordinal versions of these theorems (in this case ~ oa0r ) so
VASURVEVNVHNVFVEVMVHADWDVJVLVHWDVJFWBVLVHWDVJWBWHUSWCUTVBVCSVD $.
$}

$( One is a natural number. (Contributed by NM, 29-Oct-1995.) $)
$( The ordinal 1 is a natural number. For a shorter proof using Peano's
postulates that depends on ~ ax-un , see ~ 1onnALT . (Contributed by NM,
29-Oct-1995.) Avoid ~ ax-un . (Revised by BTernaryTau, 1-Dec-2024.) $)
1onn $p |- 1o e. _om $=
( vx c1o com wcel con0 cv wlim wi wal 1on 1ellim ax-gen elom mpbir2an ) BCD
BEDAFZGBODHZAIJPAOKLABMN $.
$( $j usage '1onn' avoids 'ax-un'; $)

$( Shorter proof of ~ 1onn using Peano's postulates that depends on ~ ax-un .
(Contributed by NM, 29-Oct-1995.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
BTernaryTau marked this conversation as resolved.
Show resolved Hide resolved
1onnALT $p |- 1o e. _om $=
( c1o c0 csuc com df-1o wcel peano1 peano2 ax-mp eqeltri ) ABCZDEBDFKDFGBHI
J $.

$( The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.) $)
$( The ordinal 2 is a natural number. For a shorter proof using Peano's
postulates that depends on ~ ax-un , see ~ 2onnALT . (Contributed by NM,
28-Sep-2004.) Avoid ~ ax-un . (Revised by BTernaryTau, 1-Dec-2024.) $)
2onn $p |- 2o e. _om $=
( vx c2o com wcel con0 cv wlim wi wal 2on 2ellim ax-gen elom mpbir2an ) BCD
BEDAFZGBODHZAIJPAOKLABMN $.
$( $j usage '2onn' avoids 'ax-un'; $)

$( Shorter proof of ~ 2onn using Peano's postulates that depends on ~ ax-un .
(Contributed by NM, 28-Sep-2004.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
2onnALT $p |- 2o e. _om $=
( c2o c1o csuc com df-2o wcel 1onn peano2 ax-mp eqeltri ) ABCZDEBDFKDFGBHIJ
$.

Expand Down Expand Up @@ -92497,16 +92581,6 @@ proved without using the Axiom of Power Sets (unlike ~ domsdomtr ).
$( $j usage 'phpeqd' avoids 'ax-pow'; $)
$}

$( A singleton ` { A } ` is never equinumerous with the ordinal number 2.
This holds for proper singletons ( ` A e. _V ` ) as well as for singletons
being the empty set ( ` A e/ _V ` ). (Contributed by AV, 6-Aug-2019.) $)
snnen2o $p |- -. { A } ~~ 2o $=
( cvv wcel csn c2o cen wbr wn c1o csuc com 1onn php5 ax-mp ensn1g wi ensymb
df-2o c0 wceq eqcomi breq2i entr ex sylbi con3rr3 sylnbi mpsyl 2on0 nemtbir
en0 bitri snprc biimpi breq1d mtbiri pm2.61i ) ABCZADZEFGZHZIIJZFGZHZURUSIF
GZVAIKCVDLIMNABOVCIEFGZVEVAPVBEIFEVBRUAUBVEUTVFVEIUSFGZUTVFPUSIQVGUTVFIUSEU
CUDUEUFUGUHURHZUTSEFGZVIESUIVIESFGESTSEQEUKULUJVHUSSEFVHUSSTAUMUNUOUPUQ $.

$( Cardinal ordering agrees with ordinal number ordering when the smaller
number is a natural number. Compare with ~ nndomo when both are natural
numbers. (Contributed by NM, 17-Jun-1998.) Generalize from ~ nndomo .
Expand Down Expand Up @@ -92692,6 +92766,16 @@ being the empty set ( ` A e/ _V ` ). (Contributed by AV, 6-Aug-2019.) $)
UTABNOABPSQUMARZBRZUQUSTUNAUJBUKVAVBFZUQBADZKUSABUAVCVDURVBVAVDURTBAUBUCUDU
LUEUFUNUQUPLUMABEUGUHUI $.

$( Obsolete version of ~ snnen2o as of 18-Nov-2024. (Contributed by AV,
6-Aug-2019.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
snnen2oOLD $p |- -. { A } ~~ 2o $=
( cvv wcel csn c2o cen wbr wn c1o csuc com 1onn php5 ax-mp ensn1g wi ensymb
df-2o c0 wceq eqcomi breq2i entr ex sylbi con3rr3 sylnbi mpsyl 2on0 nemtbir
en0 bitri snprc biimpi breq1d mtbiri pm2.61i ) ABCZADZEFGZHZIIJZFGZHZURUSIF
GZVAIKCVDLIMNABOVCIEFGZVEVAPVBEIFEVBRUAUBVEUTVFVEIUSFGZUTVFPUSIQVGUTVFIUSEU
CUDUEUFUGUHURHZUTSEFGZVIESUIVIESFGESTSEQEUKULUJVHUSSEFVHUSSTAUMUNUOUPUQ $.


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Expand Down Expand Up @@ -92815,6 +92899,23 @@ Finite sets (cont.)
EWFXMXTFXSXPXRWGXHWSXLXSWHWIWNXHWSFERWJWKWLWMWOWPWQWR $.
$}

${
$d A f $.
$( A singleton ` { A } ` is never equinumerous with the ordinal number 2.
This holds for proper singletons ( ` A e. _V ` ) as well as for
singletons being the empty set ( ` A e/ _V ` ). (Contributed by AV,
6-Aug-2019.) Avoid ~ ax-pow , ~ ax-un . (Revised by BTernaryTau,
1-Dec-2024.) $)
snnen2o $p |- -. { A } ~~ 2o $=
( vf vx csn c2o cen wbr cv wf1o wex ccnv wf1 wceq c0 c1o cvv wcel wne nex
mto cpr df2o3 0ex 1oex 1n0 necomi prnesn mp3an eqnetri neii f1cdmsn mpan2
2on0 f1ocnv f1of1 syl wb snex 2oex breng mp2an mtbir ) ADZEFGZVCEBHZIZBJZ
VFBVFEVCVEKZLZVIECHZDZMZCJZVLCEVKENOUAZVKUBNPQOPQNORVNVKRUCUDONUEUFNOVJPP
UGUHUIUJSVIENRVMUMCEAVHUKULTVFEVCVHIVIVCEVEUNEVCVHUOUPTSVCPQEPQVDVGUQAURU
SVCEBPPUTVAVB $.
$( $j usage 'snnen2o' avoids 'ax-pow' 'ax-un'; $)
$}

${
$d F w z $. $d a b m n s t w x z $.
unxpdomlem1.1 $e |- F = ( x e. ( a u. b ) |-> G ) $.
Expand Down
Loading