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-11 usage #4511

Merged
merged 8 commits into from
Dec 30, 2024
Merged

Reduce ax-11 usage #4511

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
783fa65
Prove alcomw
BTernaryTau Dec 29, 2024
95b330c
Prove dftr2c
BTernaryTau Dec 29, 2024
098ef8b
Revise dftr5
BTernaryTau Dec 29, 2024
f1e115e
Revise unissb
BTernaryTau Dec 29, 2024
fc45de6
Revise cotrg
BTernaryTau Dec 29, 2024
da7fd1e
Revise cnvsym
BTernaryTau Dec 29, 2024
0b4a308
Revise dffun2
BTernaryTau Dec 29, 2024
b2afe33
Merge remote-tracking branch 'upstream/develop' into avoid-ax-11
BTernaryTau Dec 29, 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
16 changes: 13 additions & 3 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15784,6 +15784,7 @@ New usage of "cnvbraval" is discouraged (1 uses).
New usage of "cnvfiALT" is discouraged (0 uses).
New usage of "cnvoprabOLD" is discouraged (0 uses).
New usage of "cnvsymOLD" is discouraged (0 uses).
New usage of "cnvsymOLDOLD" is discouraged (0 uses).
New usage of "cnvunop" is discouraged (2 uses).
New usage of "com3rgbi" is discouraged (1 uses).
New usage of "con3ALT" is discouraged (0 uses).
Expand All @@ -15798,6 +15799,7 @@ New usage of "conventions-labels" is discouraged (0 uses).
New usage of "copsex2gOLD" is discouraged (0 uses).
New usage of "copsexg" is discouraged (1 uses).
New usage of "cotrgOLD" is discouraged (0 uses).
New usage of "cotrgOLDOLD" is discouraged (0 uses).
New usage of "counop" is discouraged (0 uses).
New usage of "crhmsubcALTV" is discouraged (1 uses).
New usage of "cringcALTV" is discouraged (9 uses).
Expand Down Expand Up @@ -16037,6 +16039,7 @@ New usage of "dfcnqs" is discouraged (4 uses).
New usage of "dfeu" is discouraged (0 uses).
New usage of "dffr2ALT" is discouraged (0 uses).
New usage of "dffun2OLD" is discouraged (0 uses).
New usage of "dffun2OLDOLD" is discouraged (0 uses).
New usage of "dffun3OLD" is discouraged (0 uses).
New usage of "dffun6OLD" is discouraged (0 uses).
New usage of "dfhnorm2" is discouraged (3 uses).
Expand All @@ -16056,6 +16059,7 @@ New usage of "dfsb2" is discouraged (1 uses).
New usage of "dfsb3" is discouraged (0 uses).
New usage of "dfsn2ALT" is discouraged (0 uses).
New usage of "dfss2OLD" is discouraged (0 uses).
New usage of "dftr5OLD" is discouraged (0 uses).
New usage of "dftru2" is discouraged (0 uses).
New usage of "dfvd1imp" is discouraged (1 uses).
New usage of "dfvd1impr" is discouraged (1 uses).
Expand Down Expand Up @@ -19409,6 +19413,7 @@ New usage of "uniprgOLD" is discouraged (0 uses).
New usage of "unipwr" is discouraged (0 uses).
New usage of "unipwrVD" is discouraged (0 uses).
New usage of "unisnALT" is discouraged (0 uses).
New usage of "unissbOLD" is discouraged (0 uses).
New usage of "unitreslOLD" is discouraged (0 uses).
New usage of "unop" is discouraged (5 uses).
New usage of "unopadj" is discouraged (2 uses).
Expand Down Expand Up @@ -20112,7 +20117,8 @@ Proof modification of "cnncvsaddassdemo" is discouraged (46 steps).
Proof modification of "cnncvsmulassdemo" is discouraged (95 steps).
Proof modification of "cnvfiALT" is discouraged (46 steps).
Proof modification of "cnvoprabOLD" is discouraged (262 steps).
Proof modification of "cnvsymOLD" is discouraged (88 steps).
Proof modification of "cnvsymOLD" is discouraged (69 steps).
Proof modification of "cnvsymOLDOLD" is discouraged (88 steps).
Proof modification of "com3rgbi" is discouraged (35 steps).
Proof modification of "con3ALT" is discouraged (54 steps).
Proof modification of "con3ALT2" is discouraged (14 steps).
Expand All @@ -20124,7 +20130,8 @@ Proof modification of "conventions" is discouraged (1 steps).
Proof modification of "conventions-comments" is discouraged (1 steps).
Proof modification of "conventions-labels" is discouraged (1 steps).
Proof modification of "copsex2gOLD" is discouraged (119 steps).
Proof modification of "cotrgOLD" is discouraged (110 steps).
Proof modification of "cotrgOLD" is discouraged (99 steps).
Proof modification of "cotrgOLDOLD" is discouraged (110 steps).
Proof modification of "csbcnvgALT" is discouraged (112 steps).
Proof modification of "csbconstgOLD" is discouraged (8 steps).
Proof modification of "csbeq2gVD" is discouraged (61 steps).
Expand Down Expand Up @@ -20152,7 +20159,8 @@ Proof modification of "demoivreALT" is discouraged (1087 steps).
Proof modification of "dfbi1ALT" is discouraged (100 steps).
Proof modification of "dfeu" is discouraged (35 steps).
Proof modification of "dffr2ALT" is discouraged (64 steps).
Proof modification of "dffun2OLD" is discouraged (157 steps).
Proof modification of "dffun2OLD" is discouraged (109 steps).
Proof modification of "dffun2OLDOLD" is discouraged (157 steps).
Proof modification of "dffun3OLD" is discouraged (72 steps).
Proof modification of "dffun6OLD" is discouraged (10 steps).
Proof modification of "dfid2OLD" is discouraged (3 steps).
Expand All @@ -20164,6 +20172,7 @@ Proof modification of "dfnul4OLD" is discouraged (23 steps).
Proof modification of "dfrecs3OLD" is discouraged (263 steps).
Proof modification of "dfsn2ALT" is discouraged (30 steps).
Proof modification of "dfss2OLD" is discouraged (56 steps).
Proof modification of "dftr5OLD" is discouraged (93 steps).
Proof modification of "dfvd1imp" is discouraged (10 steps).
Proof modification of "dfvd1impr" is discouraged (10 steps).
Proof modification of "dfvd1ir" is discouraged (11 steps).
Expand Down Expand Up @@ -21426,6 +21435,7 @@ Proof modification of "uniprgOLD" is discouraged (80 steps).
Proof modification of "unipwr" is discouraged (32 steps).
Proof modification of "unipwrVD" is discouraged (41 steps).
Proof modification of "unisnALT" is discouraged (146 steps).
Proof modification of "unissbOLD" is discouraged (138 steps).
Proof modification of "unitreslOLD" is discouraged (24 steps).
Proof modification of "upgr0eopALT" is discouraged (55 steps).
Proof modification of "upgr1eopALT" is discouraged (126 steps).
Expand Down
131 changes: 119 additions & 12 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17015,6 +17015,19 @@ variables and no wff metavariables (see ~ ax12wdemo for an example of
$.
$}

