From 5cfb2ea7c1297aa80bb7a74481be14e76776cbce Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Sun, 4 Feb 2024 08:41:25 -0800 Subject: [PATCH] Rename syl6eqssr to eqsstrrdi This is in iset.mm and set.mm --- changes-set.txt | 2 +- iset.mm | 22 ++++---- set.mm | 136 ++++++++++++++++++++++++------------------------ 3 files changed, 80 insertions(+), 80 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index 25d98b7928..df59c4b6bd 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -110,12 +110,12 @@ proposed syl6eleqr eleqtrrdi compare to eleqtrri or eleqtrrd proposed syl6ss sstrdi compare to sstri or sstrd proposed syl6sseq sseqtrdi compare to sseqtri or sseqtrd proposed syl6eqss eqsstrdi compare to eqsstri or eqsstrd -proposed syl6eqssr eqsstrrdi compare to eqsstrri or eqsstrrd (Please send any comments on these proposals to the mailing list or make a github issue.) DONE: Date Old New Notes + 4-Feb-24 syl6eqssr eqsstrrdi compare to eqsstrri or eqsstrrd 29-Jan-24 ccatw2s1ccatws2 [same] revised - eliminated unnecessary antecedent 28-Jan-24 ccat2s1fst [same] revised - eliminated unnecessary antecedent 28-Jan-24 ccatw2s1ass [same] revised - eliminated unnecessary antecedent diff --git a/iset.mm b/iset.mm index 21850a4505..acf37b2efc 100644 --- a/iset.mm +++ b/iset.mm @@ -27592,11 +27592,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use $} ${ - syl6eqssr.1 $e |- ( ph -> B = A ) $. - syl6eqssr.2 $e |- B C_ C $. + eqsstrrdi.1 $e |- ( ph -> B = A ) $. + eqsstrrdi.2 $e |- B C_ C $. $( A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) $) - syl6eqssr $p |- ( ph -> A C_ C ) $= + eqsstrrdi $p |- ( ph -> A C_ C ) $= ( eqcomd syl6eqss ) ABCDACBEGFH $. $} @@ -49996,7 +49996,7 @@ We use their notation ("onto" under the arrow). (Contributed by NM, ffvresb $p |- ( Fun F -> ( ( F |` A ) : A --> B <-> A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) ) $= ( wfun cres wf cv cdm wcel cfv wa wral fdm cin dmres inss2 adantl wfn wss - eqsstri syl6eqssr sselda wceq fvres ffvelrn eqeltrrd jca ralrimiva ralimi + eqsstri eqsstrrdi sselda wceq fvres ffvelrn eqeltrrd jca ralrimiva ralimi crn simpl dfss3 sylibr funfn fnssres sylanb sylan2 eleq1d syl5ibr ralimia simpr fnfvrnss syl2anc df-f sylanbrc ex impbid2 ) DEZBCDBFZGZAHZDIZJZVLDK ZCJZLZABMZVKVQABVKVLBJZLZVNVPVKBVMVLVKBVJIZVMBCVJNWABVMOVMDBPBVMQUAUBUCVT @@ -57019,7 +57019,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and 10-Sep-2015.) $) tposss $p |- ( F C_ G -> tpos F C_ tpos G ) $= ( vx wss cdm ccnv c0 csn cun cv cuni cmpt ccom ctpos coss1 cres wceq dmss - cnvss df-tpos unss1 resmpt 4syl resss syl6eqssr coss2 syl sstrd 3sstr4g ) + cnvss df-tpos unss1 resmpt 4syl resss eqsstrrdi coss2 syl sstrd 3sstr4g ) ABDZACAEZFZGHZIZCJHFKZLZMZBCBEZFZUMIZUOLZMZANBNUJUQBUPMZVBABUPOUJUPVADVCV BDUJUPVAUNPZVAUJUKURDULUSDUNUTDVDUPQABRUKURSULUSUMUACUTUNUOUBUCVAUNUDUEUP VABUFUGUHCATCBTUI $. @@ -66604,7 +66604,7 @@ texts assume excluded middle (in which case the two intersection sbthlemi5 $p |- ( ( EXMID /\ ( dom f = A /\ ran g C_ A ) ) -> dom H = A ) $= ( vy wem cv cdm wceq wss wa cdif cun cin cuni cima sbthlem1 difss sstri - crn sseq2 mpbiri dfss sylib uneq1d sbthlemi3 imassrn syl6eqssr sylan9eq + crn sseq2 mpbiri dfss sylib uneq1d sbthlemi3 imassrn eqsstrrdi sylan9eq uneq2d an12s cres ccnv dmeqi dmres df-rn eqcomi ineq2i uneq12i syl6reqr dmun eqtri 3eqtri wcel wdc wral exmidexmid ralrimivw biantrud undifdcss syl6rbbr adantr eqtr4d ) LEMZNZBOZFMZUFZBPZQZQZGNZDUAZBWIRZSZBWGWKWIWAT @@ -98002,7 +98002,7 @@ Infinity and the extended real number system (cont.) iooval2 $p |- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } ) $= ( cxr wcel wa cioo co cv clt wbr crab cr iooval cin inrab2 ressxr sseqin2 - wceq wss mpbi rabeq ax-mp eqtri elioore ssriv syl6eqssr df-ss sylib eqtrd + wceq wss mpbi rabeq ax-mp eqtri elioore ssriv eqsstrrdi df-ss sylib eqtrd syl5reqr ) BDECDEFZBCGHZBAIZJKUNCJKFZADLZUOAMLZABCNZULUQUPMOZUPUSUOADMOZL ZUQUOADMPUTMSZVAUQSMDTVBQMDRUAUOAUTMUBUCUDULUPMTUSUPSULUPUMMURAUMMUNBCUEU FUGUPMUHUIUKUJ $. @@ -119261,7 +119261,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) wa c0 eluzfz1 syl rspcdva adantr subidd sum0 syl6reqr oveq2 adantl syl6eq cv sumeq1d wi eqeq1 eqeq1d imbi12d vtoclg imp sylan oveq2d 3eqtr4d cz cfn fzo0 eluzel2 eluzelz fzofig syl2anc wral elfzofz fzofzp1 fsumsub eluzp1m1 - cbvsumv fzoval fzossfz syl6eqssr sselda adantlr syldan fsum1p syl5eqr wss + cbvsumv fzoval fzossfz eqsstrrdi sselda adantlr syldan fsum1p syl5eqr wss simpr fzp1ss fsumm1 peano2zd fsumshftm ax-1cn pncan sylancl oveq1d eqtr4d 1zzd sylan2 fsumcl eluzfz2 addcomd eqtr3d 3eqtr3d oveq12d pnpcan2d 3eqtrd zcnd eqtrd wo uzp1 mpjaodan ) AJIQZIJUARZCDUBRZFUCZEHUBRZQJIUDUERZUFUGSZA @@ -131637,7 +131637,7 @@ class of all (base sets of) groups is proper. (Contributed by Mario structcnvcnv $p |- ( F Struct X -> `' `' F = ( F \ { (/) } ) ) $= ( cstr wbr ccnv c0 csn cdif wss cin wceq wcel cvv cxp 0nelxp cnvcnv eqsstri wn inss2 cnvss sseli mto disjsn mpbir cnvcnvss reldisj ax-mp mpbi wrel wfun - wb a1i structn0fun funrel syl dfrel2 sylib difss mp2b syl6eqssr eqssd ) ABC + wb a1i structn0fun funrel syl dfrel2 sylib difss mp2b eqsstrrdi eqssd ) ABC DZAEZEZAFGZHZVDVFIZVBVDVEJFKZVGVHFVDLZRVIFMMNZLMMOVDVJFVDAVJJVJAPAVJSQUAUBV DFUCUDVDAIVHVGUKAUEVDVEAUFUGUHULVBVFVFEZEZVDVBVFUIZVLVFKVBVFUJVMABUMVFUNUOV FUPUQVFAIVKVCIVLVDIAVEURVFATVKVCTUSUTVA $. @@ -136684,7 +136684,7 @@ F C_ ( CC X. X ) ) $= txss12 $p |- ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) C_ ( B tX D ) ) $= ( vx vy wcel wa wss cv cxp cmpo crn ctg cfv ctx co cvv eqid txbasex resss - cres resmpo syl6eqssr adantl rnss syl tgss syl2an2r wceq ssexg txval an4s + cres resmpo eqsstrrdi adantl rnss syl tgss syl2an2r wceq ssexg txval an4s syl2an ancoms adantr 3sstr4d ) BEIZDFIZJZABKZCDKZJZJZGHACGLHLMZNZOZPQZGHB DVGNZOZPQZACRSZBDRSZVBVLTIVEVIVLKZVJVMKGHVLBDEFVLUAZUBVFVHVKKZVPVEVRVBVEV HVKACMZUDVKGHBDACVGUEVKVSUCUFUGVHVKUHUIVIVLTUJUKVEVBVNVJULZVCUTVDVAVTVCUT @@ -136696,7 +136696,7 @@ F C_ ( CC X. X ) ) $= txbasval $p |- ( ( R e. V /\ S e. W ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( R tX S ) ) $= ( vu vv vm vn vx vy wcel wa cv cxp ctg cfv cvv wss wceq ciun cmpo crn ctx - co eqid txbasex cres bastg resmpo syl2an resss syl6eqssr rnss syl wral wf + co eqid txbasex cres bastg resmpo syl2an resss eqsstrrdi rnss syl wral wf cuni wex eltg3 bi2anan9 exdistrv an4 xpeq12i xpiundir xpiundi a1i iuneq2i uniiun 3eqtri txvalex adantr ad2antrr ssel2 anim12i an4s sylan2 ralrimiva txopn anassrs tgiun syl2anc fveq2d 3eqtr4d eleqtrd eqeltrid xpeq12 eleq1d diff --git a/set.mm b/set.mm index 4716c10c71..d47b35efb5 100644 --- a/set.mm +++ b/set.mm @@ -37492,11 +37492,11 @@ technically classes despite morally (and provably) being sets, like ` 1 ` $} ${ - syl6eqssr.1 $e |- ( ph -> B = A ) $. - syl6eqssr.2 $e |- B C_ C $. + eqsstrrdi.1 $e |- ( ph -> B = A ) $. + eqsstrrdi.2 $e |- B C_ C $. $( A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.) $) - syl6eqssr $p |- ( ph -> A C_ C ) $= + eqsstrrdi $p |- ( ph -> A C_ C ) $= ( eqcomd syl6eqss ) ABCDACBEGFH $. $} @@ -55211,7 +55211,7 @@ the restriction (of the relation) to the singleton containing this $( Sufficient condition for inclusion among two functions in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $) mptss $p |- ( A C_ B -> ( x e. A |-> C ) C_ ( x e. B |-> C ) ) $= - ( wss cmpt cres resmpt resss syl6eqssr ) BCEABDFACDFZBGKACBDHKBIJ $. + ( wss cmpt cres resmpt resss eqsstrrdi ) BCEABDFACDFZBGKACBDHKBIJ $. $} ${ @@ -64172,7 +64172,7 @@ in the range of the function (the implication "to the right" is always ffvresb $p |- ( Fun F -> ( ( F |` A ) : A --> B <-> A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) ) $= ( wfun cres wf cv cdm wcel cfv wa wral fdm cin dmres inss2 adantl wfn wss - eqsstri syl6eqssr sselda wceq fvres ffvelrn eqeltrrd jca ralrimiva ralimi + eqsstri eqsstrrdi sselda wceq fvres ffvelrn eqeltrrd jca ralrimiva ralimi crn simpl dfss3 sylibr funfn fnssres sylanb sylan2 eleq1d syl5ibr ralimia simpr fnfvrnss syl2anc df-f sylanbrc ex impbid2 ) DEZBCDBFZGZAHZDIZJZVLDK ZCJZLZABMZVKVQABVKVLBJZLZVNVPVKBVMVLVKBVJIZVMBCVJNWABVMOVMDBPBVMQUAUBUCVT @@ -77181,7 +77181,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and 10-Sep-2015.) $) tposss $p |- ( F C_ G -> tpos F C_ tpos G ) $= ( vx wss cdm ccnv c0 csn cun cv cuni cmpt ccom ctpos coss1 cres wceq dmss - cnvss df-tpos unss1 resmpt 4syl resss syl6eqssr coss2 syl sstrd 3sstr4g ) + cnvss df-tpos unss1 resmpt 4syl resss eqsstrrdi coss2 syl sstrd 3sstr4g ) ABDZACAEZFZGHZIZCJHFKZLZMZBCBEZFZUMIZUOLZMZANBNUJUQBUPMZVBABUPOUJUPVADVCV BDUJUPVAUNPZVAUJUKURDULUSDUNUTDVDUPQABRUKURSULUSUMUACUTUNUOUBUCVAUNUDUEUP VABUFUGUHCATCBTUI $. @@ -86605,7 +86605,7 @@ the first case of his notation (simple exponentiation) and subscript it $( Lemma for ~ sbth . (Contributed by NM, 22-Mar-1998.) $) sbthlem5 $p |- ( ( dom f = A /\ ran g C_ A ) -> dom H = A ) $= ( cv cdm wceq wss cdif cun cin cima dfss eqtri crn sbthlem1 difss sstri - wa sseq2 mpbiri sylib uneq1d sbthlem3 imassrn syl6eqssr uneq2d sylan9eq + wa sseq2 mpbiri sylib uneq1d sbthlem3 imassrn eqsstrrdi uneq2d sylan9eq cuni cres ccnv dmeqi dmun dmres df-rn eqcomi ineq2i syl6reqr undif mpbi uneq12i syl6eq ) EKZLZBMZFKZUAZBNZUEZGLZDUOZBVQOZPZBVOVSVQVJQZVRVMQZPZV PVKVNVSVTVRPWBVKVQVTVRVKVQVJNZVQVTMVKWCVQBNZVQBVLCVIVQROZRZOBABCDEFHIUB @@ -96828,7 +96828,7 @@ suc suc ( ( rank ` A ) u. ( rank ` B ) ) $= 18-Sep-2006.) $) rankxpl $p |- ( ( A X. B ) =/= (/) -> ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) $= - ( cxp c0 wne cun crnk cfv cuni unixp xpex uniex rankuniss sstri syl6eqssr + ( cxp c0 wne cun crnk cfv cuni unixp xpex uniex rankuniss sstri eqsstrrdi fveq2d ) ABEZFGZABHZIJSKZKZIJZSIJZTUCUAIABLRUDUBIJUEUBSABCDMZNOSUFOPQ $. $( An upper bound on the rank of a Cartesian product. (Contributed by NM, @@ -110920,7 +110920,7 @@ Tarski classes ( ~ df-tsk ), and Grothendieck universes ( ~ df-gru ). We winafp $p |- ( ( A e. InaccW /\ A =/= _om ) -> ( aleph ` A ) = A ) $= ( vx vy vz cwina wcel com wne wa cale cfv wceq wlim winalim2 cvv ad2antll cv ccf fveq2d eqtr3d wss con0 vex limelon mpan alephle syl simprl sseqtrd - alephsing csdm wbr wrex wral elwina simp2bi ad2antrr cfle syl6eqssr eqssd + alephsing csdm wbr wrex wral elwina simp2bi ad2antrr cfle eqsstrrdi eqssd c0 exlimddv ) AEFZAGHZIZBQZJKZALZVFMZIZAJKZALBBANVEVJIZVGVKAVLVFAJVLVFAVL VFVGAVIVFVGUAZVEVHVIVFUBFZVMVFOFVIVNBUCVFOUDUEVFUFUGPVEVHVIUHZUIVLAVFRKZV FVLARKZVPAVLVGRKZVQVPVLVGARVOSVIVRVPLVEVHVFUJPTVCVQALZVDVJVCAVAHVSCQDQUKU @@ -111310,7 +111310,7 @@ prove that every set is contained in a weak universe in ZF (see c1o sstri wceq simprl fvex uniex unex prex mptex rnex iunex unieq uneq12d weq pweq preq12d preq2 cbvmptv preq1 mpteq2dv syl5eq rneqd cbviunv mpteq1 uneq2d iuneq12d frsucmpt2w sylancl sseqtrrd fvssunirn sseqtrri rexlimdvaa - id syl5bi ralrimiv dftr3 sylibr con0 1on unexg mpan2 fveq1i syl syl6eqssr + id syl5bi ralrimiv dftr3 sylibr con0 1on unexg mpan2 fveq1i syl eqsstrrdi fr0g unssbd ssn0 ssiun2s sseqtrrid sstrd unssad vpwex vuniex simprd fveq2 1n0 prss sseq2d vtoclga findsg sseldd wi imbi12d eqeltri word ordom ssidd simpld simplrl ordunel mp3an2i suceq fveq2d sseq12d sstr2 syl5com syl2anc @@ -136166,7 +136166,7 @@ the expression make the whole thing evaluate to zero (on both sides), iooval2 $p |- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } ) $= ( cxr wcel wa cioo co cv clt wbr crab cr iooval cin inrab2 ressxr sseqin2 - wss wceq rabeqi eqtri elioore ssriv syl6eqssr df-ss sylib syl5reqr eqtrd + wss wceq rabeqi eqtri elioore ssriv eqsstrrdi df-ss sylib syl5reqr eqtrd mpbi ) BDECDEFZBCGHZBAIZJKUMCJKFZADLZUNAMLZABCNZUKUPUOMOZUOURUNADMOZLUPUN ADMPUNAUSMMDSUSMTQMDRUJUAUBUKUOMSURUOTUKUOULMUQAULMUMBCUCUDUEUOMUFUGUHUI $. @@ -168106,7 +168106,7 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ wa c0 eluzfz1 syl rspcdva adantr subidd sum0 syl6reqr oveq2 adantl syl6eq cv fzo0 sumeq1d wi eqeq1 eqeq1d imbi12d vtoclg sylan oveq2d 3eqtr4d fzofi imp cfn a1i wral elfzofz fzofzp1 fsumsub cbvsumv eluzel2 eluzp1m1 eluzelz - cz fzoval fzossfz syl6eqssr sselda adantlr syldan fsum1p simpr wss fzp1ss + cz fzoval fzossfz eqsstrrdi sselda adantlr syldan fsum1p simpr wss fzp1ss syl5eqr fsumm1 1zzd peano2zd fsumshftm ax-1cn pncan sylancl oveq1d eqtr4d zcnd sylan2 fsumcl eluzfz2 addcomd eqtr3d 3eqtr3d oveq12d pnpcan2d 3eqtrd eqtrd wo uzp1 mpjaodan ) AJIQZIJUARZCDUBRZFUCZEHUBRZQJIUDUERZUFUGSZAYBULZ @@ -194826,7 +194826,7 @@ class of all (base sets of) groups is proper. (Contributed by Mario structcnvcnv $p |- ( F Struct X -> `' `' F = ( F \ { (/) } ) ) $= ( cstr wbr ccnv c0 csn cdif wss cin wceq wcel cvv cxp 0nelxp cnvcnv eqsstri wn inss2 cnvss sseli mto disjsn mpbir cnvcnvss reldisj ax-mp mpbi wrel wfun - wb a1i structn0fun funrel syl dfrel2 sylib difss mp2b syl6eqssr eqssd ) ABC + wb a1i structn0fun funrel syl dfrel2 sylib difss mp2b eqsstrrdi eqssd ) ABC DZAEZEZAFGZHZVDVFIZVBVDVEJFKZVGVHFVDLZRVIFMMNZLMMOVDVJFVDAVJJVJAPAVJSQUAUBV DFUCUDVDAIVHVGUKAUEVDVEAUFUGUHULVBVFVFEZEZVDVBVFUIZVLVFKVBVFUJVMABUMVFUNUOV FUPUQVFAIVKVCIVLVDIAVEURVFATVKVCTUSUTVA $. @@ -195534,7 +195534,7 @@ C_ dom ( S sSet <. I , E >. ) ) $= original structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) $) ressbasss $p |- ( Base ` R ) C_ B $= - ( cvv wcel cbs cfv wss cin ressbas inss2 syl6eqssr wn c0 cress reldmress + ( cvv wcel cbs cfv wss cin ressbas inss2 eqsstrrdi wn c0 cress reldmress co ovprc2 syl5eq fveq2d base0 0ss eqsstrri syl6eqss pm2.61i ) AGHZCIJZBKU IUJABLBABCGDEFMABNOUIPZUJQIJZBUKCQIUKCDARTQEDARSUAUBUCULQBUDBUEUFUGUH $. $} @@ -216211,7 +216211,7 @@ net proof size (existence part)? $) 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) $) tsrdir $p |- ( A e. TosetRel -> A e. DirRel ) $= ( ctsr wcel cdir wrel cid cuni cres wss ccom cxp ccnv cps syl jca wceq eqid - wa eqsstrrid eqsstrrd tsrps psrel cin psref2 inss1 syl6eqssr cdm crn psdmrn + wa eqsstrrid eqsstrrd tsrps psrel cin psref2 inss1 eqsstrrdi cdm crn psdmrn pstr2 simpld sqxpeqd cun istsr simprbi relcoi2 cnvresid cnvss coss1 relcoi1 relcnv ax-mp relcnvfld reseq2d coss2 unssd sstrd isdir mpbir2and ) ABCZADCA EZFAGGZHZAIZRAAJAIZVLVLKZALZAJZIZRVJVKVNVJAMCZVKAUAZAUBNZVJVTVNWAVTVMAVQUCA @@ -226060,7 +226060,7 @@ operation is a permutation group (group consisting of permutations), see -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) ) $= ( wcel cid cres csn csubg cfv cgrp cbs wss wa idressubgsymg cress co cvv eqid pgrpsubgsymgbi cin wceq snex ressbas mp1i inss2 eqcomi eleq1i biimpi - syl6eqssr adantl anim12ci ex sylbid mpd ) ADGZHAIZJZCKLGZBMGZBNLZCNLZOZPZ + eqsstrrdi adantl anim12ci ex sylbid mpd ) ADGZHAIZJZCKLGZBMGZBNLZCNLZOZPZ ACDEQURVAUTVDOZCUTRSZMGZPZVFAVDUTCDEVDUAZUBURVJVFURVEVJVBURVCUTVDUCZVDUTT GVLVCUDURUSUEUTVDBTCFVKUFUGUTVDUHULVIVBVGVIVBVHBMBVHFUIUJUKUMUNUOUPUQ $. $} @@ -226973,7 +226973,7 @@ operation is a permutation group (group consisting of permutations), see ( wcel cv cid cdif cdm wss cfv wceq difeq1 dmeqd sseq1d c0 vy crab cplusg vz cress co c0g cbs ssrab2 sseqtri a1i cgrp symggrp eqid grpidcl syl cres eqidd symgid difeq1d resss ssdif0 mpbi dmeqi dm0 eqtri 0ss eqsstri elrabd - syl6eqssr biid elrab w3a 3ad2ant1 simp2l simp3l grpcl syl3anc ccom symgov + eqsstrrdi biid elrab w3a 3ad2ant1 simp2l simp3l grpcl syl3anc ccom symgov wa syl2anc cun mvdco simp2r simp3r unssd eqsstrd syl3anb cminusg grpinvcl sstrid simprl syl2an2r ccnv symginv ad2antrl wf1o symgbasf1o eqtrd simprr f1omvdcnv sylan2b issubgrpd2 ) CEIZUAUDAJZKLZMZFNZABUBZDUCOZDXJUEUFZDDUGO @@ -236142,7 +236142,7 @@ elements of arbitrarily large orders (so ` E ` is zero) but no elements fof mrcssidd fssd wf1 f1of1 ad2antll cnvimass fssdm f1ss f1f fco oppgsubm ffvelrnda mrccl submcl 3expb sylan cress ccmn cntzspan wb submcmn2 sselda mpbid cntzi oppgplus syl6reqr anasss seqfeq4 mpbird gsumval3 cfn oppgcntz - ccntz oppgbas syl6sseq cdm suppssdm syl6eqssr fssdmd f1ofo sseq2d exlimdv + ccntz oppgbas syl6sseq cdm suppssdm eqsstrrdi fssdmd f1ofo sseq2d exlimdv forn expr expimpd wo fsuppimpd eqeltrrd fz1f1o mpjaod ) ADUEUFHUGUHZUIZUJ UKZFDULUMZEDULUMZUKZUVAUNSZUOTZUPUVFUQUMZUVAUAURZUSZUAUTZVAZAUVBUVEAUVBVA ZFUBBHVBZULUMZEUVNULUMZUVCUVDAUVOUVPUKUVBAUVOHUVPAFVCTZBGTZUVOHUKAEVCTZUV @@ -257263,7 +257263,7 @@ series in the subring which are also polynomials (in the parent ring). wi wb soeq2 mpbird soinxp sylib cdif copws fvexi pltfval ax-mp difundir cun c0 resss ssdif0 mpbi uneq2i 3eqtri opsrtoslem1 difeq1d wrel relinxp un0 a1i cop df-br vex ideq bitr3i brin simprbi brxp sonr syl2im pm2.01d - wn ex breq2 syl6bb notbid syl5ibcom syl5bi con2d opex syl5eq syl6eqssr + wn ex breq2 syl6bb notbid syl5ibcom syl5bi con2d opex syl5eq eqsstrrdi eldif mpbiran syl6ibr relssdv disj2 disj3 3eqtr4a soeq1 opsrbas reseq2d sylibr mpbid ssun2 sseqtrrd sylanbrc ) AQULUMZQUNUMZUOZUPUUQUQZPURZQUSU TZAGUURUOZUUSAUVCGBCDVAZGGVBZVCZUOZAGUVDUOZUVGAUVHJULUMZIVDVHZUVDUOZIVE @@ -267413,7 +267413,7 @@ is based on direct sums of abelian groups ("We define on [the direct sum of O'Rear, 11-Jan-2015.) $) dsmmsubg $p |- ( ph -> H e. ( SubGrp ` P ) ) $= ( va vb cfv wcel wceq cgrp eqid cplusg cress co c0g eqidd cdsmm cbs cprds - cv wne cdm crab cfn cvv fex syl2anc dsmmbase syl ssrab2 syl6eqssr 3sstr4g + cv wne cdm crab cfn cvv fex syl2anc dsmmbase syl ssrab2 eqsstrrdi 3sstr4g fveq2i cmnd wss grpmnd ssriv fss sylancl dsmm0cl w3a 3ad2ant1 simp2 simp3 wf dsmmacl wa cminusg prdsgrpd adantr sselda grpinvcl simpr wfn dsmmelbas mpbid simprd ad2antrr prdsinvgd2 adantrr fveq2 ad2antll ffvelrnda adantlr @@ -287655,7 +287655,7 @@ converges to zero (in the standard topology on the reals) with this cnclsi $p |- ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( F " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` K ) ` ( F " S ) ) ) $= ( ccn co wcel wss wa ccl cfv cima ccnv ctop cntop1 adantr cuni sseqtrrd - cnvimass wf eqid cnf fssdm cdm cin wceq simpr fdmd sylib dminss syl6eqssr + cnvimass wf eqid cnf fssdm cdm cin wceq simpr fdmd sylib dminss eqsstrrdi sseqin2 clsss syl3anc imassrn frnd sstrid cncls2i syldan sstrd wfun ffund crn wb clsss3 sylan funimass3 syl2anc mpbird ) BCDGHIZAEJZKZBACLMZMZNBANZ DLMMZJZVPBOZVRNZJZVNVPVTVQNZVOMZWAVNCPIZWCEJAWCJVPWDJVLWEVMBCDQZRVNEDSZWC @@ -293269,7 +293269,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually txss12 $p |- ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) C_ ( B tX D ) ) $= ( vx vy wcel wa wss cv cxp cmpo crn ctg cfv ctx co cvv eqid txbasex resss - cres resmpo syl6eqssr adantl rnss syl tgss syl2an2r wceq ssexg txval an4s + cres resmpo eqsstrrdi adantl rnss syl tgss syl2an2r wceq ssexg txval an4s syl2an ancoms adantr 3sstr4d ) BEIZDFIZJZABKZCDKZJZJZGHACGLHLMZNZOZPQZGHB DVGNZOZPQZACRSZBDRSZVBVLTIVEVIVLKZVJVMKGHVLBDEFVLUAZUBVFVHVKKZVPVEVRVBVEV HVKACMZUDVKGHBDACVGUEVKVSUCUFUGVHVKUHUIVIVLTUJUKVEVBVNVJULZVCUTVDVAVTVCUT @@ -293281,7 +293281,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually txbasval $p |- ( ( R e. V /\ S e. W ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( R tX S ) ) $= ( vu vv vm vn vx vy wcel wa cv cxp ctg cfv wss wceq ciun cvv ctx cmpo crn - co eqid txval cres bastg resmpo syl2an resss syl6eqssr rnss syl wral cuni + co eqid txval cres bastg resmpo syl2an resss eqsstrrdi rnss syl wral cuni wf wex eltg3 bi2anan9 exdistrv an4 uniiun xpeq12i xpiundir xpiundi 3eqtri a1i iuneq2i ovex ssel2 anim12i an4s txopn anassrs ralrimiva tgiun sylancr sylan2 txbasex tgidm fveq2d 3eqtr4d adantr eleqtrd eqeltrid xpeq12 eleq1d @@ -296705,7 +296705,7 @@ indistinguishability map (in the terminology of ~ qtoprest ). ( `' F " ( F " U ) ) = U ) $= ( vz ctopon cfv wcel wa ccnv cima cv wb wfn syl adantr wceq kqffn kqfvima elpreima 3expa biimprd expimpd sylbid ssrdv cdm cin toponss fndm sseqtrrd - wss sseqin2 sylib dminss syl6eqssr eqssd ) EFIJZKZCEKZLZDMDCNZNZCVCHVECVC + wss sseqin2 sylib dminss eqsstrrdi eqssd ) EFIJZKZCEKZLZDMDCNZNZCVCHVECVC HOZVEKZVFFKZVFDJVDKZLZVFCKZVAVGVJPZVBVADFQZVLABDEUTFGUAZFVFVDDUCRSVCVHVIV KVCVHLVKVIVAVBVHVKVIPABVFCDEFGUBUDUEUFUGUHVCCDUIZCUJZVEVCCVOUNVPCTVCCFVOC EFUKVAVOFTZVBVAVMVQVNFDULRSUMCVOUOUPCDUQURUS $. @@ -296736,7 +296736,7 @@ indistinguishability map (in the terminology of ~ qtoprest ). cldss fndm eqtrd sseqtrd dfss4 sylib imaeq2d ineq2d simpll difeq1d cldopn sseqtrrd eqeltrd kqdisj syl2anc eqtr3d syl5eq eleq2d syl5bbr mtbiri imnan sylibr eldif baibr simpr kqfvima syl3anc bitrd sylibd sylbid ssrdv dminss - con1bid expimpd sseqin2 syl6eqssr eqssd ) EFUBHZIZCEUDHIZJZDUEDCKZKZCWRUA + con1bid expimpd sseqin2 eqsstrrdi eqssd ) EFUBHZIZCEUDHIZJZDUEDCKZKZCWRUA WTCWRUAUFZWTIZXAFIZXADHZWSIZJZXACIZWPXBXFLZWQWPDFUCZXHABDEWOFGUGZFXAWSDUH UIMWRXCXEXGWRXCJZXEXDDFCNZKZIZOZXGXKXEXNJZOXEXOUJXKXPXDPIZXDUKXPXDWSXMQZI XKXQXDWSXMULXKXRPXDXKXRXMWSQZPWSXMUMXKXMDFXLNZKZQZXSPXKYAWSXMXKXTCDXKCFRZ @@ -300110,7 +300110,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the ( F : Y --> X /\ B C_ C ) ) -> ( ( X FilMap F ) ` B ) C_ ( ( X FilMap F ) ` C ) ) $= ( vy wcel cfbas cfv wss wa cmpt crn cfg co eqid fbasrn syl3anc wceq wf cv - w3a cima simpl2 simprl simpl1 simpl3 cres resmpt ad2antll resss syl6eqssr + w3a cima simpl2 simprl simpl1 simpl3 cres resmpt ad2antll resss eqsstrrdi cfm rnss syl fgss fmval 3sstr4d ) EAHZBFIJZHZCVAHZUCZFEDUAZBCKZLZLZEGBDGU BUDZMZNZOPZEGCVIMZNZOPZBEDUNPZJZCVPJZVHVKEIJZHZVNVSHZVKVNKZVLVOKVHVBVEUTV TUTVBVCVGUEZVDVEVFUFZUTVBVCVGUGZGBVKDAFEVKQRSVHVCVEUTWAUTVBVCVGUHZWDWEGCV @@ -311443,7 +311443,7 @@ the half element (corresponding to half the distance) is also in this c2 imass2 sseq1 elfg syl12anc cfiluexsm syl3anc funimass2 ex reximdv sylc rspcev ralrimiva jca simprl sseq2d rexbidv simp-4r rspcdva nfv nfcv nfre1 simprd nfral nfan ad4antr fbelss sylancom xpss12 simp-6r sseqtrrd ralrimi - r19.29r cin sseqin2 biimpi adantl dminss syl6eqssr adantr reximi syl sstr + r19.29r cin sseqin2 biimpi adantl dminss eqsstrrdi adantr reximi syl sstr sstrd r19.41v sylbir simp-5r biimpa r19.29a wb iscfilu mpbir2and impbida ) FUBUCZDFUDJKZLZCFFUEZEUFMZUGJKZCFUHJKZDBNZUULUEZUIZOANZUJMZPZBCQZARUKZL ZUUGUUJLZUUKUUSUUGUUIFULJKZUUJUUKDEFGHUMZUUICFUNUOUVAUURARUVAUUORKZLZDUPZ @@ -312808,7 +312808,7 @@ definition of norm (which itself uses the metric). (Contributed by tngtopn $p |- ( ( G e. V /\ N e. W ) -> J = ( TopOpen ` T ) ) $= ( vx vy wcel cfv wss wceq cmopn cdm eqid syl wa cts ctopn tngtset cbs cpw cxmet crn cuni cv cbl ctg df-mopn dmmptss sseli cxp csg cds tngds syl6eqr - ccom adantl dmeqd dmcoss cminusg cplusg grpsubfval ovex sseqtri syl6eqssr + ccom adantl dmeqd dmcoss cminusg cplusg grpsubfval ovex sseqtri eqsstrrdi co dmmpo adantr dmss dmxpid syl6sseq simpr xmetunirn sylib mopnuni tngbas ad2antlr 3sstr3d sspwuni sylibr ex syl5 wn c0 ndmfv 0ss syl6eqss pm2.61d1 eqsstrid eqsstrrd topnid eqtrd ) CFMZEGMZUAZDBUBNZBUCNZABCDEFGHIJUDZWTXAB @@ -340046,7 +340046,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvaddf $p |- ( ph -> ( S _D ( F oF + G ) ) = ( ( S _D F ) oF + ( S _D G ) ) ) $= ( vx co caddc cfv cc wf wcel syl mpbid adantr vy cdv cof cv cvv cr dvbsss - cpr cdm syl6eqssr ssexd dvfg feq2d wss recnprss wa addcl adantl inidm off + cpr cdm eqsstrrdi ssexd dvfg feq2d wss recnprss wa addcl adantl inidm off ffnd dvbss ccnfld ctopn fvexd eleq2d biimpar wfun ffun funfvbrb 4syl eqid wbr wb dvaddbr reldv releldmi eqelssd eqidd dvadd eqcomd offveq ) ABCUBLZ BDUBLZMUCZLBCDWELZUBLZAKEKUDZWCNZWHWDNZMWCWDWGUEAEBUFOUHZFAEWCUIZBIBCUGUJ @@ -340065,7 +340065,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvmulf $p |- ( ph -> ( S _D ( F oF x. G ) ) = ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) ) $= ( vx cmul co cfv wcel cc wf adantr syl cvv vy cv cof cdv caddc wa wss cdm - cmpt dvbsss syl6eqssr cr cpr eleq2d biimpar dvmul mpteq2dva dvfg recnprss + cmpt dvbsss eqsstrrdi cr cpr eleq2d biimpar dvmul mpteq2dva dvfg recnprss mulcl adantl ssexd inidm off dvbss wbr ccnfld ctopn wfun wb ffun funfvbrb fvexd 3syl mpbid eqid dvmulbr reldv eqelssd feq2d feqmptd offval2 3eqtr4d releldmi ovexd ) AKEKUBZBCDLUCZMZUDMZNZUIKEWFBCUDMZNZWFDNZLMZWFBDUDMZNZWF @@ -340251,7 +340251,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvcof $p |- ( ph -> ( T _D ( F o. G ) ) = ( ( ( S _D F ) o. G ) oF x. ( T _D G ) ) ) $= ( vx cfv wcel cc wf adantr syl vy cv ccom cdv co cmpt cmul cof wa wss cdm - dvbsss syl6eqssr cr ffvelrnda wceq eleqtrrd eleq2d biimpar dvco mpteq2dva + dvbsss eqsstrrdi cr ffvelrnda wceq eleqtrrd eleq2d biimpar dvco mpteq2dva cpr dvfg recnprss fco syl2anc dvbss wbr ccnfld ctopn cvv wfun wb funfvbrb fvexd ffun 4syl mpbid eqid dvcobr reldv eqelssd feq2d feqmptd ssexd fveq2 releldmi fmptco offval2 3eqtr4d ) ANGNUBZCDEUCZUDUEZOZUFNGWKEOZBDUDUEZOZW @@ -340482,7 +340482,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ( S _D ( x e. Y |-> A ) ) = ( x e. Y |-> B ) ) $= ( cmpt cres cdv cc co cr cpr wcel cdm wceq fmpttd dmeqd eqid dmmptd eqtrd wf dvres3a syl22anc cin rescom resres reseq2d syl5eq wfn ffn fnresdm 3syl - eqtri reseq1d inss2 syl6eqssr resmptd 3eqtr3d oveq2d wral ralrimiva fnmpt + eqtri reseq1d inss2 eqsstrrdi resmptd 3eqtr3d oveq2d wral ralrimiva fnmpt eqtr4d ) AEBHCQZERZSUAZTVOSUAZERZEBICQZSUABIDQZAEUBTUCUDHTVOULZHFUDVRUEZH UFVQVSUFKABHCTNUGZLAWCBHDQZUEHAVRWEPUHABWEHDGWEUIZOUJUKHEVOFJUMUNAVPVTESA VOHRZERZVOIRZVPVTAWHVOEHUOZRZWIWHVPHRWKVOHEUPVOEHUQVDAWJIVOMURUSAWGVOEAWB @@ -340576,7 +340576,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvmptres2 $p |- ( ph -> ( S _D ( x e. Z |-> A ) ) = ( x e. Y |-> B ) ) $= ( cc cmpt cres cdv co cnt cfv wss wceq cpr wcel recnprss syl fmpttd cdm - wf cr dmeqd wral ralrimiva dmmptg eqtrd dvbsss syl6eqssr sstrd syl22anc + wf cr dmeqd wral ralrimiva dmmptg eqtrd dvbsss eqsstrrdi sstrd syl22anc dvres resmptd oveq2d reseq1d reseq2d ctop cuni crest cnfldtopon sylancr ctopon resttopon eqeltrid topontop toponuni sseqtrd eqid ntrss2 syl2anc eqsstrrd 3eqtrd 3eqtr3d ) AEBICUAZKUBZUCUDZEWHUCUDZKFUEUFUFZUBZEBKCUAZU @@ -340612,7 +340612,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvmptcmul $p |- ( ph -> ( S _D ( x e. X |-> ( C x. A ) ) ) = ( x e. X |-> ( C x. B ) ) ) $= ( cmul co cmpt cc0 cc wcel cfv cdv caddc cv adantr wa 0cnd ccnfld ctopn - crest dvmptc cdm dmeqd wral ralrimiva dmmptg syl eqtrd dvbsss syl6eqssr + crest dvmptc cdm dmeqd wral ralrimiva dmmptg syl eqtrd dvbsss eqsstrrdi wceq eqid cnt ctop cuni wss ctopon cnfldtopon cr cpr recnprss resttopon sylancr topontop toponuni sseqtrd ntrss2 fmpttd dvbssntr eqsstrrd eqssd syl2anc dvmptres2 dvmptmul mul02d oveq1d dvmptcl mulcld addid2d mulcomd @@ -340674,7 +340674,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvmptcj $p |- ( ph -> ( RR _D ( x e. X |-> ( * ` A ) ) ) = ( x e. X |-> ( * ` B ) ) ) $= ( vy cr ccj cmpt ccom cdv co cfv cc wf wceq wss fmpttd cdm wcel ralrimiva - dmeqd wral dmmptg syl dvbsss syl6eqssr dvcj syl2anc cjf a1i cofmpt oveq2d + dmeqd wral dmmptg syl dvbsss eqsstrrdi dvcj syl2anc cjf a1i cofmpt oveq2d eqtrd cv cpr reelprrecn dvmptcl feqmptd fveq2 fmptco 3eqtr3d ) AKLBFCMZNZ OPZLKVGOPZNZKBFCLQMZOPBFDLQZMAFRVGSFKUAVIVKTABFCRGUBAFVJUCZKAVNBFDMZUCZFA VJVOIUFADEUDZBFUGVPFTAVQBFHUEBFDEUHUIURKVGUJUKVGFULUMAVHVLKOABFCRRLRRLSAU @@ -340912,7 +340912,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by csn cv wf1o f1of syl ffvelrnd ctop wceq ctopon crest wss cnfldtopon cpr wf cr recnprss resttopon sylancr eqeltrid topontop isopn3i eleqtrrd wne syl2anc wa f1ocnv eldifi ffvelrn syl2an anim1i sylibr anasss cdm dvbsss - 3syl eldifsn syl6eqssr sstrd sselda sylan2 sseldd adantr subcld toponss + 3syl eldifsn eqsstrrdi sstrd sselda sylan2 sseldd adantr subcld toponss fssd cc0 eldifsni adantl subeq0ad wf1 wb f1of1 syl12anc bitrd necon3bid f1fveq mpbird divcld limcresi feqmptd reseq1d difss resmpt ax-mp syl6eq cres sseqtrid f1ocnvfv1 cnlimci eqeltrrd dvlem subne0d divne0d sylanbrc @@ -340968,7 +340968,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvcnv $p |- ( ph -> ( S _D `' F ) = ( x e. Y |-> ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) ) ) $= ( cfv cc wcel adantr ccnv cdv co cv cmpt c1 cdiv cdm wf cpr dvfg recnprss - cr syl wss wf1o f1ocnv f1of 3syl dvbsss syl6eqssr sstrd fssd ctopon crest + cr syl wss wf1o f1ocnv f1of 3syl dvbsss eqsstrrdi sstrd fssd ctopon crest cnfldtopon resttopon sylancr eqeltrid toponss syl2anc dvbss wbr f1ocnvfv2 wa wceq sylan ccncf cc0 crn wn ffvelrnda dvcnvlem eqbrtrrd reldv releldmi eqelssd feq2d mpbid feqmptd wfun ffund funbrfv sylc mpteq2dva eqtrd ) ACD @@ -343004,7 +343004,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by dvcnvrelem1 $p |- ( ph -> ( F ` C ) e. ( ( int ` ( topGen ` ran (,) ) ) ` ( F " ( ( C - R ) [,] ( C + R ) ) ) ) ) $= ( cr cfv wcel wa clt wbr wi vx vy cmin co caddc cicc cres crn wceq wrex - cv cima ctg cnt cdv cdm dvbsss syl6eqssr sseldd rpred resubcld readdcld + cv cima ctg cnt cdv cdm dvbsss eqsstrrdi sseldd rpred resubcld readdcld cioo ltsubrpd ltaddrpd lttrd ltled ccncf rescncf sylc evthicc2 wf cncff wss syl ffvelrnd adantr wiso cxr cle rexrd lbicc2 syl3anc w3a wb elicc2 syl2anc mpbir3and isorel biimpd exp32 com4l syl3c fvresd breq12d sylibd @@ -343067,7 +343067,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by crn ctg eqeltri wf1o wfo wceq f1ofo forn 3syl ccncf wf eqsstrrd imassrn cncff frn sseqtrid cuni uniretop unieqi eqtr4i ntrss dvcnvrelem1 fveq2i mp3an2i fveq1i syl6eleqr sseldd cres crest wfun f1of ffun funcnvres ccn - f1ocnv cdv cdm dvbsss syl6eqssr ax-resscn syl6ss cncfss syl2anc wf1 syl + f1ocnv cdv cdm dvbsss eqsstrrdi ax-resscn syl6ss cncfss syl2anc wf1 syl cc f1of1 f1ores ccmp wb tgioo2 eqtri oveq1i cvv cnfldtop sstrd reex a1i restabs syl5eq rpred resubcld readdcld eqid icccmp eqeltrrd sstrid sylc rescncf cncffvrn mpbird cncfcnvcn mpbid cncfcn eleqtrd cle ltled ctopon @@ -349916,7 +349916,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by cima a1i eqnetrd fveq2 dgr0 syl6eq necon3i quotdgr syl3anc 0lt1 breqtrrid breq1d syl5ibrcom pm2.62 sylc breqtrd cn0 cquot co cmul cof cmin plymulcl quotcl2 syl2anc plysubcl eqeltrid dgrcl nn0lt10b mpbid fveq1d fveq1i plyf - 0dgrb wf adantr ffnd cnex inidm offn eqidd cun wss simp3d ssun1 syl6eqssr + 0dgrb wf adantr ffnd cnex inidm offn eqidd cun wss simp3d ssun1 eqsstrrdi snssg mpbird ofmulrt eleqtrrd wfn fniniseg simprd ofval anabss3 ffvelrnda syl5eq subid1d eqtrd fvex fvconst2 3eqtr3d sneqd xpeq2d eqtr4d ) DCUAHZIZ AJIZUBZBJKBHZLZUCZJADHZLZUCYFBMHZKNZBYINZYFYLOPUDZYMYFYLEMHZOPYFBQNZYLYPP @@ -352592,7 +352592,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the syl adantrr resexg eqid fvmpt2 syl2anc fveq1d 3eqtr4d ralrimivva nfv nfcv nffvmpt1 nfral fveq2 eqeq12d ralbidv cbvral sylib r19.21bi fvoveq1 breq1d nffv nfeq ralimi 3syl sylibrd sylan2 anassrs ralimdva reximdva ralimdv cc - ralbi cmap ulmf cdm fdm dmmptss syl6eqssr uzid adantl ssel eluzel2 eleq2s + ralbi cmap ulmf cdm fdm dmmptss eqsstrrdi uzid adantl ssel eluzel2 eleq2s wf cz syl6 syl2imc rexlimdva mpd wfn crn ralrimiva frn rexlimivw sylanbrc fnmpt df-f eqidd ulmcl ulmscl ulm2 fvmptelrn elmapi fssresd ssexd sylancr cnex elmapg mpbird fmpttd 3imtr4d ) ABICUDZFDUEPUFZBICEUGZUDZFEUGZEUEPUFZ @@ -352749,7 +352749,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the cli rspcdva mptex a1i weq fveq1d fvex adantl ffvelrnda eqtr4d climsubc1 eqeltrd oveq12d recnd sylan syldan ffnd ad2antrr syl22anc eqbrtrd cxmet fnfvof mpbird fvexd feqmptd breq1d rspccva culm rgenw fnmpt mp1i dvbsss - ulmf2 fdmd syl6eqssr cpr recnprss sstrd subne0d ulmcl readdcld abs3difd + ulmf2 fdmd eqsstrrdi cpr recnprss sstrd subne0d ulmcl readdcld abs3difd sub4d divsubdird absdivd csn syl6eleq eluzelz ralrimiva climsub climabs fvexi remulcld eqimss2i climconst2 uztrn2 fvconst2 cof ulmscl ccom cres cbl ovresd cnmetdval cxr cnxmet xmetres2 sylancr rpxrd elbl3 crp blcntr @@ -352845,7 +352845,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the ulmdvlem3 $p |- ( ( ph /\ z e. X ) -> z ( S _D G ) ( H ` z ) ) $= ( wcel wa cfv vy vv vu vr vx vn vm vj vs vw cv cdv wbr ccnfld ctopn crest co cnt csn cdif cmin cdiv cmpt climc wss wceq biidd ulmdvlem2 cc recnprss - cdm cr cpr adantr cmap wf ffvelrnda elmapi dvbsss syl6eqssr eqid dvbssntr + cdm cr cpr adantr cmap wf ffvelrnda elmapi dvbsss eqsstrrdi eqid dvbssntr syl eqsstrrd ralrimiva cuz cz uzid syl6eleqr rspcdva sselda cabs clt wral wi crp wrex sylancr cvv ovex syl2anc mpbid uztrn2 weq fveq2 oveq2d fveq1d c2 oveq12d breq1d ralbidv ad2antrr rphalfcl adantl simplr oveq1d fvoveq1d @@ -352931,7 +352931,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the derivative ` H ` . (Contributed by Mario Carneiro, 27-Feb-2015.) $) ulmdv $p |- ( ph -> ( S _D G ) = H ) $= ( cc wcel syl cdv co cdm wf cr cpr dvfg wss recnprss cv wceq biidd wa cfv - ulmdvlem2 dvbsss syl6eqssr ralrimiva cuz uzid syl6eleqr rspcdva dvbss wbr + ulmdvlem2 dvbsss eqsstrrdi ralrimiva cuz uzid syl6eleqr rspcdva dvbss wbr cz ulmdvlem3 vex fvex eqelssd feq2d mpbid ffnd cmpt culm ulmcl wfun ffund breldm adantr funbrfv sylc eqfnfvd ) ABICFUAUBZGAIRWCAWCUCZRWCUDZIRWCUDAC UERUFSZWELCFUGTZAWDIRWCABWDIAICFAWFCRUHLCUITOAICUHZWHDJHDUJZHUKWHULAWHDJA @@ -368874,7 +368874,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 ( cn wcel cvma cfv cc0 wne cv wbr cprime chash c1 wceq c1o cfn wb cvv syl c2 cdvds crab cuni clog cif wreu vmaval neeq1d cen reuen1 wa hash1 eqeq2i eqid prmdvdsfi com 1onn nnfi ax-mp hashen sylancl syl5bbr biimpar iftrued - cuz csn wss simpr en1b sylib ssrab2 syl6eqssr uniexg adantr mpbird prmuz2 + cuz csn wss simpr en1b sylib ssrab2 eqsstrrdi uniexg adantr mpbird prmuz2 cr snssg eluzelre clt eluz2gt1 rplogcld rpne0d eqnetrd ex necon1ai syl5ib iffalse impbid syl5bb bitr4d ) ACDZAEFZGHBIAUAJZBKUBZLFZMNZWOUCZUDFZGUEZG HZWNBKUFZWLWMWTGAWOBWOUNUGUHXBWOOUIJZWLXAWNBKUJWLXCXAWLXCXAWLXCUKZWTWSGXD @@ -371613,7 +371613,7 @@ particular proof approach is due to Cauchy (1821). This is Metamath 100 ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) ) $= ( wcel cfv cc0 wi cc cmgp ccnfld cmhm co cdif csn cxp wss wa cv dchrelbas wne wral cdm cres wceq wfun wf eqid mgpbas cnfldbas adantl ffund funssres - mhmf sylan simpr resss syl6eqssr impbida 0cn fconst6g mp1i reseq2d eqeq1d + mhmf sylan simpr resss eqsstrrdi impbida 0cn fconst6g mp1i reseq2d eqeq1d fdmd wfn wb difss fssres sylancl ffnd syl2anc fvres c0ex fvconst2 eqeq12d eqfnfv ralbiia eldif imbi1i impexp con1b df-ne bitr4i imbi2i 3bitri bitri wn ralbii2 syl6bb 3bitrd pm5.32da bitrd ) AHDPHIUAQZUBUAQZUCUDPZCEUEZRUFU @@ -446782,7 +446782,7 @@ to a member of the subspace (Definition of complete subspace in [Beran] NM, 13-Aug-2002.) (New usage is discouraged.) $) chsupsn $p |- ( A e. CH -> ( \/H ` { A } ) = A ) $= ( vx cch wcel csn chsup cfv cuni cv wss crab cint wceq snssi chsupval2 wa - syl unisng eqimss ancli sseq2 elrab sylibr intss1 ssintub syl6eqssr eqssd + syl unisng eqimss ancli sseq2 elrab sylibr intss1 ssintub eqsstrrdi eqssd eqtrd ) ACDZAEZFGZUJHZBIZJZBCKZLZAUIUJCJUKUPMACNBUJOQUIUPAUIAUODZUPAJUIUI ULAJZPUQUIURUIULAMURACRZULASQTUNURBACUMAULUAUBUCAUOUDQUIAULUPUSBULCUEUFUG UH $. @@ -455855,7 +455855,7 @@ Positive operators (cont.) ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) ) $= ( vx wss cpjh cfv ccom wceq cv chba wral wcel pjcoi adantl pjfi crn pjrni wa cch pjcli ssel2 sylan2 pjid sylancr eqtrd ralrimiva hocofi hoeqi sylib - rneq rncoss syl6eqssr 3sstr3g impbii ) ABFZBGHZAGHZIZUSJZUQEKZUTHZVBUSHZJ + rneq rncoss eqsstrrdi 3sstr3g impbii ) ABFZBGHZAGHZIZUSJZUQEKZUTHZVBUSHZJ ZELMVAUQVEELUQVBLNZTZVCVDURHZVDVFVCVHJUQVBBADCOPVGBUANVDBNZVHVDJDVFUQVDAN VIVBACUBABVDUCUDVDBUEUFUGUHEUTUSURUSBDQACQZUIVJUJUKVAUSRZURRZABVAVKUTRVLU TUSULURUSUMUNACSBDSUOUP $. @@ -462392,7 +462392,7 @@ Class abstractions (a.k.a. class builders) 17-Feb-2017.) $) off2 $p |- ( ph -> ( F oF R G ) : C --> U ) $= ( vz cv cfv co cof cmpt ffnd eqid wcel wa eqidd offval mpteq1d eqtrd wral - cin wf adantr inss1 syl6eqssr ffvelrnd inss2 ralrimivva ovrspc2v syl21anc + cin wf adantr inss1 eqsstrrdi ffvelrnd inss2 ralrimivva ovrspc2v syl21anc sselda fmpt3d ) AUAFUAUBZKUCZVHLUCZGUDZJKLGUEUDZAVLUADEUPZVKUFUAFVKUFAUAD EVIVJGVMKLMNADHKPUGAEILQUGRSVMUHAVHDUIUJVIUKAVHEUIUJVJUKULAUAVMFVKTUMUNAV HFUIZUJZVIHUIVJIUIBUBCUBGUDJUIZCIUOBHUOZVKJUIVODHVHKADHKUQVNPURAFDVHAFVMD @@ -467139,7 +467139,7 @@ Splicing words (substring replacement) 20-Jan-2018.) $) resspos $p |- ( ( F e. Poset /\ A e. V ) -> ( F |`s A ) e. Poset ) $= ( vx vy vz cpo wcel wa cress cvv cv cple cfv wbr wi wral eqid ssralv breq - co wceq w3a cbs ovexd wss cin ressbas inss2 syl6eqssr adantl ispos adantr + co wceq w3a cbs ovexd wss cin ressbas inss2 eqsstrrdi adantl ispos adantr simprbi ralimdv syld sylc ressle anbi12d imbi1d imbi12d 3anbi123d ralbidv wb 2ralbidv syl mpbid sylanbrc ) BGHZACHZIZBAJUAZKHDLZVMVLMNZOZVMELZVNOZV PVMVNOZIZVMVPUBZPZVQVPFLZVNOZIZVMWBVNOZPZUCZFVLUDNZQZEWHQDWHQZVLGHVKBAJUE @@ -467156,7 +467156,7 @@ Splicing words (substring replacement) 20-Jan-2018.) $) resstos $p |- ( ( F e. Toset /\ A e. V ) -> ( F |`s A ) e. Toset ) $= ( vx vy ctos wcel cpo cv cple cfv wbr wo cbs wral eqid adantl istos breqd - ssralv wa cress co tospos resspos sylan wss cin ressbas syl6eqssr simprbi + ssralv wa cress co tospos resspos sylan wss cin ressbas eqsstrrdi simprbi inss2 adantr ralimdv syld sylc wb ressle orbi12d 2ralbidv mpbid sylanbrc ) BFGZACGZUAZBAUBUCZHGZDIZEIZVFJKZLZVIVHVJLZMZEVFNKZODVNOZVFFGVCBHGZVDVGB UDABCUEUFVEVHVIBJKZLZVIVHVQLZMZEVNOZDVNOZVOVEVNBNKZUGZVTEWCOZDWCOZWBVDWDV @@ -468232,7 +468232,7 @@ real number multiplication operation (this has to be defined in the main ( va vb vc wcel co wa cv cfv wbr cbs wral cvv adantr wceq eqid syl sseldd c0 comnd cress cmnd ctos cple cplusg wi simpr omndtos wn reldmress ovprc2 fveq2d adantl syl6eqr wne c0g mndidcl ne0d ad2antlr neneqd condan resstos - base0 syl2anc w3a simplll wss cin ressbas inss2 syl6eqssr simplr1 simplr2 + base0 syl2anc w3a simplll wss cin ressbas inss2 eqsstrrdi simplr1 simplr2 ad2antrr simplr3 ressle breqd biimpar omndadd syl131anc wb oveqd breq123d ressplusg mpbid ex ralrimivvva isomnd syl3anbrc ) BUAFZBAUBGZUCFZHZWMWLUD FZCIZDIZWLUEJZKZWPEIZWLUFJZGZWQWTXAGZWRKZUGZEWLLJZMDXFMCXFMWLUAFWKWMUHWNB @@ -472557,7 +472557,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a breq123d corng crg cogrp cv cple cmulr wi wral simpr comnd ringgrp adantl cmnd orngogrp isogrp simprbi ringmnd submomnd syl2an sylanbrc simp-4l wss wn reldmress ovprc2 fveq2d base0 syl6eqr wne cur ringidcl ad2antlr neneqd - ne0d condan ressbas inss2 syl6eqssr ad3antrrr simpllr sseldd simprl csubg + ne0d condan ressbas inss2 eqsstrrdi ad3antrrr simpllr sseldd simprl csubg wb orngring ressinbas oveq2d eqtrd eqeltrrd issubg syl3anbrc subg0 eqtr4d cin ad2antrr ressle eqidd mpbird simplr simprr orngmul syl122anc ressmulr oveqd mpbid ex anasss ralrimivva isorng ) BUAEZBAFGZUBEZHZXLXKUCEZXKIJZCU @@ -475923,7 +475923,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a = ( M |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) ) $= ( vi vj cn wcel cfv co c1 cfz cv cmpo cres wceq adantr wa csubma csn cdif csmat cmin cxp submat1n simpr cuz nnuz eleq2i biimpi eluzfz2 syl submaval - syl3anc fzdif2 difss syl6eqssr resmpo syl2anc matmpo reseq1d adantl eqidd + syl3anc fzdif2 difss eqsstrrdi resmpo syl2anc matmpo reseq1d adantl eqidd eqid wss mpoeq123dv 3eqtr4rd 3eqtrd ) EJKZDBKZUAZEEDUELMEEDNEOMZCUBMZLMZH IVOEUCZUDZVSHPIPDMZQZDNENUFMOMZWBUGZRZABCDEFGUHVNVMEVOKZWEVQWASVLVMUIVLWE VMVLENUJLZKZWEVLWGJWFEUKULUMZNEUNUOTZWIABVPCHIEEDVOFVPVGGUPUQVNHIVOVOVTQZ @@ -476513,7 +476513,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a nn0ltlem1 biimpa eqbrtrd iftrued oveq1d nncnd 1cnd pncand 3eqtrd fvmptd eqtrd idi f1ocnvfv imp fveq2d breq1d breqtrrd ad2antrr ad3antrrr simplr adantlr eqtr2d wn eqbrtrrd ex con3d an32s ifeqda wfun cdm f1ocnv f1ofun - 3syl wss cdif fzdif2 difss syl6eqssr f1odm sseqtrrd sseldd fvco syl2anc + 3syl wss cdif fzdif2 difss eqsstrrdi f1odm sseqtrrd sseldd fvco syl2anc csn eqtr4d ) APUMOUMUNUOZUPUOZUQZURZPKUSUTZPPUMVAUOZVBPGVCZVHZEVHZPEUVD VDVHZUVAUVBPUVCUVFUVAUVBURZUVFUVCEVHZPUVAUVFUVIVEZUVBUVAUVEUVCEUVAUMOUP UOZUVKGVFZUVCUVKUQZUVCGVHPVEZUVEUVCVEZAUVLUUTAGUVKVGVHZVIVHZUQZUVLAOUVK @@ -476559,7 +476559,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a madjusmdetlem3 $p |- ( ph -> ( I ( subMat1 ` U ) J ) = ( N ( subMat1 ` W ) N ) ) $= ( csmat cfv co c1 cmin cfz cxp cres wceq cv wral wcel wa ccnv cvv wss - ccom csn cdif cuz cn nnuz syl6eleq fzdif2 syl syl6eqssr adantr simprl + ccom csn cdif cuz cn nnuz syl6eleq fzdif2 syl eqsstrrdi adantr simprl difss sseldd simprr ovexd ovmpt4g syl3anc ovresd clt wbr cif cbs eqid caddc cmap fz1ssnn sseldi eqidd smatlem madjusmdetlem2 syldan oveq12d matbas2i eqtrd 3eqtr4rd ralrimivva cmat wb smatcl cmpo ccrg fzfid w3a @@ -485658,7 +485658,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry omsmon $p |- ( ph -> ( M ` A ) <_ ( M ` B ) ) $= ( vx vz vy cfv wss wa wcel syl coms cle cuni com cdom wbr cdm cpw cesum cv crab cmpt crn cc0 cpnf cicc co cinf cres wceq wi adantr sstr2 anim1d - clt ss2rabdv resmpt resss syl6eqssr rnss wral wf ad2antrr ssrab2 simplr + clt ss2rabdv resmpt resss eqsstrrdi rnss wral wf ad2antrr ssrab2 simplr sseldi elpwi fdmd sseqtrd sseldd ffvelrnd ralrimiva cvv vex nfcv esumcl simpr rnmptss xrge0infssd sstrd omsfval syl3anc 3brtr4d fveq1i 3brtr4g mpan eqid ) ABEUAPZPZCWRPZBFPCFPUBAMBNUJZUCZQZXAUDUEUFZRZNEUGZUHZUKZMUJ @@ -486565,7 +486565,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry Thierry Arnoux, 19-Jul-2020.) @) caraextros @p |- ( ph -> ( M |` R ) = P ) @= ( vv wa wss wceq wcel vu vz ve cdm cuni cpw wfn cfv wral cres cpnf cicc - cv cc0 co wf coms omsf syl2anc wb feq1 sylibr ffn syl jca fdm syl6eqssr + cv cc0 co wf coms omsf syl2anc wb feq1 sylibr ffn syl jca fdm eqsstrrdi ax-mp pwuni cle wbr com cdom crab cesum cmpt crn clt ccnv fveq1i adantr csup elssuni adantl omsfval syl3anc syl5eq ad2antrr unieq breq1 anbi12d sseq2d elrab simplbi pweqd eleqtrd elpwi sselda ffvelrnd ralrimiva nfcv @@ -492414,7 +492414,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry cv cgsu c1 cmin caddc cneg ctp signswbase signswmnd a1i cn0 cuz cn eldifi cmnd wne lencl syl eldifsn hasheq0 necon3bid biimpar sylbi elnnne0 adantr sylanbrc nnm1nn0 nn0uz syl6eleq cxr cfzo wf ccatws1cl wrdf wceq cz fzoval - nn0zd fzossfz syl6eqssr s1cl ccatlen sylan2 oveq2i syl6eq oveq2d peano2zd + nn0zd fzossfz eqsstrrdi s1cl ccatlen sylan2 oveq2i syl6eq oveq2d peano2zd s1len nn0cnd 1cnd pncand 3eqtrd sseqtrrd sselda sylanl1 rexrd signswplusg ffvelrnd sgncl rexr adantl id npcand sylan9eqr fveq2d ccatws1ls gsumnunsn eqtrd mpteq1d simpll ad2antlr eleq2d ccatval1 syl3anc mpteq2dva oveq1d wo @@ -513867,7 +513867,7 @@ proper pair (of ordinal numbers) as model for a Godel-set of membership ( <. D , H , A >. e. P /\ D C_ ( Z X. Z ) ) ) $= ( cotp wcel wss c1st cfv wceq syl cvv cxp wa mstapst cin cmsr eqid msrval sseli msrid eqtr3d fveq2d inss1 mpstrcl simp1d ssexg simp2d simp3d ot1stg - w3a sylancr syl3anc 3eqtr3d inss2 syl6eqssr jca adantr simpr df-ss oteq1d + w3a sylancr syl3anc 3eqtr3d inss2 eqsstrrdi jca adantr simpr df-ss oteq1d crn sylib eqtrd wfn wf msrf ffn ax-mp fnfvelrn eqeltrrd mstaval syl6eleqr simpl impbii ) BFAMZDNZWDCNZBHHUAZOZUBZWEWFWHDCWDCDEIJUCUHZWEBBWGUDZWGWEW KFAMZPQZPQZWDPQZPQZWKBWEWMWOPWEWLWDPWEWDEUEQZQZWLWDWEWFWRWLRZWJABCWQEFGHK @@ -514508,7 +514508,7 @@ proper pair (of ordinal numbers) as model for a Godel-set of membership cnveqi a1i uneq12d cnvun 3eqtr4g jca simp2d simp3d syl3anbrc cv wrex c1st elmthm simpll adantr cin c2nd csn cima cuni mppspst simprl mpst123 fveq2d syl simprr eqtr3d eqeltrrd msrval 3eqtr3d fvex inex1 sneqd imaeq2d unieqd - otth syl6eqr sqxpeqd ineq2d inss1 syl6eqssr eqidd oteq123d simp1bi ssdifd + otth syl6eqr sqxpeqd ineq2d inss1 eqsstrrdi eqidd oteq123d simp1bi ssdifd eqtrd unss12 syl2anc inundif eqcomi 3sstr4g ss2mcls elmpps simprbi sseldd ssidd rexlimddv sylanbrc ineq1i indir c0 incom disjdif 0ss eqsstri 3eqtri ssequn2 mpbi oteq1d 3eqtr4d ex mthmi impbid1 ) EUBSZBGAUCZFSZIGAUCZHSZUUN @@ -540531,7 +540531,7 @@ coordinates of a barycenter of two points in one dimension (complex dissneqlem $p |- ( ( C C_ B /\ B e. ( TopOn ` A ) ) -> B = ~P A ) $= ( vy vz wss cfv wcel wa adantl cv cuni wceq wex wrex cab crn ctopon cpw cpr topgele simprd velpw w3a csn cvv simp3 cmpt cima cres df-ima resmpt - c0 syl5eq rnmptsn syl6eq imassrn syl6eqssr syl6sseq sneq eqeq2d cbvrexv + c0 syl5eq rnmptsn syl6eq imassrn eqsstrrdi syl6sseq sneq eqeq2d cbvrexv rneqd abbii eqtri sseqtrrdi wi sstr expcom adantr mpd ssexd isset sylib 3adant3 eqid mptsnun unieqd eqtrd sseq1 unieq anbi12d syl5ibrcom eximdv jca syl3an2b 3com23 3expia wb ctg ctop topontop tgtop syl eleq2d bitr3d @@ -541279,7 +541279,7 @@ coordinates of a barycenter of two points in one dimension (complex exrecfnlem $p |- ( ( A e. V /\ A. y B e. W ) -> E. x ( A C_ x /\ A. y e. x B e. x ) ) $= ( vu wcel com cfv wss cv wa wi wceq cvv nfcv crdg wex wal c0 rdg0g peano1 - wral con0 wlim omelon limom rdglimss mpanl12 syl6eqssr wrex ciun rdglim2a + wral con0 wlim omelon limom rdglimss mpanl12 eqsstrrdi wrex ciun rdglim2a ax-mp mp2an eleq2i eliun bitri csuc nnon cmpt crn cun eqid elrnmpt1 elun2 peano2 syl fvex nfmpt1 nfrn nfun nfmpt nfcxfr nfrdg nffv rnex unex rdgeq1 mptexgf id nfeq2 eqidd mpteq12df rneqd uneq12d rdgsucmptf eleq2d rdgellim @@ -642391,7 +642391,7 @@ of ideals (the usual "pure ring theory" definition). (Contributed by simprl breq1d rexrab abbii eqtri syl6eqr adantr sseqtrd simprr fipreima wi ssrab2 sstr2 mpi adantl velpw sylibr adantrr elind cbs syl6ss lidlss ply1ring sstrd rspcl cres df-ima wral rspssid simprbi ad2antrl sylanbrc - ssrab resmptd resmpt eqtr4d syl6eqssr rnss eqsstrid sseqtrrd rspssp jca + ssrab resmptd resmpt eqtr4d eqsstrrdi rnss eqsstrid sseqtrrd rspssp jca resss sseq1d anbi2d syl5ibcom sylan2b expimpd reximdv2 sseq1 syl5ibrcom mpd rexbidv rexlimdva ) AIGDRRZUAUNZCUERZRZUFZUAYOUGUHUIZUJZYOIFUNZHRZD RRZSZFGUGZUHUIZUJZACUKTZYOCULRZTZUUANACUMTZGETZIUOTZUUKAUUIUULNCUPUQZOP @@ -686055,7 +686055,7 @@ distinct definitions for the same symbol (limit of a sequence). dvmulcncf $p |- ( ph -> ( S _D ( F oF x. G ) ) e. ( X -cn-> CC ) ) $= ( cof co cdv cc wcel wf cdm wceq wss cr cmul caddc ccncf cncff fdm dvmulf 3syl wi wa wo ax-resscn sseq1 mpbiri eqimss pm3.2i cpr elpri pm3.44 mpsyl - syl dvbsss syl6eqssr dvcn syl31anc mulcncff addcncff eqeltrd ) ABCDUAKZLM + syl dvbsss eqsstrrdi dvcn syl31anc mulcncff addcncff eqeltrd ) ABCDUAKZLM LBCMLZDVHLZBDMLZCVHLZUBKLENUCLZABCDEFGHAVIVMOENVIPVIQZERZIENVIUDENVIUEUGZ AVKVMOENVKPVKQERZJENVKUDENVKUEUGZUFAVJVLEAVIDEIABNSZENDPEBSZVQDVMOBTRZVSU HZBNRZVSUHZUIAWAWCUJZVSWBWDWAVSTNSUKBTNULUMBNUNUOABTNUPOWEFBTNUQUTVSWAWCU @@ -686106,7 +686106,7 @@ distinct definitions for the same symbol (limit of a sequence). dvdivcncf $p |- ( ph -> ( S _D ( F oF / G ) ) e. ( X -cn-> CC ) ) $= ( cof co cdv cc wcel wf wceq wss cr cc0 vx cdiv cmul cmin ccncf cdm cncff vy fdm dvdivf wi wa wo ax-resscn sseq1 mpbiri eqimss pm3.2i cpr elpri syl - 3syl pm3.44 mpsyl csn cdif difssd fssd dvbsss syl6eqssr syl31anc mulcncff + 3syl pm3.44 mpsyl csn cdif difssd fssd dvbsss eqsstrrdi syl31anc mulcncff dvcn subcncff cvv cv eldifi adantr adantl mulcld eldifsni mulne0d eldifsn wne sylanbrc ssexd inidm off wb cncffvrn syl2anc mpbird divcncff eqeltrd ) ABCDUBKZLMLBCMLZDUCKZLZBDMLZCWQLZUDKLZDDWQLZWOLENUELZABCDEFGHAWPXCOENWP @@ -688726,7 +688726,7 @@ distinct definitions for the same symbol (limit of a sequence). cv cr nffv cbvditg cioo wa wceq wss iccssred adantr ioossicc sseli adantl cc sseldd iftrued a1i ccncf wf syl feq1dd fvmptelrn syldan fvmpt2 syl2anc cncff eqeltrd 3eqtrd ditgeq3d cpnf cmnf mnfxr pnfxr ioomax eqcomi sseqtrd - cxr ax-resscn syl6eqssr cncfss ccnfld ctopn crn crest cuni cres eqid ctop + cxr ax-resscn eqsstrrdi cncfss ccnfld ctopn crn crest cuni cres eqid ctop ctg ccn cnfldtop syl6ss ssid unicntop restid ax-mp cncfcn sylancl restabs cvv syl3anc tgioo2 oveq1d eqtr3d eqtrd eleqtrd icccncfext simpld uniretop reex cnf feq2d mpbid eqeltrrd ctopon resttopon sylancr feqmptd frnd eqtri @@ -742452,7 +742452,7 @@ Ring homomorphisms (extension) subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.) $) lidlssbas $p |- ( U e. L -> ( Base ` I ) C_ ( Base ` R ) ) $= - ( wcel cbs cfv cin eqid ressbas inss2 syl6eqssr ) BDGCHIBAHIZJOBOCDAFOKLB + ( wcel cbs cfv cin eqid ressbas inss2 eqsstrrdi ) BDGCHIBAHIZJOBOCDAFOKLB OMN $. $( A (left) ideal of a ring is the base set of the restriction of the ring