From 1e51d774b95e48bcf8e8134112a640ecb50fd42d Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Wed, 2 Oct 2024 13:55:27 +0200 Subject: [PATCH] Add lemmas, reduce axiom usage (#4256) * reduce axiom usage * move ralidmw * review remarks * add $j tags --- discouraged | 14 +++ set.mm | 245 ++++++++++++++++++++++++++++++++++++++++++---------- 2 files changed, 214 insertions(+), 45 deletions(-) diff --git a/discouraged b/discouraged index 2d36eb77e0..c8ac110c87 100644 --- a/discouraged +++ b/discouraged @@ -14861,6 +14861,7 @@ New usage of "cbviing" is discouraged (1 uses). New usage of "cbviinvg" is discouraged (0 uses). New usage of "cbviota" is discouraged (2 uses). New usage of "cbviotav" is discouraged (0 uses). +New usage of "cbviotavwOLD" is discouraged (0 uses). New usage of "cbviung" is discouraged (1 uses). New usage of "cbviunvg" is discouraged (0 uses). New usage of "cbvmo" is discouraged (1 uses). @@ -14884,6 +14885,7 @@ New usage of "cbvralv2" is discouraged (0 uses). New usage of "cbvreu" is discouraged (2 uses). New usage of "cbvreucsf" is discouraged (0 uses). New usage of "cbvreuv" is discouraged (0 uses). +New usage of "cbvreuvwOLD" is discouraged (0 uses). New usage of "cbvrex" is discouraged (4 uses). New usage of "cbvrex2v" is discouraged (0 uses). New usage of "cbvrexcsf" is discouraged (1 uses). @@ -14893,6 +14895,7 @@ New usage of "cbvrexv" is discouraged (3 uses). New usage of "cbvrexv2" is discouraged (0 uses). New usage of "cbvriota" is discouraged (1 uses). New usage of "cbvriotav" is discouraged (0 uses). +New usage of "cbvriotavwOLD" is discouraged (0 uses). New usage of "cbvrmo" is discouraged (1 uses). New usage of "cbvrmov" is discouraged (0 uses). New usage of "cbvrmowOLD" is discouraged (0 uses). @@ -18077,8 +18080,10 @@ New usage of "ralcom2" is discouraged (0 uses). New usage of "raleleqALT" is discouraged (0 uses). New usage of "ralf0OLD" is discouraged (0 uses). New usage of "ralidmOLD" is discouraged (0 uses). +New usage of "ralprgOLD" is discouraged (0 uses). New usage of "ralrexbidOLD" is discouraged (0 uses). New usage of "ralrnmpt" is discouraged (1 uses). +New usage of "ralsngOLD" is discouraged (0 uses). New usage of "ralxfrALT" is discouraged (0 uses). New usage of "rb-ax1" is discouraged (5 uses). New usage of "rb-ax2" is discouraged (9 uses). @@ -18144,7 +18149,9 @@ New usage of "rexbidvALT" is discouraged (0 uses). New usage of "rexbidvaALT" is discouraged (0 uses). New usage of "rexlimddvcbv" is discouraged (0 uses). New usage of "rexn0OLD" is discouraged (0 uses). +New usage of "rexprgOLD" is discouraged (0 uses). New usage of "rexrnmpt" is discouraged (0 uses). +New usage of "rexsngOLD" is discouraged (0 uses). New usage of "rgen2a" is discouraged (0 uses). New usage of "rhmsubcALTV" is discouraged (1 uses). New usage of "rhmsubcALTVcat" is discouraged (0 uses). @@ -19241,8 +19248,11 @@ Proof modification of "cbval2vOLD" is discouraged (85 steps). Proof modification of "cbveuALT" is discouraged (48 steps). Proof modification of "cbveuwOLD" is discouraged (29 steps). Proof modification of "cbvexsv" is discouraged (29 steps). +Proof modification of "cbviotavwOLD" is discouraged (12 steps). Proof modification of "cbvmowOLD" is discouraged (62 steps). Proof modification of "cbvralfwOLD" is discouraged (139 steps). +Proof modification of "cbvreuvwOLD" is discouraged (13 steps). +Proof modification of "cbvriotavwOLD" is discouraged (13 steps). Proof modification of "cbvrmowOLD" is discouraged (58 steps). Proof modification of "ccat2s1fstOLD" is discouraged (43 steps). Proof modification of "ccat2s1fvwALT" is discouraged (116 steps). @@ -20157,7 +20167,9 @@ Proof modification of "ralab2OLD" is discouraged (67 steps). Proof modification of "raleleqALT" is discouraged (26 steps). Proof modification of "ralf0OLD" is discouraged (41 steps). Proof modification of "ralidmOLD" is discouraged (68 steps). +Proof modification of "ralprgOLD" is discouraged (17 steps). Proof modification of "ralrexbidOLD" is discouraged (29 steps). +Proof modification of "ralsngOLD" is discouraged (10 steps). Proof modification of "ralxfrALT" is discouraged (85 steps). Proof modification of "rb-ax1" is discouraged (32 steps). Proof modification of "rb-ax2" is discouraged (17 steps). @@ -20204,6 +20216,8 @@ Proof modification of "rexab2OLD" is discouraged (67 steps). Proof modification of "rexbidvALT" is discouraged (10 steps). Proof modification of "rexbidvaALT" is discouraged (10 steps). Proof modification of "rexn0OLD" is discouraged (17 steps). +Proof modification of "rexprgOLD" is discouraged (17 steps). +Proof modification of "rexsngOLD" is discouraged (10 steps). Proof modification of "rgen2a" is discouraged (81 steps). Proof modification of "rlimaddOLD" is discouraged (159 steps). Proof modification of "rlimmulOLD" is discouraged (159 steps). diff --git a/set.mm b/set.mm index 4b3dbc6940..5e06831ead 100644 --- a/set.mm +++ b/set.mm @@ -23132,6 +23132,20 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not CFZGABIQCIORPSABCDJABCDKLABMQCMN $. $} + ${ + $d x y $. $d x z ps $. $d y z ph $. + cbvmovw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Change bound variable. Uses only Tarski's FOL axiom schemes. See + ~ cbvmo for a version with fewer disjoint variable conditions but + requiring more axioms. (Contributed by NM, 9-Mar-1995.) (Revised by + Gino Giotto, 30-Sep-2024.) $) + cbvmovw $p |- ( E* x ph <-> E* y ps ) $= + ( vz wmo weq wi wal wex df-mo equequ1 imbi12d cbvalvw exbii bicomi bitri + ) ACGACFHZIZCJZFKZBDGZACFLUBBDFHZIZDJZFKZUCUAUFFTUECDCDHABSUDECDFMNOPUCUG + BDFLQRR $. + $( $j usage 'cbvmovw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $} + ${ $d x y z $. $d ph z $. $d ps z $. cbvmow.1 $e |- F/ y ph $. @@ -23169,13 +23183,26 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not cbvmo.3 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ~ ax-13 . Use the - weaker ~ cbvmow when possible. (Contributed by NM, 9-Mar-1995.) - (Revised by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf - Lammen, 4-Jan-2023.) (New usage is discouraged.) $) + weaker ~ cbvmow , ~ cbvmovw when possible. (Contributed by NM, + 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.) (Proof shortened + by Wolf Lammen, 4-Jan-2023.) (New usage is discouraged.) $) cbvmo $p |- ( E* x ph <-> E* y ps ) $= ( wmo wsb sb8mo sbie mobii bitri ) ACHACDIZDHBDHACDEJNBDABCDFGKLM $. $} + ${ + $d x y $. $d x ps $. $d y ph $. + cbveuvw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Change bound variable. Uses only Tarski's FOL axiom schemes. See + ~ cbveu for a version with fewer disjoint variable conditions but + requiring more axioms. (Contributed by NM, 25-Nov-1994.) (Revised by + Gino Giotto, 30-Sep-2024.) $) + cbveuvw $p |- ( E! x ph <-> E! y ps ) $= + ( wex wmo wa weu cbvexvw cbvmovw anbi12i df-eu 3bitr4i ) ACFZACGZHBDFZBDG + ZHACIBDIOQPRABCDEJABCDEKLACMBDMN $. + $( $j usage 'cbveuvw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $} + ${ $d x y $. cbveuw.1 $e |- F/ y ph $. @@ -23209,8 +23236,9 @@ of the unique existential quantifier (note that ` y ` and ` z ` need not cbveu.3 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ~ ax-13 . Use the - weaker ~ cbveuw when possible. (Contributed by NM, 25-Nov-1994.) - (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.) $) + weaker ~ cbveuw , ~ cbveuvw when possible. (Contributed by NM, + 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) + (New usage is discouraged.) $) cbveu $p |- ( E! x ph <-> E! y ps ) $= ( weu wsb sb8eu sbie eubii bitri ) ACHACDIZDHBDHACDEJNBDABCDFGKLM $. @@ -30954,8 +30982,9 @@ generally appear in a single form (either definitional, but more often $( Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it - depends on ~ ax-13 . Use the weaker ~ cbvrmow when possible. - (Contributed by NM, 16-Jun-2017.) (New usage is discouraged.) $) + depends on ~ ax-13 . Use the weaker ~ cbvrmow , ~ cbvrmovw when + possible. (Contributed by NM, 16-Jun-2017.) + (New usage is discouraged.) $) cbvrmo $p |- ( E* x e. A ph <-> E* y e. A ps ) $= ( wrex wreu wi wrmo cbvrex cbvreu imbi12i rmo5 3bitr4i ) ACEIZACEJZKBDEIZ BDEJZKACELBDELRTSUAABCDEFGHMABCDEFGHNOACEPBDEPQ $. @@ -30984,13 +31013,30 @@ generally appear in a single form (either definitional, but more often ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. $( $j usage 'cbvrexvw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $( Change the bound variable of a restricted at-most-one quantifier using + implicit substitution. Version of ~ cbvrmov with a disjoint variable + condition, which requires fewer axioms. (Contributed by NM, + 16-Jun-2017.) (Revised by Gino Giotto, 30-Sep-2024.) $) + cbvrmovw $p |- ( E* x e. A ph <-> E* y e. A ps ) $= + ( cv wcel wa wmo wrmo weq eleq1w anbi12d cbvmovw df-rmo 3bitr4i ) CGEHZAI + ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. + $( $j usage 'cbvrmovw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $( Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of ~ cbvreuv with a disjoint - variable condition, which does not require ~ ax-13 . (Contributed by - NM, 5-Apr-2004.) (Revised by Gino Giotto, 10-Jan-2024.) $) + variable condition, which requires fewer axioms. (Contributed by NM, + 5-Apr-2004.) (Revised by Gino Giotto, 30-Sep-2024.) $) cbvreuvw $p |- ( E! x e. A ph <-> E! y e. A ps ) $= + ( cv wcel wa weu wreu weq eleq1w anbi12d cbveuvw df-reu 3bitr4i ) CGEHZAI + ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. + $( $j usage 'cbvreuvw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + + $( Obsolete version of ~ cbvreuvw as of 30-Sep-2024. (Contributed by NM, + 5-Apr-2004.) (Revised by Gino Giotto, 10-Jan-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + cbvreuvwOLD $p |- ( E! x e. A ph <-> E! y e. A ps ) $= ( nfv cbvreuw ) ABCDEADGBCGFH $. - $( $j usage 'cbvreuvw' avoids 'ax-13'; $) + $( $j usage 'cbvreuvwOLD' avoids 'ax-13'; $) $} ${ @@ -40054,6 +40100,23 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets, ( c0 crab cv wcel wa cab df-rab wceq wn ab0 noel intnanr mpgbir eqtri ) ABC DBEZCFZAGZBHZCABCITCJSKBSBLRAQMNOP $. + ${ + $d x y A $. $d x ps $. $d y ph $. + rabeq0w.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Condition for a restricted class abstraction to be empty. Version of + ~ rabeq0 using implicit substitution, which does not require ~ ax-10 , + ~ ax-11 , ~ ax-12 , but requires ~ ax-8 . (Contributed by Gino Giotto, + 30-Sep-2024.) $) + rabeq0w $p |- ( { x e. A | ph } = (/) <-> A. y e. A -. ps ) $= + ( cv wcel wa cab c0 wceq wn wal crab wral wb wfal falim bitri weq anbi12d + eqcom eleq1w abeq2w noel bifal bibi1i wi idd pm5.21ni impbii albii df-rab + bija id eqeq1i raln 3bitr4i ) CGEHZAIZCJZKLZDGZEHZBIZMZDNZACEOZKLBMDEPVCK + VBLZVHVBKUCVJVDKHZVFQZDNVHVAVFCDKCDUAUTVEABCDEUDFUBUEVLVGDVLRVFQZVGVKRVFV + KVDUFUGUHVMVGRVFVGVFVGUISRMVGUJUORVFVFVFSVFUPUKULTUMTTVIVBKACEUNUQBDEURUS + $. + $( $j usage 'rabeq0w' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + $( Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.) $) rabeq0 $p |- ( { x e. A | ph } = (/) <-> A. x e. A -. ph ) $= @@ -41139,6 +41202,20 @@ disjoint classes (see ~ disjdif ). Part of proof of Corollary 6K of HZGOBGABCDJNBPOBCDKLM $. $} + ${ + $d x y A $. $d ph y $. $d ps x $. + ralidmw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Idempotent law for restricted quantifier. Weak version of ~ ralidm , + which does not require ~ ax-10 , ~ ax-12 , but requires ~ ax-8 . + (Contributed by Gino Giotto, 30-Sep-2024.) $) + ralidmw $p |- ( A. x e. A A. x e. A ph <-> A. x e. A ph ) $= + ( cv wcel wral wi wal df-ral imbi2i albii pm2.21 weq eleq1w imbi12d spw + ja alimi hba1w ax-1 alrimih impbii bitri 3bitr4i ) CGEHZACEIZJZCKZUHAJZCK + ZUICEIUIUKUHUMJZCKZUMUJUNCUIUMUHACELZMNUOUMUNULCUHUMULUHAOULDGEHZBJZCDCDP + UHUQABCDEQFRZSTUAUMUNCULURCDUSUBUMUHUCUDUEUFUICELUPUG $. + $( $j usage 'ralidmw' avoids 'ax-10' 'ax-11' 'ax-12'; $) + $} + ${ $d x A $. $d x y $. $( Vacuous quantification is always true. (Contributed by NM, @@ -42842,14 +42919,23 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). ralsng.1 $e |- ( x = A -> ( ph <-> ps ) ) $. $( Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, - 23-Apr-2015.) (Proof shortened by AV, 7-Apr-2023.) $) + 23-Apr-2015.) Avoid ~ ax-10 , ~ ax-12 . (Revised by Gino Giotto, + 30-Sep-2024.) $) ralsng $p |- ( A e. V -> ( A. x e. { A } ph <-> ps ) ) $= - ( nfv ralsngf ) ABCDEBCGFH $. + ( csn wral cv wceq wi wal wcel df-ral velsn imbi1i albii bitri wb a1i wex + elisset pm5.74i 19.23v pm5.5 3bitrd syl syl5bb ) ACDGZHZCIZDJZAKZCLZDEMZB + UJUKUIMZAKZCLUNACUINUQUMCUPULACDOPQRUOULCUAZUNBSCDEUBURUNULBKZCLZURBKZBUN + UTSURUMUSCULABFUCQTUTVASURULBCUDTURBUEUFUGUH $. + $( $j usage 'ralsng' avoids 'ax-10' 'ax-11' 'ax-12'; $) $( Restricted existential quantification over a singleton. (Contributed by - NM, 29-Jan-2012.) (Proof shortened by AV, 7-Apr-2023.) $) + NM, 29-Jan-2012.) Avoid ~ ax-10 , ~ ax-12 . (Revised by Gino Giotto, + 30-Sep-2024.) $) rexsng $p |- ( A e. V -> ( E. x e. { A } ph <-> ps ) ) $= - ( nfv rexsngf ) ABCDEBCGFH $. + ( wcel wn wral wb wrex cv wceq notbid ralsng dfrex2 bicom1 con1bid syl5bb + csn syl ) DEGAHZCDTZIZBHZJZACUCKZBJUBUECDECLDMABFNOUGUDHUFBACUCPUFBUDUDUE + QRSUA $. + $( $j usage 'rexsng' avoids 'ax-10' 'ax-11' 'ax-12'; $) $( Restricted existential uniqueness over a singleton. (Contributed by AV, 3-Apr-2023.) $) @@ -42866,6 +42952,23 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). UAUBDFHDOFPABETJQRBCEGIKRS $. $} + ${ + $d A x $. $d ps x $. + ralsngOLD.1 $e |- ( x = A -> ( ph <-> ps ) ) $. + $( Obsolete version of ~ ralsng as of 30-Sep-2024. (Contributed by NM, + 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof + shortened by AV, 7-Apr-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + ralsngOLD $p |- ( A e. V -> ( A. x e. { A } ph <-> ps ) ) $= + ( nfv ralsngf ) ABCDEBCGFH $. + + $( Obsolete version of ~ rexsng as of 30-Sep-2024. (Contributed by NM, + 29-Jan-2012.) (Proof shortened by AV, 7-Apr-2023.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + rexsngOLD $p |- ( A e. V -> ( E. x e. { A } ph <-> ps ) ) $= + ( nfv rexsngf ) ABCDEBCGFH $. + $} + ${ $d A x y $. $d ph y $. $( Restricted existential uniqueness over a singleton is equivalent to a @@ -43017,15 +43120,39 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). ralprg.2 $e |- ( x = B -> ( ph <-> ch ) ) $. $( Convert a restricted universal quantification over a pair to a conjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario - Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) $) + Carneiro, 23-Apr-2015.) Avoid ~ ax-10 , ~ ax-12 . (Revised by Gino + Giotto, 30-Sep-2024.) $) ralprg $p |- ( ( A e. V /\ B e. W ) -> + ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) ) $= + ( cpr wral csn wa wcel cun df-pr raleqi ralunb ralsng bi2anan9 syl5bb + bitri ) ADEFKZLZADEMZLZADFMZLZNZEGOZFHOZNBCNUEADUFUHPZLUJADUDUMEFQRADUFUH + SUCUKUGBULUICABDEGITACDFHJTUAUB $. + $( $j usage 'ralprg' avoids 'ax-10' 'ax-11' 'ax-12'; $) + + $( Obsolete version of ~ ralprg as of 30-Sep-2024. (Contributed by NM, + 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof + shortened by AV, 8-Apr-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + ralprgOLD $p |- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } ph <-> ( ps /\ ch ) ) ) $= ( nfv ralprgf ) ABCDEFGHBDKCDKIJL $. $( Convert a restricted existential quantification over a pair to a disjunction. (Contributed by NM, 17-Sep-2011.) (Revised by Mario - Carneiro, 23-Apr-2015.) (Proof shortened by AV, 8-Apr-2023.) $) + Carneiro, 23-Apr-2015.) Avoid ~ ax-10 , ~ ax-12 . (Revised by Gino + Giotto, 30-Sep-2024.) $) rexprg $p |- ( ( A e. V /\ B e. W ) -> + ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) ) $= + ( wcel wa wn cpr wral wb wrex wo wceq notbid ralprg ralnex pm4.56 bibi12i + cv notbi sylbb2 syl ) EGKFHKLAMZDEFNZOZBMZCMZLZPZADUJQZBCRZPZUIULUMDEFGHD + UEZESABITUSFSACJTUAUOUPMZUQMZPURUKUTUNVAADUJUBBCUCUDUPUQUFUGUH $. + $( $j usage 'rexprg' avoids 'ax-10' 'ax-11' 'ax-12'; $) + + $( Obsolete version of ~ rexprg as of 30-Sep-2024. (Contributed by NM, + 17-Sep-2011.) (Revised by Mario Carneiro, 23-Apr-2015.) (Proof + shortened by AV, 8-Apr-2023.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + rexprgOLD $p |- ( ( A e. V /\ B e. W ) -> ( E. x e. { A , B } ph <-> ( ps \/ ch ) ) ) $= ( nfv rexprgf ) ABCDEFGHBDKCDKIJL $. @@ -52349,16 +52476,18 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few $} ${ - $d x y A $. $d x y B $. $d x y R $. + $d x y z A $. $d x y z B $. $d x y z R $. frc.1 $e |- B e. _V $. $( Property of well-founded relation (one direction of definition using class variables). (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 19-Nov-2014.) $) frc $p |- ( ( R Fr A /\ B C_ A /\ B =/= (/) ) -> E. x e. B { y e. B | y R x } = (/) ) $= - ( wfr wss c0 wne w3a cv wbr wn wral wrex crab wceq cvv wcel wa fri mpanl1 - 3impb rabeq0 rexbii sylibr ) CEGZDCHZDIJZKBLALEMZNBDOZADPZUKBDQIRZADPUHUI - UJUMDSTUHUIUJUAUMFABCDSEUBUCUDUNULADUKBDUEUFUG $. + ( vz wfr wss c0 wne w3a cv wbr wn wral wrex crab wceq cvv wcel fri mpanl1 + wa 3impb breq1 rabeq0w rexbii sylibr ) CEHZDCIZDJKZLGMZAMZENZOGDPZADQZBMZ + UNENZBDRJSZADQUJUKULUQDTUAUJUKULUDUQFAGCDTEUBUCUEUTUPADUSUOBGDURUMUNEUFUG + UHUI $. + $( $j usage 'frc' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} ${ @@ -52447,17 +52576,18 @@ We have not yet defined relations ( ~ df-rel ), but here we introduce a few $} ${ - $d x y A $. $d x y B $. $d x y R $. + $d x y A $. $d x y z B $. $d x y z R $. $( A well-founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 2-Jan-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) $) frirr $p |- ( ( R Fr A /\ B e. A ) -> -. B R B ) $= - ( vx vy wfr wcel wa cv wbr csn crab c0 wceq wrex wss adantl wral notbid - wn wne simpl snssi snnzg snex frc syl3anc wb rabeq0 ralbidv syl5bb rexsng - breq2 breq1 ralsng bitrd mpbid ) ACFZBAGZHZDIZEIZCJZDBKZLMNZEVDOZBBCJZTZU - TURVDAPZVDMUAZVFURUSUBUSVIURBAUCQUSVJURBAUDQEDAVDCBUEUFUGUSVFVHUHURUSVFVA - BCJZTZDVDRZVHVEVMEBAVEVCTZDVDRVBBNZVMVCDVDUIVOVNVLDVDVOVCVKVBBVACUMSUJUKU - LVLVHDBAVABNVKVGVABBCUNSUOUPQUQ $. + ( vx vy vz wfr wcel wa cv wbr csn crab c0 wceq adantl wral breq1 notbid + wn wrex wss wne simpl snssi snnzg snex frc syl3anc rabeq0w ralbidv syl5bb + wb breq2 rexsng ralsng bitrd mpbid ) ACGZBAHZIZDJZEJZCKZDBLZMNOZEVEUAZBBC + KZTZVAUSVEAUBZVENUCZVGUSUTUDUTVJUSBAUEPUTVKUSBAUFPEDAVECBUGUHUIUTVGVIUMUS + UTVGFJZBCKZTZFVEQZVIVFVOEBAVFVLVCCKZTZFVEQVCBOZVOVDVPDFVEVBVLVCCRUJVRVQVN + FVEVRVPVMVCBVLCUNSUKULUOVNVIFBAVLBOVMVHVLBBCRSUPUQPUR $. + $( $j usage 'frirr' avoids 'ax-10' 'ax-11' 'ax-12'; $) $} ${ @@ -59553,15 +59683,27 @@ Definite description binder (inverted iota) $} ${ - $d ph y $. $d ps x $. $d x y $. + $d ph y z $. $d ps x z $. $d x y $. cbviotavw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Change bound variables in a description binder. Version of ~ cbviotav - with a disjoint variable condition, which does not require ~ ax-13 . + with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by Gino Giotto, - 26-Jan-2024.) $) + 30-Sep-2024.) $) cbviotavw $p |- ( iota x ph ) = ( iota y ps ) $= + ( vz cab cv csn wceq cuni cio cbvabv eqeq1i abbii unieqi df-iota 3eqtr4i + ) ACGZFHIZJZFGZKBDGZTJZFGZKACLBDLUBUEUAUDFSUCTABCDEMNOPACFQBDFQR $. + $( $j usage 'cbviotavw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $} + + ${ + $d ph y $. $d ps x $. $d x y $. + cbviotavwOLD.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Obsolete version of ~ cbviotavw as of 30-Sep-2024. (Contributed by + Andrew Salmon, 1-Aug-2011.) (Revised by Gino Giotto, 26-Jan-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + cbviotavwOLD $p |- ( iota x ph ) = ( iota y ps ) $= ( nfv cbviotaw ) ABCDEADFBCFG $. - $( $j usage 'cbviotavw' avoids 'ax-13'; $) + $( $j usage 'cbviotavwOLD' avoids 'ax-13'; $) $} ${ @@ -68451,12 +68593,24 @@ Restricted iota (description binder) $d x y A $. $d y ph $. $d x ps $. cbvriotavw.1 $e |- ( x = y -> ( ph <-> ps ) ) $. $( Change bound variable in a restricted description binder. Version of - ~ cbvriotav with a disjoint variable condition, which does not require - ~ ax-13 . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, - 26-Jan-2024.) $) + ~ cbvriotav with a disjoint variable condition, which requires fewer + axioms . (Contributed by NM, 18-Mar-2013.) (Revised by Gino Giotto, + 30-Sep-2024.) $) cbvriotavw $p |- ( iota_ x e. A ph ) = ( iota_ y e. A ps ) $= + ( cv wcel wa cio crio weq eleq1w anbi12d cbviotavw df-riota 3eqtr4i ) CGE + HZAIZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $. + $( $j usage 'cbvriotavw' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $) + $} + + ${ + $d x y A $. $d y ph $. $d x ps $. + cbvriotavwOLD.1 $e |- ( x = y -> ( ph <-> ps ) ) $. + $( Obsolete version of ~ cbvriotavw as of 30-Sep-2024. (Contributed by NM, + 18-Mar-2013.) (Revised by Gino Giotto, 26-Jan-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + cbvriotavwOLD $p |- ( iota_ x e. A ph ) = ( iota_ y e. A ps ) $= ( nfv cbvriotaw ) ABCDEADGBCGFH $. - $( $j usage 'cbvriotavw' avoids 'ax-13'; $) + $( $j usage 'cbvriotavwOLD' avoids 'ax-13'; $) $} ${ @@ -72947,16 +73101,17 @@ result of an operator (deduction version). (Contributed by Paul ( vz wa cv wbr weq w3o wral wn wi wcel w3a wal breq2 r3al 3imtr4g ralbii wwe wfr wor df-we df-so simpr ax-1 fr2nr 3adantr3 anbi2d notbid syl5ibcom wpo pm2.21 syl6 fr3nr df-3an biimpri ancoms nsyl pm2.21d expd 3jaod frirr - a1i 3ad2antr1 jctild ex a2d alimdv 2alimdv ralidm equequ2 breq1 3orbi123d - cbvralvw bitr3i df-po ancrd impbid2 syl5bb pm5.32i bitri ) CDUACDUBZCDUCZ - FWDAGZBGZDHZABIZWGWFDHZJZBCKZACKZFCDUDWDWEWMWECDUMZWMFZWDWMABCDUEWDWOWMWN - WMUFWDWMWNWDWFEGZDHZAEIZWPWFDHZJZECKZBCKZACKZWFWFDHLZWHWGWPDHZFZWQMZFZECK - BCKACKZWMWNWDWFCNZWGCNZWPCNZOZWTMZEPZBPAPXMXHMZEPZBPAPXCXIWDXOXQABWDXNXPE - WDXMWTXHWDXMWTXHMWDXMFZWTXGXDXRWQXGWRWSWQXGMXRWQXFUGVEXRWRXFLZXGXRWHWJFZL - ZWRXSWDXJXKYAXLCWFWGDUHUIWRXTXFWRWJXEWHWFWPWGDQUJUKULXFWQUNUOXRWSXFWQXRWS - XFFZWQXRWHXEWSOZYBCWFWGWPDUPXFWSYCYCXFWSFWHXEWSUQURUSUTVAVBVCWDXKXJXDXLCW - FDVDVFVGVHVIVJVKWTABECCCRXHABECCCRSWLXBACWLWLBCKXBWKBCVLWLXABCWKWTBECBEIW - HWQWIWRWJWSWGWPWFDQBEAVMWGWPWFDVNVOVPTVQTABECDVRSVSVTWAWBWC $. + a1i 3ad2antr1 jctild ex a2d alimdv 2alimdv equequ2 breq1 ralidmw cbvralvw + 3orbi123d bitr3i df-po ancrd impbid2 syl5bb pm5.32i bitri ) CDUACDUBZCDUC + ZFWDAGZBGZDHZABIZWGWFDHZJZBCKZACKZFCDUDWDWEWMWECDUMZWMFZWDWMABCDUEWDWOWMW + NWMUFWDWMWNWDWFEGZDHZAEIZWPWFDHZJZECKZBCKZACKZWFWFDHLZWHWGWPDHZFZWQMZFZEC + KBCKACKZWMWNWDWFCNZWGCNZWPCNZOZWTMZEPZBPAPXMXHMZEPZBPAPXCXIWDXOXQABWDXNXP + EWDXMWTXHWDXMWTXHMWDXMFZWTXGXDXRWQXGWRWSWQXGMXRWQXFUGVEXRWRXFLZXGXRWHWJFZ + LZWRXSWDXJXKYAXLCWFWGDUHUIWRXTXFWRWJXEWHWFWPWGDQUJUKULXFWQUNUOXRWSXFWQXRW + SXFFZWQXRWHXEWSOZYBCWFWGWPDUPXFWSYCYCXFWSFWHXEWSUQURUSUTVAVBVCWDXKXJXDXLC + WFDVDVFVGVHVIVJVKWTABECCCRXHABECCCRSWLXBACWLWLBCKXBWKWTBECBEIWHWQWIWRWJWS + WGWPWFDQBEAVLWGWPWFDVMVPZVNWLXABCWKWTBECYDVOTVQTABECDVRSVSVTWAWBWC $. + $( $j usage 'dfwe2' avoids 'ax-10' 'ax-11' 'ax-12'; $) $}