${
$d ph z $. $d ph w $. $d ps x $. $d ch y $. $d x y $. $d y z $.
$d w x $.
alcomw.1 $e |- ( x = w -> ( ph <-> ps ) ) $.
alcomw.2 $e |- ( y = z -> ( ph <-> ch ) ) $.
$( Weak version of ~ alcom . Uses only Tarski's FOL axiom schemes.
(Contributed by BTernaryTau, 28-Dec-2024.) $)
alcomw $p |- ( A. x A. y ph <-> A. y A. x ph ) $=
( wal alcomiw impbii ) AEJDJADJEJACDEFIKABEDGHKL $.
$( $j usage 'alcomw' avoids 'ax-8' 'ax-9' 'ax-10' 'ax-11' 'ax-12'
'ax-13'; $)
$}

${
$d x y $.
hbn1fw.1 $e |- ( A. x ph -> A. y A. x ph ) $.
Expand Down Expand Up @@ -45816,10 +45829,28 @@ there is another (different) element of the class ` V ` which is an
$.

${
$d x y A $. $d x y B $.
$d A x y z $. $d B x y z $.
$( Relationship involving membership, subset, and union. Exercise 5 of
[Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) $)
[Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.)
Avoid ~ ax-11 . (Revised by BTernaryTau, 28-Dec-2024.) $)
unissb $p |- ( U. A C_ B <-> A. x e. A x C_ B ) $=
( vy vz cv cuni wcel wi wal wss wral wel wa albii weq bitri dfss2 3bitr4i
eleq1w wex eluni imbi1i 19.23v bitr4i elequ1 anbi1d imbi12d elequ2 imbi1d
anbi12d alcomw 19.21v impexp bi2.04 imbi2i df-ral ) DFZBGZHZURCHZIZDJZAFZ
BHZVDCKZIZAJZUSCKVFABLVCDAMZVENZVAIZAJZDJZVHVBVLDVBVJAUAZVAIVLUTVNVAAURBU
BUCVJVAAUDUEOVMVKDJZAJVHVKEAMZVENZEFZCHZIDEMZVRBHZNZVAIDAEEDEPZVJVQVAVSWC
VIVPVEDEAUFUGDECTUHAEPZVJWBVAWDVIVTVEWAAEDUIAEBTUKUJULVOVGAVEVIVAIZIZDJVE
WEDJZIVOVGVEWEDUMVKWFDVKVIVEVAIIWFVIVEVAUNVIVEVAUOQOVFWGVEDVDCRUPSOQQDUSC
RVFABUQS $.
$( $j usage 'unissb' avoids 'ax-11'; $)
$}

