From 87f6fe1752f98ba61376246e5f0f7929d6ba84b2 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Wed, 20 Nov 2024 15:56:20 +0100 Subject: [PATCH] prove sbrim without ax-10 --- discouraged | 4 ++-- set.mm | 59 ++++++++++++++++++++--------------------------------- 2 files changed, 24 insertions(+), 39 deletions(-) diff --git a/discouraged b/discouraged index ce8ee24282..319c1394ce 100644 --- a/discouraged +++ b/discouraged @@ -18682,8 +18682,8 @@ New usage of "sbidm" is discouraged (0 uses). New usage of "sbie" is discouraged (20 uses). New usage of "sbied" is discouraged (3 uses). New usage of "sbiedv" is discouraged (1 uses). -New usage of "sbiedwOLD" is discouraged (0 uses). New usage of "sbn1ALT" is discouraged (0 uses). +New usage of "sbrimOLD" is discouraged (0 uses). New usage of "sbtALT" is discouraged (0 uses). New usage of "sbtT" is discouraged (0 uses). New usage of "sbtr" is discouraged (0 uses). @@ -20836,8 +20836,8 @@ Proof modification of "sbcoreleleqVD" is discouraged (176 steps). Proof modification of "sbcrexgOLD" is discouraged (77 steps). Proof modification of "sbcssgVD" is discouraged (229 steps). Proof modification of "sbequ2OLD" is discouraged (75 steps). -Proof modification of "sbiedwOLD" is discouraged (51 steps). Proof modification of "sbn1ALT" is discouraged (41 steps). +Proof modification of "sbrimOLD" is discouraged (33 steps). Proof modification of "sbsbc" is discouraged (21 steps). Proof modification of "sbtALT" is discouraged (12 steps). Proof modification of "sbtT" is discouraged (7 steps). diff --git a/set.mm b/set.mm index 1ac2b94cc4..8dcea6b69b 100644 --- a/set.mm +++ b/set.mm @@ -17626,26 +17626,15 @@ disjoint variable condition ( ~ sb2 ). Theorem ~ sb6f replaces the ( ) B $. $} - ${ - $d x y $. - sbrimvlem.1 $e |- ( A. x ( ph -> ( x = y -> ps ) ) - <-> ( ph -> A. x ( x = y -> ps ) ) ) $. - $( Common proof template for ~ sbrimvw and ~ sbrimv . The hypothesis is an - instance of ~ 19.21 . (Contributed by Wolf Lammen, 29-Jan-2024.) $) - sbrimvlem $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $= - ( wi wsb weq wal sb6 bi2.04 albii 3bitr2i imbi2i bitr4i ) ABFZCDGZACDHZBF - ZCIZFZABCDGZFQRPFZCIASFZCIUAPCDJUDUCCARBKLEMUBTABCDJNO $. - $} - ${ $d x y $. $d x ph $. $( Substitution in an implication with a variable not free in the - antecedent affects only the consequent. Version of ~ sbrim and ~ sbrimv - based on fewer axioms, but with more disjoint variable conditions. - Based on an idea of Gino Giotto. (Contributed by Wolf Lammen, - 29-Jan-2024.) $) + antecedent affects only the consequent. Version of ~ sbrim based on + fewer axioms, but with more disjoint variable conditions. Based on an + idea of Gino Giotto. (Contributed by Wolf Lammen, 29-Jan-2024.) $) sbrimvw $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $= - ( weq wi 19.21v sbrimvlem ) ABCDACDEBFCGH $. + ( wi wsb weq wal sb6 bi2.04 albii 19.21v 3bitr2i imbi2i bitr4i ) ABEZCDFZ + ACDGZBEZCHZEZABCDFZEQRPEZCHASEZCHUAPCDIUDUCCARBJKASCLMUBTABCDINO $. $} ${ @@ -19815,21 +19804,25 @@ any disjoint variable condition (but the version with a disjoint ( wi wsb sbi1 sbi2 impbii ) ABECDFACDFBCDFEABCDGABCDHI $. ${ + $d t x $. $d t y $. $d ps t $. $d ph t $. sbrim.1 $e |- F/ x ph $. $( Substitution in an implication with a variable not free in the - antecedent affects only the consequent. See ~ sbrimv for a version with - disjoint variables not requiring ~ ax-10 . (Contributed by NM, - 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) $) + antecedent affects only the consequent. (Contributed by NM, + 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Avoid ~ ax-10 . + (Revised by Gino Giotto, 20-Nov-2024.) $) sbrim $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $= + ( vt wi wsb wal nf5ri stdpc4 syl sbi1 syl5 weq wn nfn alimi df-sb imim2i + pm2.21 a1d a1i syl5com ax-1 sps sylbi ja alrimiv sylibr impbii ) ABGZCDHZ + ABCDHZGZAACDHZUMUNAACIUPACEJACDKLABCDMNUOFDOZCFOZULGZCIZGZFIUMUOVAFAUNVAA + PZVBCIZUQUTVBCACEQJVCUTGUQVBUSCVBULURABUAUBRUCUDUNUQURBGZCIZGZFIVABCFDSVF + VAFVEUTUQVDUSCBULURBAUETRTUFUGUHUIULCFDSUJUK $. + $( $j usage 'sbrim' avoids 'ax-10'; $) + + $( Obsolete version of ~ sbrim as of 20-Nov-2024. (Contributed by NM, + 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + sbrimOLD $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $= ( wi wsb sbim sbf imbi1i bitri ) ABFCDGACDGZBCDGZFAMFABCDHLAMACDEIJK $. - - $d x y $. - $( Substitution in an implication with a variable not free in the - antecedent affects only the consequent. Version of ~ sbrim not - depending on ~ ax-10 , but with disjoint variables. (Contributed by - Wolf Lammen, 28-Jan-2024.) $) - sbrimv $p |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) $= - ( weq wi 19.21 sbrimvlem ) ABCDACDFBGCEHI $. $} ${ @@ -19902,19 +19895,11 @@ any disjoint variable condition (but the version with a disjoint $( Conversion of implicit substitution to explicit substitution (deduction version of ~ sbiev ). Version of ~ sbied with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) - (Revised by Gino Giotto, 10-Jan-2024.) Avoid ~ ax-10 . (Revised by - Wolf Lammen, 28-Jan-2024.) $) + (Revised by Gino Giotto, 10-Jan-2024.) $) sbiedw $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $= - ( wsb wi sbrimv nfim1 weq wb com12 pm5.74d sbiev bitr3i pm5.74ri ) ABDEIZ - CATJABJZDEIACJZABDEFKUAUBDEACDFGLDEMZABCAUCBCNHOPQRS $. - $( $j usage 'sbiedw' avoids 'ax-10' 'ax-11' 'ax-13'; $) - - $( Obsolete version of ~ sbiedw as of 28-Jan-2024. (Contributed by Gino - Giotto, 10-Jan-2024.) (Proof modification is discouraged.) - (New usage is discouraged.) $) - sbiedwOLD $p |- ( ph -> ( [ y / x ] ps <-> ch ) ) $= ( wsb wi sbrim nfim1 weq wb com12 pm5.74d sbiev bitr3i pm5.74ri ) ABDEIZC ATJABJZDEIACJZABDEFKUAUBDEACDFGLDEMZABCAUCBCNHOPQRS $. + $( $j usage 'sbiedw' avoids 'ax-10' 'ax-11' 'ax-13'; $) $} $( Show that the original axiom ~ ax-c7 can be derived from ~ ax-10