${
$d x y A $. $d x y B $.
$( Obsolete version of ~ unissb as of 28-Dec-2024. (Contributed by NM,
20-Sep-2003.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
unissbOLD $p |- ( U. A C_ B <-> A. x e. A x C_ B ) $=
( vy cv cuni wcel wi wal wss wa wex eluni imbi1i 19.23v albii bitri dfss2
wral 3bitr4i bitr4i alcom 19.21v impexp bi2.04 imbi2i df-ral ) DEZBFZGZUH
CGZHZDIZAEZBGZUNCJZHZAIZUICJUPABSUMUHUNGZUOKZUKHZAIZDIZURULVBDULUTALZUKHV
Expand Down Expand Up @@ -49111,10 +49142,36 @@ transitive relation (see ~ cotr ). Definition of [Enderton] p. 71
( cuni wss cv wcel wi wal wa dfss2 df-tr 19.23v eluni imbi1i bitr4i albii
wtr wex 3bitr4i ) CDZCEAFZUAGZUBCGZHZAICRUBBFZGUFCGJZUDHBIZAIAUACKCLUHUEA
UHUGBSZUDHUEUGUDBMUCUIUDBUBCNOPQT $.
$}

${
$d A x y z $.
$( Variant of ~ dftr2 with commuted quantifiers, useful for shortening
proofs and avoiding ~ ax-11 . (Contributed by BTernaryTau,
28-Dec-2024.) $)
dftr2c $p |- ( Tr A <-> A. y A. x ( ( x e. y /\ y e. A ) -> x e. A ) ) $=
( vz wtr wel cv wcel wa wal dftr2 weq elequ1 anbi1d eleq1w imbi12d elequ2
wi anbi12d imbi1d alcomw bitri ) CEABFZBGCHZIZAGCHZRZBJAJUGAJBJABCKUGDBFZ
UDIZDGCHZRADFZUJIZUFRABDDADLZUEUIUFUJUMUCUHUDADBMNADCOPBDLZUEULUFUNUCUKUD
UJBDAQBDCOSTUAUB $.
$( $j usage 'dftr2c' avoids 'ax-11'; $)
$}

${
$d A x y $.
$( An alternate way of defining a transitive class. (Contributed by NM,
20-Mar-2004.) $)
20-Mar-2004.) Avoid ~ ax-11 . (Revised by BTernaryTau,
28-Dec-2024.) $)
dftr5 $p |- ( Tr A <-> A. x e. A A. y e. x y e. A ) $=
( wel cv wcel wa wal wral wtr impexp albii df-ral r19.21v 3bitr2i 3bitr4i
wi dftr2c ) BADZAEZCFZGBECFZQZBHZAHUAUBBTIZQZAHCJUEACIUDUFAUDSUAUBQZQZBHU
GBTIUFUCUHBSUAUBKLUGBTMUAUBBTNOLBACRUEACMP $.
$( $j usage 'dftr5' avoids 'ax-11'; $)

$( Obsolete version of ~ dftr5 as of 28-Dec-2024. (Contributed by NM,
20-Mar-2004.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
dftr5OLD $p |- ( Tr A <-> A. x e. A A. y e. x y e. A ) $=
( wtr cv wcel wa wi wal wral dftr2 alcom impexp albii df-ral bitr4i bitri
r19.21v ) CDBEZAEZFZTCFZGSCFZHZAIBIZUCBTJZACJZBACKUEUDBIZAIZUGUDBALUIUBUF
HZAIUGUHUJAUHUBUCHZBTJZUJUHUAUKHZBIULUDUMBUAUBUCMNUKBTOPUBUCBTRQNUFACOPQQ
Expand Down Expand Up @@ -57440,14 +57497,33 @@ the restriction (of the relation) to the singleton containing this
$}

${
$d x y z A $. $d x y z B $. $d x y z C $.
$d A w x y z $. $d B w x y z $. $d C w x y z $.
$( Two ways of saying that the composition of two relations is included in
a third relation. See its special instance ~ cotr for the main
application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by
Andrew Salmon, 27-Aug-2011.) Generalized from its special instance
~ cotr . (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by
SN, 19-Dec-2024.) $)
SN, 19-Dec-2024.) Avoid ~ ax-11 . (Revised by BTernaryTau,
29-Dec-2024.) $)
cotrg $p |-
( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) $=
( vw ccom wss cv wbr wi wal wa wrel vex albii weq breq2 bitri relco ax-mp
ssrel3 wex brco imbi1i 19.23v bitr4i anbi2d imbi12d anbi12d imbi1d alcomw
wb breq1 ) DEHZFIZAJZCJZUPKZURUSFKZLZCMZAMZURBJZEKZVEUSDKZNZVALZCMBMZAMUP
OUQVDUNDEUAACUPFUCUBVCVJAVCVIBMZCMVJVBVKCVBVHBUDZVALVKUTVLVABURUSDEAPCPUE
UFVHVABUGUHQVIVFVEGJZDKZNZURVMFKZLURVMEKZVMUSDKZNZVALCBGGCGRZVHVOVAVPVTVG
VNVFUSVMVEDSUIUSVMURFSUJBGRZVHVSVAWAVFVQVGVRVEVMURESVEVMUSDUOUKULUMTQT $.
$( $j usage 'cotrg' avoids 'ax-11'; $)
$}

${
$d x y z A $. $d x y z B $. $d x y z C $.
$( Obsolete version of ~ cotrg as of 29-Dec-2024. (Contributed by NM,
27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Generalized from its special instance ~ cotr . (Revised by Richard
Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
cotrgOLD $p |-
( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) $=
( ccom wss cv wbr wi wal wa wrel wb relco ssrel3 vex albii bitri wex brco
ax-mp imbi1i 19.23v bitr4i alcom ) DEGZFHZAIZCIZUHJZUJUKFJZKZCLZALZUJBIZE
Expand All @@ -57459,7 +57535,7 @@ the restriction (of the relation) to the singleton containing this
Generalized from its special instance ~ cotr . (Revised by Richard
Penner, 24-Dec-2019.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
cotrgOLD $p |-
cotrgOLDOLD $p |-
( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) ) $=
( ccom wss cv cop wcel wi wal wbr wa wrel wb vex albii bitri relco opelco
ssrel ax-mp wex df-br bicomi imbi12i 19.23v bitr4i alcom ) DEGZFHZAIZCIZJ
Expand Down Expand Up @@ -57502,16 +57578,29 @@ the restriction (of the relation) to the singleton containing this
$( Two ways of saying a relation is symmetric. Similar to definition of
symmetry in [Schechter] p. 51. (Contributed by NM, 28-Dec-1996.)
(Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by
SN, 23-Dec-2024.) $)
SN, 23-Dec-2024.) Avoid ~ ax-11 . (Revised by BTernaryTau,
29-Dec-2024.) $)
cnvsym $p |- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) $=
( vz ccnv wss cv wbr wi wal wrel wb relcnv ssrel3 ax-mp weq breq1 imbi12d
breq2 vex alcomw brcnv imbi1i 2albii 3bitri ) CEZCFZBGZAGZUFHZUHUICHZIZAJ
BJZULBJAJUIUHCHZUKIZBJAJUFKUGUMLCMBAUFCNOULDGZUIUFHZUPUICHZIUHUPUFHZUHUPC
HZIBADDBDPUJUQUKURUHUPUIUFQUHUPUICQRADPUJUSUKUTUIUPUHUFSUIUPUHCSRUAULUOAB
UJUNUKUHUICBTATUBUCUDUE $.
$( $j usage 'cnvsym' avoids 'ax-11'; $)

$( Obsolete proof of ~ cnvsym as of 29-Dec-2024. (Contributed by NM,
28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof
shortened by SN, 23-Dec-2024.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
cnvsymOLD $p |- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) $=
( ccnv wss cv wbr wi wal wrel relcnv ssrel3 ax-mp alcom vex imbi1i 2albii
wb brcnv 3bitri ) CDZCEZBFZAFZUAGZUCUDCGZHZAIBIZUGBIAIUDUCCGZUFHZBIAIUAJU
BUHRCKBAUACLMUGBANUGUJABUEUIUFUCUDCBOAOSPQT $.

$( Obsolete proof of ~ cnvsym as of 23-Dec-2024. (Contributed by NM,
28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
cnvsymOLD $p |- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) $=
cnvsymOLDOLD $p |- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) $=
( cv cop ccnv wcel wi wal wss wbr alcom wrel relcnv ssrel ax-mp vex brcnv
wb df-br bitr3i imbi12i 2albii 3bitr4i ) BDZADZEZCFZGZUGCGZHZAIBIZUKBIAIU
HCJZUFUECKZUEUFCKZHZBIAIUKBALUHMUMULSCNBAUHCOPUPUKABUNUIUOUJUNUEUFUHKUIUE
Expand Down Expand Up @@ -61497,21 +61586,39 @@ empty set when it is not meaningful (as shown by ~ ndmfv and ~ fvprc ).
$}

${
$d A x y z $.
$d A w x y z $.
$( Alternate definition of a function. (Contributed by NM, 29-Dec-1996.)
Avoid ~ ax-10 , ~ ax-12 . (Revised by SN, 19-Dec-2024.) $)
Avoid ~ ax-10 , ~ ax-12 . (Revised by SN, 19-Dec-2024.) Avoid
~ ax-11 . (Revised by BTernaryTau, 29-Dec-2024.) $)
dffun2 $p |- ( Fun A <-> ( Rel A /\
A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) ) $=
( vw wfun wrel ccnv ccom cid wa cv wbr weq wi wal breq1 albidv vex bitri
df-fun cotrg anbi1d imbi12d breq2 anbi12d imbi1d alcomw brcnv anbi1i ideq
wss imbi12i 3albii anbi2i ) DFDGZDDHZIJULZKUPALZBLZDMZUSCLZDMZKZBCNZOZCPB
PAPZKDUAURVGUPURUTUSUQMZVCKZUTVBJMZOZCPZAPBPZVGBACDUQJUBVMVLBPAPVGVLELZUS
UQMZVCKZVNVBJMZOZCPUTVNUQMZVNVBDMZKZVJOZCPBAEEBENZVKVRCWCVIVPVJVQWCVHVOVC
UTVNUSUQQUCUTVNVBJQUDRAENZVKWBCWDVIWAVJWDVHVSVCVTUSVNUTUQUEUSVNVBDQUFUGRU
HVKVFABCVIVDVJVEVHVAVCUTUSDBSASUIUJUTVBCSUKUMUNTTUOT $.
$( $j usage 'dffun2' avoids 'ax-10' 'ax-11' 'ax-12'; $)
$}

${
$d A x y z $.
$( Obsolete version of ~ dffun2 as of 29-Dec-2024. (Contributed by NM,
29-Dec-1996.) Avoid ~ ax-10 , ~ ax-12 . (Revised by SN, 19-Dec-2024.)
(Proof modification is discouraged.) (New usage is discouraged.) $)
dffun2OLD $p |- ( Fun A <-> ( Rel A /\
A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) ) $=
( wfun wrel ccnv ccom cid wss wa cv wbr weq wi wal df-fun cotrg vex bitri
alcom brcnv anbi1i ideq imbi12i 3albii anbi2i ) DEDFZDDGZHIJZKUHALZBLZDMZ
UKCLZDMZKZBCNZOZCPBPAPZKDQUJUSUHUJULUKUIMZUOKZULUNIMZOZCPZAPBPZUSBACDUIIR
VEVDBPAPUSVDBAUAVCURABCVAUPVBUQUTUMUOULUKDBSASUBUCULUNCSUDUEUFTTUGT $.
$( $j usage 'dffun2' avoids 'ax-10' 'ax-12'; $)
$( $j usage 'dffun2OLD' avoids 'ax-10' 'ax-12'; $)

$( Obsolete version of ~ dffun2 as of 11-Dec-2024. (Contributed by NM,
29-Dec-1996.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
dffun2OLD $p |- ( Fun A <-> ( Rel A /\
dffun2OLDOLD $p |- ( Fun A <-> ( Rel A /\
A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) ) $=
( wfun wrel cid wss wa cv wbr wal wex copab 3bitri vex albii alcom bitri
wi ccnv weq df-fun df-id sseq2i df-co sseq1i ssopab2bw brcnv anbi1i exbii
Expand Down
Loading