From 4d51170e96e43136c9014aec8da2328bcdc264b4 Mon Sep 17 00:00:00 2001 From: Jim Kingdon Date: Thu, 25 Jan 2024 05:03:57 -0800 Subject: [PATCH] Rename syl6sseqr to sseqtrrdi (#3789) This is in set.mm and iset.mm Co-authored-by: Wolf Lammen <30736367+wlammen@users.noreply.github.com> --- changes-set.txt | 2 +- iset.mm | 46 +++--- set.mm | 422 ++++++++++++++++++++++++------------------------ 3 files changed, 235 insertions(+), 235 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index 08397e4e04..60304da5e6 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -71,7 +71,6 @@ proposed syl6eleq eleqtrdi compare to eleqtri or eleqtrd 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 syl6sseqr sseqtrrdi 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 @@ -80,6 +79,7 @@ make a github issue.) DONE: Date Old New Notes 23-Jan-24 nelb [same] moved from TA's mathbox to main set.mm +22-Jan-24 syl6sseqr sseqtrrdi 20-Jan-24 nfiund nfiundg 20-Jan-24 bnj1441 bnj1441g 20-Jan-24 cbviinv cbviinvg diff --git a/iset.mm b/iset.mm index 7c7b98f28d..4b7c3bdf67 100644 --- a/iset.mm +++ b/iset.mm @@ -27555,11 +27555,11 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use $} ${ - syl6ssr.1 $e |- ( ph -> A C_ B ) $. - syl6ssr.2 $e |- C = B $. + sseqtrrdi.1 $e |- ( ph -> A C_ B ) $. + sseqtrrdi.2 $e |- C = B $. $( A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) $) - syl6sseqr $p |- ( ph -> A C_ C ) $= + sseqtrrdi $p |- ( ph -> A C_ C ) $= ( eqcomi syl6sseq ) ABCDEDCFGH $. $} @@ -38851,7 +38851,7 @@ rather than an implication (but the two are equivalent by ~ bm1.3ii ), (Contributed by NM, 29-Nov-2003.) $) iunpw $p |- ( E. x e. A x = U. A <-> ~P U. A = U_ x e. A ~P x ) $= ( vy cuni wceq wrex cpw ciun wcel sseq2 biimprcd reximdv com12 ssiun elpw - cv wss eliun wa uniiun syl6sseqr impbid1 df-pw abeq2i bitri 3bitr4g eqrdv + cv wss eliun wa uniiun sseqtrrdi impbid1 df-pw abeq2i bitri 3bitr4g eqrdv vex rexbii ssid uniex eleq2 syl5bbr mpbii sylib elssuni elpwi eqss sylibr anim12i ex reximia syl impbii ) AQZBEZFZABGZVGHZABVFHZIZFZVIDVJVLVIDQZVGR ZVNVFRZABGZVNVJJVNVLJZVIVOVQVOVIVQVOVHVPABVHVPVOVFVGVNKLMNVQVNABVFIVGABVF @@ -45515,7 +45515,7 @@ Definite description binder (inverted iota) Salmon, 11-Jul-2011.) $) iotanul $p |- ( -. E! x ph -> ( iota x ph ) = (/) ) $= ( vz weu wn cio c0 wss wceq weq wb wal wex df-eu cab dfiota2 alnex ax-in2 - cuni wi alimi ss2ab sylibr dfnul2 syl6sseqr sylbir uni0 syl6sseq eqsstrid + cuni wi alimi ss2ab sylibr dfnul2 sseqtrrdi sylbir uni0 syl6sseq eqsstrid unissd sylnbi ss0 syl ) ABDZEABFZGHZUOGIUNABCJKBLZCMZUPABCNUREZUOUQCOZSZG ABCPUSVAGSGUSUTGUSUQEZCLZUTGHUQCQVCUTCCJEZCOZGVCUQVDTZCLUTVEHVBVFCUQVDRUA UQVDCUBUCCUDUEUFUJUGUHUIUKUOULUM $. @@ -45539,7 +45539,7 @@ Definite description binder (inverted iota) iotass $p |- ( A. x ( ph -> x C_ A ) -> ( iota x ph ) C_ A ) $= ( vy cv wss wal cio cab csn wceq cuni df-iota cpw unieq vex df-pw sspwuni wi sylib unisn syl6eq sseq2i ss2ab bitri biimpri sseq1 syl2anr ex ss2abdv - biimpa syl6sseqr eqsstrid ) ABECFZSBGZABHABIZDEZJZKZDIZLZCABDMUOUTCNZFVAC + biimpa sseqtrrdi eqsstrid ) ABECFZSBGZABHABIZDEZJZKZDIZLZCABDMUOUTCNZFVAC FUOUTUQCFZDIVBUOUSVCDUOUSVCUSUPLZUQKZVDCFZVCUOUSVDURLUQUPUROUQDPUAUBUOUPV BFZVFVGUOVGUPUNBIZFUOVBVHUPBCQUCAUNBUDUEUFUPCRTVEVFVCVDUQCUGUKUHUIUJDCQUL UTCRTUM $. @@ -57858,7 +57858,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) $= ( vz cdm wcel cv wex cfv cres wceq wa con0 wi syl com3l crecs cop ibi wfn eldm2g wral wrex cab cuni df-recs eleq2i eluniab bitri wss abeq2i elssuni - fnop rspe recsfval syl6sseqr sylbir fveq2 reseq2 fveq2d rspcv fndm eleq2d + fnop rspe recsfval sseqtrrdi sylbir fveq2 reseq2 fveq2d rspcv fndm eleq2d eqeq12d wfun tfrlem7 funssfv mp3an1 adantrl eleq1d onelss imp31 fun2ssres syl6bir w3a sylan2 exbiri exp31 com34 com24 sylbird syld imp4d mpdi exp4d ex com4r pm2.43i imp4a rexlimdv imp exlimiv sylbi ) DFUAZIZJZDHKZUBZWRJZH @@ -58010,7 +58010,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and shortened by Mario Carneiro, 24-May-2019.) $) tfrlemibfn $p |- ( ph -> U. B Fn x ) $= ( wss cvv wcel syl cuni wfun cdm cv wceq wfn crecs tfrlemibacc recsfval - unissd syl6sseqr tfrlem7 funss cxp cpw cfv cop csn cun w3a wex wrex cab + unissd sseqtrrdi tfrlem7 funss cxp cpw cfv cop csn cun w3a wex wrex cab mpisyl wa simpr3 csuc wf wal ad2antrr con0 simplr onelon syl2anc simpr1 simpr2 tfrlemisucfn dffn2 sylib fssxp word eloni ordsucss sylc xpss1 wb sstrd vex tfrlem3-2d simprd opexg sylancr snexg unexg mpbird eqeltrd ex @@ -58039,7 +58039,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and tfrlemiubacc $p |- ( ph -> A. u e. x ( U. B ` u ) = ( F ` ( U. B |` u ) ) ) $= ( cfv wceq wcel cv cuni cres wral crecs cdm wfn tfrlemibfn fndm syl wss - tfrlemibacc unissd recsfval syl6sseqr dmss eqsstrrd sselda tfrlem9 wfun + tfrlemibacc unissd recsfval sseqtrrdi dmss eqsstrrd sselda tfrlem9 wfun wa tfrlem7 a1i adantr eleq2d biimpar funssfv syl3anc word eloni ordelss sylan sseqtrrd fun2ssres fveq2d 3eqtr3d ralrimiva fveq2 eqeq12d cbvralv con0 reseq2 sylibr ) AEUAZHUBZRZWEWDUCZLRZSZEBUAZUDFUAZWERZWEWKUCZLRZSZ @@ -58107,7 +58107,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and cun wal simprl fneq2 raleq anbi12d rspcev adantll tfrlem3a tfrlemisucaccv vex sylibr tfrlem3-2d simprd opexg sylancr snidg 3syl wi opeldmg mpd dmeq elun2 eleq2d syl2anc exlimddv eliun ssrdv cuni recsfval dmeqi dmuni eqtri - ex syl6sseqr eqssd ) AFUAZNZOWPUBWPOUFABCDEFGUCWPUGUDAOIDIPZNZUEZWPAJOWSA + ex sseqtrrdi eqssd ) AFUAZNZOWPUBWPOUFABCDEFGUCWPUGUDAOIDIPZNZUEZWPAJOWSA JPZOQZWTWSQZAXARZWTWRQZIDUHZXBXCKPZWTUIZLPZXFSXFXHUJFSUKZLWTULZRZXEKABCLD WTEKFGHUMXCXKRZXFWTXFFSZUNZUOZUSZDQWTXPNZQZXEXLBCJDEKFGAFUPZBPFSTQRBUTXAX KHUQAXAXKURXCXGXJVAXLXFMPZUIZXILXTULZRZMOUHZXFDQXAXKYDAYCXKMWTOXTWTUKYAXG @@ -58229,7 +58229,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and a subset of ` recs ` . (Contributed by Jim Kingdon, 15-Mar-2022.) $) tfr1onlemssrecs $p |- ( ph -> U. A C_ recs ( G ) ) $= ( cuni cv wfn cfv cres wceq wral wa con0 wrex cab word wss ordsson ssrexv - crecs wi 3syl ss2abdv eqsstrid unissd df-recs syl6sseqr ) ADJEKZBKZLCKZUM + crecs wi 3syl ss2abdv eqsstrid unissd df-recs sseqtrrdi ) ADJEKZBKZLCKZUM MUMUONFMOCUNPQZBRSZETZJFUEADURADUPBGSZETURHAUSUQEAGUAGRUBUSUQUFIGUCUPBGRU DUGUHUIUJBCEFUKUL $. $} @@ -58531,7 +58531,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and csuc wi wal 3expia alrimiv fneq1 fveq2 eleq1d imbi12d spv syl rspcdva ralrimiva imp opexg sylancr snidg elun2 3syl opeldmg mpd dmeq syl2anc eleq2d exlimddv eliun ssrdv dmuni wss tfr1onlemssrecs eqsstrrid sstrd - ex dmss dmeqi syl6sseqr ) AIGUEZUFZFUFAIUADUARZUFZUGZYBAUBIYEAUBRZISZ + ex dmss dmeqi sseqtrrdi ) AIGUEZUFZFUFAIUADUARZUFZUGZYBAUBIYEAUBRZISZ YFYESZAYGUHZYFYDSZUADUIZYHYIQRZYFUJZUCRZYLUKYLYNULGUKUMZUCYFUNZUHZYKQ AYGYFHSZYQQUOYIHUPZYGIHSZUHYRAYSYGLUQYIYGYTAYGURZAYTYGPUQUSYFIHUTVAZA BCUCDYFEQFGHJKLMNOVBVFYIYQUHZYLYFYLGUKZVCZVDZVEZDSYFUUGUFZSZYKUUCBCUB @@ -58926,7 +58926,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and vex fveq1 ralbidv rexbidv elab2 sylibr tfrcllemsucaccv cvv imbi1d wal 3expia alrimiv eleq1d imbi12d spv syl ralrimiva rspcdva opexg sylancr wi imp snidg elun2 3syl opeldmg dmeq eleq2d syl2anc exlimddv eliun ex - mpd ssrdv dmuni tfrcllemssrecs dmss eqsstrrid sstrd dmeqi syl6sseqr + mpd ssrdv dmuni tfrcllemssrecs dmss eqsstrrid sstrd dmeqi sseqtrrdi wss ) AJHUEZUFZGUFAJUADUAUNZUFZUGZYJAUBJYMAUBUNZJRZYNYMRZAYOSZYNYLRZU ADUHZYPYQYNEUCUNZVFZUDUNZYTTZYTUUBUIZHTZUJZUDYNUKZSZYSUCAYOYNIRZUUHUC ULYQIUMZYOJIRZSUUIAUUJYOMUOYQYOUUKAYOUPZAUUKYOQUOUQYNJIURUSZABCUDDYNE @@ -69664,7 +69664,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element. cinl csuc elelsuc df-2o eleqtrri a1i ffvelrnd adantr eqeltrrd 0ex djulclb wf wb orcd df-dc cpr 1oex prid2 df2o3 wrex simp-4r djulcl syl2anc simplrr foelrn fveq2d simp-5r 3eqtrd elpri eleq2s ad2antrl mpjaodan rexlimddv wne - djune neii pm2.65da olcd syl6sseqr exmidfodomrlemeldju exlimdd ex alrimiv + djune neii pm2.65da olcd sseqtrrdi exmidfodomrlemeldju exlimdd ex alrimiv simplr df-exmid ) CFZBFZGZCHZYTAFZIJZKZUUCYTDFZUCZDHZLZBUDZAUDZEFZMUEZUFZ MUULGZUGZLZEUDUHUUKUUQEUUKUUNUUPUUKUUNKZNUULOUAZUUFUCZUUPDUUKUUNDUUJDAUUI DBUUEUUHDUUEDUIUUGDUJUKULULUUNDUIUMUUPDUIUURUUKYSUUSGZCHZUUSNIJZKZUUTDHZU @@ -69708,7 +69708,7 @@ elements or fails to hold (is equal to ` (/) ` ) for some element. orcd df-dc sylibr simp-4r djulcl foelrn syl2anc simprr wb eqeq1d ad2antlr wrex fvres mpbird adantr simpr fveq2d simp-5r 3eqtrd elpri df2o3 ad2antrl cpr eleq2s mpjaodan rexlimddv wne 0ex djune neii a1i mtbiri pm2.65da olcd - eqeq12d simplr syl6sseqr wf 1oex eleqtrri ffvelrnd exmidfodomrlemreseldju + eqeq12d simplr sseqtrrdi wf 1oex eleqtrri ffvelrnd exmidfodomrlemreseldju fof prid2 csuc elelsuc df-2o exlimdd ex alrimiv df-exmid ) CFZBFZGZCHZUUF AFZIJZKZUUIUUFDFZUAZDHZLZBUBZAUBZEFZMUDZUEZMUURGZUFZLZEUBUGUUQUVCEUUQUUTU VBUUQUUTKZNUUROUHZUULUAZUVBDUUQUUTDUUPDAUUODBUUKUUNDUUKDUIUUMDUJUKULULUUT @@ -94736,7 +94736,7 @@ nonnegative integers (cont.)". $) $( The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.) $) uznnssnn $p |- ( N e. NN -> ( ZZ>= ` N ) C_ NN ) $= - ( cn wcel cuz cfv c1 wss elnnuz uzss sylbi nnuz syl6sseqr ) ABCZADEZFDEZBMA + ( cn wcel cuz cfv c1 wss elnnuz uzss sylbi nnuz sseqtrrdi ) ABCZADEZFDEZBMA OCNOGAHFAIJKL $. ${ @@ -109818,7 +109818,7 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new ( vz vw cc wcel wa cv cmin co wbr copab cvv cshi wceq caddc wrex sylancom simpr simpl cdm cab crn cxp wss simplr simpll subcld breldmg mp3an2 npcan vex eqcomd ancoms adantr oveq1 eqeq2d rspcev syl2anc eqeq1 rexbidv sylibr - elab brelrng jca ssopab2dv df-xp syl6sseqr dmexg abrexexg syl rnexg xpexg + elab brelrng jca ssopab2dv df-xp sseqtrrdi dmexg abrexexg syl rnexg xpexg expl ssexg syl2an elex breq anbi2d opabbidv breq1d df-shft ovmpog syl3an1 oveq2 syl3anc ) CHIZDEIZJWKWJAKZHIZWLCLMZBKZDNZJZABOZPIZDCQMWRRZWJWKUBWJW KUCWJWRFKZGKZCSMZRZGDUDZTZFUEZDUFZUGZUHXIPIZWSWKWJWRWLXGIZWOXHIZJZABOXIWJ @@ -109872,7 +109872,7 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new ( vz vw cc wcel cv cmin co wbr wa copab cvv cshi wceq caddc wrex sylancom cdm cab crn cxp wss simplr simpll subcld vex breldmg mp3an2 eqcomd ancoms npcan adantr oveq1 eqeq2d rspcev syl2anc eqeq1 rexbidv sylibr brelrng jca - elab expl ssopab2dv df-xp syl6sseqr dmex abrexex rnex xpex sylancl anbi2d + elab expl ssopab2dv df-xp sseqtrrdi dmex abrexex rnex xpex sylancl anbi2d ssexg breq opabbidv oveq2 breq1d df-shft ovmpog mp3an1 mpdan ) CHIZAJZHIZ WGCKLZBJZDMZNZABOZPIZDCQLWMRZWFWMFJZGJZCSLZRZGDUBZTZFUCZDUDZUEZUFXDPIWNWF WMWGXBIZWJXCIZNZABOXDWFWLXGABWFWHWKXGWFWHNZWKNZXEXFXIWGWRRZGWTTZXEXIWIWTI @@ -133351,7 +133351,7 @@ _Introduction to General Topology_ (1983), p. 114) and it is convenient $( A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) $) eltopss $p |- ( ( J e. Top /\ A e. J ) -> A C_ X ) $= - ( wcel wss ctop cuni elssuni syl6sseqr adantl ) ABEZACFBGELABHCABIDJK $. + ( wcel wss ctop cuni elssuni sseqtrrdi adantl ) ABEZACFBGELABHCABIDJK $. $} @@ -134325,7 +134325,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on $( The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) $) difopn $p |- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A \ B ) e. J ) $= - ( wcel ccld cfv wa cin cdif wss wceq elssuni syl6sseqr adantr df-ss sylib + ( wcel ccld cfv wa cin cdif wss wceq elssuni sseqtrrdi adantr df-ss sylib cuni adantl difeq1d indif2 cldrcl simpl cldopn syl3anc eqeltrrid eqeltrrd ctop inopn ) ACFZBCGHFZIZADJZBKZABKCUMUNABUMADLZUNAMUKUPULUKACSDACNEOPADQ RUAUMUOADBKZJZCADBUBUMCUIFZUKUQCFZURCFULUSUKBCUCTUKULUDULUTUKBCDEUETAUQCU @@ -134948,7 +134948,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on ( topGen ` ( B |`t A ) ) = ( ( topGen ` B ) |`t A ) ) $= ( vx vy vz vw wcel wa crest cv wss cuni wceq wex cvv cin cmpt crn ctg cfv co wb cxp wfn restfn elex fnovex mp3an3an syl cima wfun simpll funmpt a1i - eltg3 restval sseq2d wral vex inex1 rgenw eqid fnmpt fnima mp2b syl6sseqr + eltg3 restval sseq2d wral vex inex1 rgenw eqid fnmpt fnima mp2b sseqtrrdi biimpa ssimaexg syl3anc wi ciun df-ima resmpt adantl syl5eq unieqd dfiun3 cres rneqd syl6eqr iunin1 syl6eq tgvalex ad2antrr adantr uniiun eqeltrrid simpr eltg3i adantlr elrestr eqeltrd unieq syl5ibrcom expimpd exlimdv mpd @@ -136388,7 +136388,7 @@ F C_ ( CC X. X ) ) $= ( vz vr vs cxp cv wcel wa wrex wss wceq vw cuni relxp cop eleq2i eluni2 bitri anbi12i opelxp reeanv 3bitr4i eqid xpeq1 eqeq2d xpeq2 rspc2ev vex mp3an3 xpex eqeq1 2rexbidv crn cab rnmpo eqtri elab2 sylibr elssuni syl - cmpo sseld syl5bir rexlimivv relssi cpw wf wral syl6sseqr xpss12 syl2an + cmpo sseld syl5bir rexlimivv relssi cpw wf wral sseqtrrdi xpss12 syl2an sylbi elpw rgen2 fmpo mpbi frn ax-mp eqsstri sspwuni eqssi ) FGNZCUBZKU AWKWLFGUCKOZUAOZUDZWKPZWMLOZPZWNMOZPZQZMERLDRZWOWLPZWMFPZWNGPZQWRLDRZWT MERZQWPXBXDXFXEXGXDWMDUBZPXFFXHWMIUELWMDUFUGXEWNEUBZPXGGXIWNJUEMWNEUFUG @@ -140719,7 +140719,7 @@ S C_ ( P ( ball ` D ) T ) ) $= tgioo $p |- ( topGen ` ran (,) ) = J $= ( vz cioo cr wcel wceq wss cv co wa c1 cxr syl2anc syl clt cmnf wbr cbl vv vx vy va vb cfv crn ctg cxmet rexmet mopnval ax-mp blex rnex blssioo - vw cvv crp wrex wral cuni elssuni unirnioo syl6sseqr cin retopbas simpl + vw cvv crp wrex wral cuni elssuni unirnioo sseqtrrdi cin retopbas simpl ctb a1i sselda cmin caddc 1re bl2ioo mpan2 peano2rem peano2re ioorebasg rexrd eqeltrd simpr 1rp blcntr mp3an13 elind basis2 syl22anc cxp cpw wf wfn wb ioof ffn ovelrn mp2b wi eleq2 sseq1 anbi12d csup cinf inss2 sstr diff --git a/set.mm b/set.mm index f81f45d7b7..6a8e670435 100644 --- a/set.mm +++ b/set.mm @@ -36938,11 +36938,11 @@ technically classes despite morally (and provably) being sets, like ` 1 ` $} ${ - syl6ssr.1 $e |- ( ph -> A C_ B ) $. - syl6ssr.2 $e |- C = B $. + sseqtrrdi.1 $e |- ( ph -> A C_ B ) $. + sseqtrrdi.2 $e |- C = B $. $( A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) $) - syl6sseqr $p |- ( ph -> A C_ C ) $= + sseqtrrdi $p |- ( ph -> A C_ C ) $= ( eqcomi syl6sseq ) ABCDEDCFGH $. $} @@ -45969,7 +45969,7 @@ same distinct variable group (meaning ` A ` cannot depend on ` x ` ) and ( A. y e. A Disj_ x e. B C /\ Disj_ y e. A U_ x e. B C ) ) ) $= ( vu vv vr vs vz wdisj ciun wral wa nfcv wss cv wcel csb weq nfiu1 nfdisj wi disjss1 ssiun2 syl11 ralrimi a1i cin c0 wceq wo simplr nfcsb1v csbeq1a - cbviun syl6sseqr adantr csbeq1 sseq1d vtoclga adantl cbvdisj disjor sylbb + cbviun sseqtrrdi adantr csbeq1 sseq1d vtoclga adantl cbvdisj disjor sylbb ad2antrl rsp2 syl imp ord impr adantlr disjiun syl13anc expr orrd iuneq1d wn ralrimivva sylibr nfiun ex jcad wrex eleq2i eliun bitri anbi12i reeanv bitr4i simplrr disjeq1d rspc impcom disjors ad2ant2r simplrl eleqtrrd jca @@ -66378,7 +66378,7 @@ complete lattice has a (least) fixpoint. Here we specialize this ( vw wcel cfv wss cv cpw wral wceq fveq2 id rspcdva sylibr w3a crab pwidg cint 3ad2ant1 simp2 sseq12d intminss syl2anc eqsstrid wi wa sseq1d sseq2d pweq raleqbidv simpl3 simprl adantl vex elpw2 simprr sstrd expr ralrimiva - ssintrab cbvrabv inteqi eqtri syl6sseqr simp3 sselpwd fvex elpw eqssd jca + ssintrab cbvrabv inteqi eqtri sseqtrrdi simp3 sselpwd fvex elpw eqssd jca ) DFJZDEKZDLZBMZEKZAMZEKZLZBWBNZOZADNZOZUAZGDLGEKZGPWIGCMZEKZWKLZCWGUBZUD ZDHWIDWGJZVSWODLVQVSWPWHDFUCUEZVQVSWHUFZWMVSCDWGWKDPZWLVRWKDWKDEQWSRUGUHU IUJZWIWJGWIWJIMZEKZXALZIWGUBZUDZGWIXCWJXALZUKZIWGOWJXELWIXGIWGWIXAWGJZXCX @@ -70754,7 +70754,7 @@ result of an operator (deduction version). (Contributed by Paul (Contributed by NM, 29-Nov-2003.) $) iunpw $p |- ( E. x e. A x = U. A <-> ~P U. A = U_ x e. A ~P x ) $= ( vy cv cuni wceq wrex cpw ciun wss wcel sseq2 biimprcd com12 ssiun velpw - reximdv eliun wa uniiun syl6sseqr impbid1 rexbii bitri 3bitr4g eqrdv ssid + reximdv eliun wa uniiun sseqtrrdi impbid1 rexbii bitri 3bitr4g eqrdv ssid uniex elpw eleq2 syl5bbr mpbii sylib elssuni elpwi anim12i eqss sylibr ex reximia syl impbii ) AEZBFZGZABHZVEIZABVDIZJZGZVGDVHVJVGDEZVEKZVLVDKZABHZ VLVHLVLVJLZVGVMVOVMVGVOVMVFVNABVFVNVMVDVEVLMNROVOVLABVDJVEABVDVLPABUAUBUC @@ -72576,7 +72576,7 @@ Axiom of Replacement (unlike ~ resfunexg ). (Contributed by NM, indexed functions. (Contributed by AV, 4-Nov-2023.) $) fviunfun $p |- ( ( Fun U /\ J e. I /\ X e. dom ( F ` J ) ) -> ( U ` X ) = ( ( F ` J ) ` X ) ) $= - ( wcel wfun cfv wss cdm wceq ciun fveq2 ssiun2s syl6sseqr funssfv syl3an2 + ( wcel wfun cfv wss cdm wceq ciun fveq2 ssiun2s sseqtrrdi funssfv syl3an2 cv ) EDHZAIECJZAKFUBLHFAJFUBJMUAUBBDBTZCJZNABDUDEUBUCECOPGQFAUBRS $. $} @@ -77016,7 +77016,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and ( vg vf vx vy vz vw cdm wcel cpred cv wss wral wa cfv cres wceq ciun wrex wfn w3a wex cab cuni cwrecs df-wrecs eqtri dmeqi dmuni eleq2i eliun bitri wi eqid wfrlem1 abeq2i predeq3 sseq1d rspccv adantl wb fndm eleq2d sseq2d - imbi12d adantr mpbird adantrl 3adant3 exlimiv sylbi reximia syl syl6sseqr + imbi12d adantr mpbird adantrl 3adant3 exlimiv sylbi reximia syl sseqtrrdi ssiun ) ECMZNZABEOZGHPZIPZUEWEAQABJPZOZWEQJWERSWFWDTWDWGUADTUBJWERUFIUGHU HZGPZMZUCZWAWBEWJNZGWHUDZWCWKQZWBEWKNWMWAWKEWAWHUIZMWKCWOCABDUJWOFIJABHDU KULUMGWHUNULZUOGEWHWJUPUQWMWCWJQZGWHUDWNWLWQGWHWIWHNWIKPZUEZWRAQZABLPZOZW @@ -77079,7 +77079,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) ) $= ( vz vf vx cv cdm wcel wex cfv wceq wss wa wi cop cpred cres eldm2 wral vex wfn w3a cab cuni cwrecs df-wrecs eqtri eleq2i eluniab bitri elssuni - abid syl6sseqr sylbir wel fnop ex rsp impcom fndm sseq2d eleq2d anbi12d + abid sseqtrrdi sylbir wel fnop ex rsp impcom fndm sseq2d eleq2d anbi12d biimprd expd wfun wfrfun funssfv 3adant3l 3adant3r fveq2d mp3an1 expcom fun2ssres eqeq12d com23 syl6com com34 sylcom adantl com14 exp4a pm2.43d syl7 syldc 3impd exlimdv mpdi imp exlimiv sylbi ) ALZDMNWRILZUAZDNZIOWR @@ -77179,7 +77179,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and wfrlem16 $p |- dom F = A $= ( vf vx vy cdm wss c0 wceq cv cpred wcel wfrdmss cdif wrex eldifn csn cun wa ssun2 vsnid sselii cres cfv cop dmeqi dmun fvex dmsnop uneq2i eleqtrri - 3eqtri wfn wral w3a wex cab wfrlem15 elssuni syl df-wrecs eqtri syl6sseqr + 3eqtri wfn wral w3a wex cab wfrlem15 elssuni syl df-wrecs eqtri sseqtrrdi cuni cwrecs dmss sseld mpi mtand nrex wne df-ne difss tz6.26i mpan sylbir wn mt3 ssdif0 mpbir eqssi ) ENZBBDEFIUABWJOBWJUBZPQZWLWKDARZSPQZAWKUCZWNA WKWMWKTZWNWMWJTZWMBWJUDWPWNUGZWMCNZTWQWMWJWMUEZUFZWSWTXAWMWTWJUHAUIUJWSEW @@ -77200,7 +77200,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and wfrlem17 $p |- ( X e. dom F -> ( F |` Pred ( R , A , X ) ) e. _V ) $= ( vg vf vx vy vz vw wcel cfv cv wss wa wceq cdm cop wfn wral cres w3a wex cpred cab cvv wfun wfrfun funfvop mpan cwrecs df-wrecs eqtri eleq2i eluni - cuni bitri sylib simprr vex wfrlem3a 3simpa simprlr elssuni syl6sseqr syl + cuni bitri sylib simprr vex wfrlem3a 3simpa simprlr elssuni sseqtrrdi syl eqid predeq3 sseq1d simprrr adantl wbr simprll sylibr fvex breldmg mp3an2 df-br syldan simprrl fndm eleqtrd rspcdva sseqtrrd mp3an2i resex syl6eqel fun2ssres expr syl5 exlimdv mpd exlimddv ) ECUAZOZEECPZUBZIQZOZXBJQZKQZUC @@ -77939,7 +77939,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and ( recs ( F ) ` B ) = ( F ` ( recs ( F ) |` B ) ) ) $= ( vz cdm wcel cv wex cfv cres wceq wa con0 wi syl com3l crecs cop ibi wfn eldm2g wral wrex cab cuni dfrecs3 eleq2i eluniab bitri wss abeq2i elssuni - fnop rspe recsfval syl6sseqr sylbir fveq2 reseq2 fveq2d rspcv fndm eleq2d + fnop rspe recsfval sseqtrrdi sylbir fveq2 reseq2 fveq2d rspcv fndm eleq2d eqeq12d wfun tfrlem7 funssfv mp3an1 adantrl eleq1d onelss imp31 fun2ssres syl6bir w3a sylan2 exbiri exp31 com34 com24 sylbird syld imp4d mpdi exp4d ex com4r pm2.43i imp4a rexlimdv imp exlimiv sylbi ) DFUAZIZJZDHKZUBZWRJZH @@ -77960,7 +77960,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and tfrlem9a $p |- ( B e. dom recs ( F ) -> ( recs ( F ) |` B ) e. _V ) $= ( vg vz va cdm wcel cfv cv wa cres cvv wceq con0 wss cop wex wfun tfrlem7 crecs funfvop mpan cuni recsfval eleq2i eluni bitri sylib wfn wral simprr - wrex vex tfrlem3a a1i simplrr elssuni syl6sseqr word fndm ad2antll simprl + wrex vex tfrlem3a a1i simplrr elssuni sseqtrrdi word fndm ad2antll simprl syl eqeltrd eloni wbr simpll fvexd simplrl sylibr breldmg syl3anc ordelss df-br syl2anc fun2ssres resex expr adantrd rexlimdva mpd exlimddv ) DFUEZ KZLZDDWHMZUAZHNZLZWMCLZOZWHDPZQLZHWJWLWHLZWPHUBZWHUCZWJWSABCEFGUDZDWHUFUG @@ -78037,7 +78037,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and Mario Carneiro, 14-Nov-2014.) $) tfrlem13 $p |- -. recs ( F ) e. _V $= ( crecs cvv wcel cdm word wn tfrlem8 ordirr ax-mp cfv cop wss 3syl con0 - csn cun eqid tfrlem12 cuni elssuni recsfval syl6sseqr dmss csuc a1i dmexg + csn cun eqid tfrlem12 cuni elssuni recsfval sseqtrrdi dmss csuc a1i dmexg elon2 sylanbrc sucidg syl wfn wceq tfrlem10 fndm eleqtrrd sseldd mto ) EG ZHIZVDJZVFIZVFKZVGLABCDEFMZVFNOVEVDVFVDEPQUAUBZJZVFVFVEVJCIZVJVDRVKVFRABC VJDEFVJUCZUDVLVJCUEVDVJCUFABCDEFUGUHVJVDUISVEVFVFUJZVKVEVFTIZVFVNIVEVHVFH @@ -78246,7 +78246,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and tz7.44-2 $p |- ( suc B e. X -> ( F ` suc B ) = ( H ` ( F ` B ) ) ) $= ( wcel cfv c0 wceq cuni fveq2d cvv csuc cres cdm wlim crn cv fveq2 reseq2 cif eqeq12d vtoclga eleq1d noel dmeq dm0 syl6eq con0 word wss ordsson wtr - ax-mp ordtr trsuc mpan sseldi sucidg syl cin dmres ordelss fndm syl6sseqr + ax-mp ordtr trsuc mpan sseldi sucidg syl cin dmres ordelss fndm sseqtrrdi wfn df-ss sylib syl5eq eleqtrrd eleq2 syl5ibcom syl5 iffalsed wn nlimsucg mtoi wb limeq mtbird unieqd eloni ordunisuc 3syl eqtrd fvresd 3eqtrd fvex syl6eqel eqeq1 rneq fveq1 ifbieq12d ifbieq2d fvmptg syl2anc ) DUAZHNZXEEO @@ -78268,7 +78268,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and tz7.44-3 $p |- ( ( B e. X /\ Lim B ) -> ( F ` B ) = U. ( F " B ) ) $= ( wcel wlim cfv cuni wceq c0 cvv wa cres crn cima cv fveq2 reseq2 eqeq12d fveq2d vtoclga adantr cdm cif eleq1d simpr wn nlim0 wb cin dmres wss word - ordelss mpan wfn fndm ax-mp syl6sseqr df-ss sylib syl5eq syl6eq sylan9req + ordelss mpan wfn fndm ax-mp sseqtrrdi df-ss sylib syl5eq syl6eq sylan9req dmeq dm0 limeq syl mtbiri mt2d iffalsed mpbird iftrued eqtrd rnexg uniexg ex 3syl eqeltrd eqeq1 rneq unieqd fveq1 ifbieq12d ifbieq2d fvmptg syl2anc df-ima unieqi syl6eqr ) DHNZDOZUAZDEPZEDUBZUCZQZEDUDZQXBXCXDFPZXFWTXCXHRZ @@ -78754,7 +78754,7 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and rexbii simpllr wfn fnfun ax-mp fvelima mpan nfan rsp adantld onelon fveq2 neeq1d eleq12d imbi12d rspcv syl5bi com23 syl sylcom com3r expcomd eldifi eleq1 syl5ibcom syl8 com34 rexlimd syl5 ssrdv ssdif0 biimpri anim12i eqss - imp sylibr onss ssel cdm fndm syl6sseqr funfvima2 sylancr com12 a1i syl10 + imp sylibr onss ssel cdm fndm sseqtrrdi funfvima2 sylancr com12 a1i syl10 imp4a eldifn eleq1a con3d syl5com syldd com4r imp31 ancld tz7.48lem syl56 ralrimi ex ancoms adantr 3jca exp41 reximdai syld impcom ) ADEJZDFCUFZUAZ UBZKUCZCBUFZLZFUUAUAZDMZFUUAUDUEUGZUHZBNOZAYPDUUCUBZKMZUUBPZBNOZUUGAYPUUI @@ -89435,7 +89435,7 @@ intersections of elements of the argument (see ~ elfi2 ). (Contributed cres simprll pssss sspwb simplrr ssralv resima2 eqcomd ralbiia ssres inxp simplrl df-res xpss12 eqsstri resex imaundi undif2 breqtrdi simp-4l ssfid eqtr4i cen bren2 sylanbrc ensymd ssdifin0 domunfican syl6eq biimpar disj4 - neeq1d bicomi necon1abii resss syl6sseqr mp2d sylan2br pm2.61dan ralrimiv + neeq1d bicomi necon1abii resss sseqtrrdi mp2d sylan2br pm2.61dan ralrimiv df-ima imp exp32 exp31 a2d findcard3 ) CUIZUJFZEUIZDUIZVUCUBZGHZEUAUIZIZJ ZVUGKBUIZLZBVUDIZMZNZDVUGVUAUKZIZJZNZVUBVUFEUCUIZIZJZVUSKVUJLZBVULMZNZDVU SVUAUKZIZJZNZVUBVUFEAIZJZAKVUJLZBVULMZNZDAVUAUKZIZJZNUAUCAUAUCULZVUQVVGVU @@ -90653,7 +90653,7 @@ all reals (greatest real number) for which all positive reals are greater. ordtypelem2 $p |- ( ph -> Ord T ) $= ( va wtr word cv wss wral wcel wa wbr cima wrex con0 crab ssrab3 a1i onss sselda syl eloni weq imaeq2 raleqdv rexbidv elrab2 simprbi adantl ordelss - wi imass2 ssralv reximdv 3syl ralrimdva sylc sylanbrc syl6sseqr ralrimiva + wi imass2 ssralv reximdv 3syl ralrimdva sylc sylanbrc sseqtrrdi ralrimiva ssrab dftr3 sylibr ordon trssord mp3an23 ) AKUEZKUFZAUDUGZKUHZUDKUIWGAWJU DKAWIKUJZUKZWICUGGUGJULZCNBUGZUMZUIZGHUNZBUOUPZKWLWIUOUHZWQBWIUIZWIWRUHWL WIUOUJZWSAKUOWIKUOUHZAWQBUOKTUQZURUTZWIUSVAWLWIUFZWMCNWIUMZUIZGHUNZWTWLXA @@ -91808,7 +91808,7 @@ all reals (greatest real number) for which all positive reals are greater. csb csbeq1a equcoms eqcomd eleq12d syl5ibrcom wn nfcsb1v r19.21bi iffalse adantr pm2.61d cdm ixpfn fndm dmex syl6eqelr mptelixpg mpbird nfcv cbvixp syl6eleqr simprl fvmpt ad2antrl fveq1 eqeq2d rspc2ev exp32 rexlimd syl5bi - exlimiv sylbi alrimiv ssab sylibr rnmpo syl6sseqr frnd eqssd foeq3 fowdom + exlimiv sylbi alrimiv ssab sylibr rnmpo sseqtrrdi frnd eqssd foeq3 fowdom 3ad2ant3 syl2anc ) BDKZABCUAZEKZABCUBZUCUDZUEZFGUUEBGLZFLZMZUFZNKZUUEBUGZ UUCUUKUHZUUCUUMUIUJUUGUUMUUCUUKURZUUMNKUUDUULUUGUUJUUCKZGBOZFUUEOUUOUUGUU QFUUEUUIUUEKZUUQUUGUURALZUUIMZUUCKZABOZUUQUURUUTCKZABOZUVBUURUUIBPUVDABCU @@ -93382,7 +93382,7 @@ of all inductive sets (which is the smallest inductive set, since fveq2 elrabd ne0d ordunifi syl3anc eqeltrid sseldi cbvrabv elrab2 sylib simprrr wb word ffvelrnd onelon syl2anc eloni ordirr 3syl eleq2 eqeq12d wn nelneq imbi12d rspcdva mtod cvv ssexg sylancr ssonuni ontri1 elssuni - mpbird syl6sseqr eqssd eleq1 imbi1d ralbidv 3jca rexlimddv ) ADUBZJUCZY + mpbird sseqtrrdi eqssd eleq1 imbi1d ralbidv 3jca rexlimddv ) ADUBZJUCZY LKUCZUDZYLEUBZUDZYPJUCZYPKUCZUEZUFZEGUGZUPZLGUDZLJUCZLKUCZUDZLYPUDZYTUF ZEGUGZUHDGAJKIUIUUCDGUJTABCDEFGHIJKNOPQRSUKULAYLGUDZUUCUPZUPZUUDUUGUUJU UMMUBZJUCZUUNKUCZUDZMGUMZGLUUQMGUNZUUMLUURUOZUURUAUUMUURUQURZUURUSUDZUU @@ -94514,7 +94514,7 @@ a Cantor normal form (and injectivity, together with coherence (Contributed by Mario Carneiro, 23-Jun-2013.) $) tcss $p |- ( B C_ A -> ( TC ` B ) C_ ( TC ` A ) ) $= ( vx wss ctc cfv cv wtr wa cab cint cvv wcel wceq tcvalg syl sstr2 anim1d - ssex ss2abdv intss ax-mp syl6sseqr eqsstrd ) BAEZBFGZBDHZEZUHIZJZDKZLZAFG + ssex ss2abdv intss ax-mp sseqtrrdi eqsstrd ) BAEZBFGZBDHZEZUHIZJZDKZLZAFG ZUFBMNUGUMOBACTDBMPQUFUMAUHEZUJJZDKZLZUNUFUQULEUMUREUFUPUKDUFUOUIUJBAUHRS UAUQULUBQAMNUNUROCDAMPUCUDUE $. @@ -94522,7 +94522,7 @@ a Cantor normal form (and injectivity, together with coherence subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.) $) tcel $p |- ( B e. A -> ( TC ` B ) C_ ( TC ` A ) ) $= ( vx wcel ctc cfv cv wss wtr wa cab cint tcvalg wi ssel com12 syl6com cvv - trss impd simpr jca2 ss2abdv intss syl wceq ax-mp syl6sseqr eqsstrd ) BAE + trss impd simpr jca2 ss2abdv intss syl wceq ax-mp sseqtrrdi eqsstrd ) BAE ZBFGBDHZIZULJZKZDLZMZAFGZDBANUKUQAULIZUNKZDLZMZURUKVAUPIUQVBIUKUTUODUKUTU MUNUKUSUNUMUSUKBULEZUNUMOAULBPUNVCUMULBTQRUAUSUNUBUCUDVAUPUEUFASEURVBUGCD ASNUHUIUJ $. @@ -95114,7 +95114,7 @@ of the previous layer (and the union of previous layers when the Carneiro, 8-Jun-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) $) pwwf $p |- ( A e. U. ( R1 " On ) <-> ~P A e. U. ( R1 " On ) ) $= ( cr1 con0 cima cuni wcel cpw crnk cfv wss r1rankidb sspwb sylib cdm r1sucg - csuc wceq ax-mp syl cvv rankdmr1 syl6sseqr fvex elpw2 wlim wb wfun r1funlim + csuc wceq ax-mp syl cvv rankdmr1 sseqtrrdi fvex elpw2 wlim wb wfun r1funlim sylibr simpri limsuc syl6eleqr r1elwf r1elssi pwexr pwidg sseldd impbii mpbi ) ABCDEZFZAGZUTFZVAVBAHIZPZPZBIZFVCVAVBVEBIZGZVGVAVBVHJVBVIFVAVBVDBIZG ZVHVAAVJJVBVKJAKAVJLMVDBNZFZVHVKQAUAZVDORUBVBVHVEBUCUDUIVEVLFZVGVIQVMVOVNVL @@ -95267,7 +95267,7 @@ of the previous layer (and the union of previous layers when the rankpwi $p |- ( A e. U. ( R1 " On ) -> ( rank ` ~P A ) = suc ( rank ` A ) ) $= ( cr1 con0 cima cuni wcel crnk cfv csuc cpw wceq rankidn rankon r1suc ax-mp - wn eleq2i wss elpwi pwidg ssel syl2imc mtod r1rankidb sspwb sylib syl6sseqr + wn eleq2i wss elpwi pwidg ssel syl2imc mtod r1rankidb sspwb sylib sseqtrrdi syl5bi fvex elpw2 sylibr onsuci syl6eleqr wa wb pwwf sylbi mpbir2and eqcomd rankr1c ) ABCDEZFZAGHZIZAJZGHZVBVDVFKZVEVDBHZFZPZVEVDIBHZFZVBVIAVCBHZFZALVI VEVMJZFZVBVNVHVOVEVCCFVHVOKAMZVCNOZQVPVEVMRVBAVEFVNVEVMSAVATVEVMAUAUBUHUCVB @@ -95305,7 +95305,7 @@ of the previous layer (and the union of previous layers when the cuni crab rankdmr1 wlim word r1funlim simpri limord ordtr1 mpan2 ad2antlr wfun rankr1ag ralbidva biimpar an32s dfss3 simpll adantl rankr1bg adantrl mp2b mpbid sylbird pm2.18d alrimiv ssintab df-rab inteqi rankelb ralrimiv - syl6sseqr wceq eleq2 ralbidv onintss mpsyl eqssd ) CDEFULZGZCHIZBJZHIZAJZ + sseqtrrdi wceq eleq2 ralbidv onintss mpsyl eqssd ) CDEFULZGZCHIZBJZHIZAJZ GZBCKZAEUMZLZWKWLWOEGZWQMZAUAZLZWSWKXAWLWONZOZAUBWLXCNWKXEAWKXAXDWKXAMZXD XFXDPWOWLGZXDXFXDXGXFWLEGZWTXDXGPQCUCZWKWTWQUDWLWOUEUFUGWKWQXGXDOWTWKWQMZ XGXDXJXGMZCWODIZNZXDXKWMXLGZBCKZXMWKXGWQXOWKXGMZXOWQXPXNWPBCXPWMCGZMWMWJG @@ -96119,7 +96119,7 @@ C_ suc suc suc ( rank ` ( A u. B ) ) $= 17-Oct-2003.) $) cplem1 $p |- A. x e. A ( B =/= (/) -> ( B i^i D ) =/= (/) ) $= ( vw c0 wne cin wi cv wcel wex wceq crnk cfv wral scott0 eqeq1i necon3bii - wss crab bitr4i n0 bitri wa ssrab3 sseli ciun ssiun2 syl6sseqr sseld jcad + wss crab bitr4i n0 bitri wa ssrab3 sseli ciun ssiun2 sseqtrrdi sseld jcad a1i inelcm syl6 exlimdv syl5bi rgen ) EKLZEGMKLZNADVDJOZFPZJQZAODPZVEVDFK LVHEKFKEKRBOSTCOSTUECEUAZBEUFZKRFKRBCEUBFVKKHUCUGUDJFUHUIVIVGVEJVIVGVFEPZ VFGPZUJVEVIVGVLVMVGVLNVIFEVFVJBEFHUKULURVIFGVFVIFADFUMGADFUNIUOUPUQVFEGUS @@ -99858,7 +99858,7 @@ our Axiom of Choice (in the form of ~ ac2 ). The proof does not depend ( cfv con0 wceq wcel cr1 wf1 cuni cima crn csuc cv crnk comu co coa cif cmpt wa cvv wss wfun wfn cdm cep coi ccnv ccom tfr1 fnfun ax-mp sylancr funimaexg uniexg rnexg 3syl cxp cpw wral f1f fssxp ssv xpss1 sstr mpan2 - wf fvex elpw sylibr ralimi syl wb onss fndm syl6sseqr funimass4 sspwuni + wf fvex elpw sylibr ralimi syl wb onss fndm sseqtrrdi funimass4 sspwuni mpbird rnss sylc ad2antrr fveq2 f1eq1 f1eq2 bitrd ad2antlr eleqtrd word rankon rspcdva r1elwf rankidb ffvelrnd syl2anc char wwe adantr eleqtrrd wf1o frn f1of1 4syl wbr cen sseldd endomtr ex iftrue eqeq12d adantl a1i @@ -100897,7 +100897,7 @@ Because we use a disjoint union for cardinal addition (as explained in the fundmen 3syl fdm breqtrd jca ss2abi eqsstrri ssdomg domentr crn cmpt ovex mpisyl mptex rnex wrex wex wf1o ad2antll bren f1of adantl simplrl fssd wb sylib elmapd ad2antrr mpbird wfo f1ofo eqcomd ex eximdv mpd df-rex sylibr - forn ss2abdv eqid rnmpt syl6sseqr mpsyl wfn wral rgenw mp1i fodomnum sylc + forn ss2abdv eqid rnmpt sseqtrrdi mpsyl wfn wral rgenw mp1i fodomnum sylc fnmpt dffn4 domtr sbth 3ad2ant1 map0e 1oex enref csn df-sn en0 anbi2i 0ss df1o2 sseq1 mpbiri pm4.71ri bitr4i 3eqtr4ri breqtrri eqbrtrdi pm2.61ne abbii ) UABEFZCBEFZBCGUBZUCUDZHZUEZUUJAUFZBIZUUNCJFZKZALZJFZBMGUBZUUOUUNM @@ -101202,7 +101202,7 @@ Because we use a disjoint union for cardinal addition (as explained in the sseldi php3 ex sdomnen syl6 mt2d cv wral wa csuc ackbij1lem3 ackbij1lem12 syl fvex elpwi syl2an word wb ackbij1lem10 peano1 f0cli nnord ordsucsssuc mp2an csn ackbij1lem14 ackbij1lem8 eqtr3d sseqtrd sucssel mpsyl ralrimiva - adantr wfun cdm f1fun f1dm syl6sseqr funimass4 sylancr mpbird sspss orel1 + adantr wfun cdm f1fun f1dm sseqtrrdi funimass4 sylancr mpbird sspss orel1 sylc ) CGHZDCIZUAZXJUCJZUDZKXMXKXLLZUBZXNXIXMXKXLMNZXIXKXJMNZXJXLMNZXPGIO PZGDUMZXIXJXSQXJRHXQABDEUEZCUFZCGUGXSGXJDRUHUIXIXJOHZXLXJMNXRXICOHYCCUJCU KSZXJUNXLXJULUOXKXJXLUPUQXIXMXKXLURNZXPKXIXLOHZXMYEUSXIGOXLGUTOPOVAUTOVBV @@ -106318,7 +106318,7 @@ proved by Ernst Zermelo (the "Z" in ZFC) in 1904. (Contributed by Mario a1i word wss onordi ordelss sselda biimt syl ralbidva cima cif csn simprl cun onssi sseldi ttukeylem3 syldan ad3antrrr wn cpw cfn cin wf wrex simpr wex elin2d ciun elin1d wfn wfun cvv cdm crn cmpt tfr1 fnfun funiunfv mp2b - elpwid syl6sseqr dfss3 eliun ralbii bitri sylib eleq2d ac6sfi syl2anc wne + elpwid sseqtrrdi dfss3 eliun ralbii bitri sylib eleq2d ac6sfi syl2anc wne simp-4l simplrr ad2antrr simprrl adantr frn onss sstrd adantrr dffn4 fofi wfo ffn dm0rn0 eqeq1d syl5bbr necon3bid biimpar sseldd rspcdva ttukeylem2 fdmd ad2antrl expr ex ifclda uneq2 ordunifi syl3anc ffvelrn rnex ssonunii @@ -108556,7 +108556,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this wwe co ccnv csn cima wsbc wral relopabi simprr fpwwe2lem2 simprbda simprd a1i adantrl adantr df-ss sylib adantrr eqtr2d cvv wcel w3a adantlr simprl eqtrd fpwwe2lem10 mpjaodan ex alrimiv alrimivv dffun2 sylanbrc funfnd wex - vex elrn releldmi adantl elssuni syl syl6sseqr xpss12 syl2anc sstrd velpw + vex elrn releldmi adantl elssuni syl sseqtrrdi xpss12 syl2anc sstrd velpw cuni syl6ibr exlimdv syl5bi ssrdv df-f ) AGGUBZUCGUDZHHUEZUFZPXDXGGUGAGAG UHZNQZOQZGUIZXIUAQZGUIZRZXJXLSZUJZUAUKZOUKNUKGULXHABQZEPZIQZXRXRUEPZRXRXT UMZDQZXTYCYCUEZTFUNCQZSDXTUOYEUPZUQURCXRUSRRBIGJUTZVEAXQNOAXPUAAXNXOAXNRZ @@ -108581,7 +108581,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this wb simplbi brinxp2 breqd mpbird elind sseldd syl6eqss wo mpjaodan syl5bir expr rexlimdv exp32 alrimiv anbi12i bitr4i wor simplrl solin relelrni idd weso 3orim123d adantrr ad2antrl ssexd imp impr sylan2 impbid eliniseg elv - breq2 3bitr4g crn simprbda eqsstrid relopabi syl6sseqr xpss12 sstrd ssel2 + breq2 3bitr4g crn simprbda eqsstrid relopabi sseqtrrdi xpss12 sstrd ssel2 csn inex2 simplbda ad2ant2r wefr inss2 inelcm fri syl22anc elin1d simprll ralnex simp-4l simprlr mpbid elin2d syl21anbrc breq1 rspcev inss1 adantlr n0 w3a fpwwe2lem10 mtod ralrimiva reximssdv expimpd df-fr reeanv exdistrv @@ -108689,7 +108689,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this id eqrdv inxp dmss dmxpid ssneldd uneq2d eqcomd eleq1d rnss df-rn 3sstr3g rnxpid sseld sylbid ndmima sneqd imaeq2d cnvxp reseq1i ssid xpssres rneqi df-ima snnz rnxp cnvun imaeq1i eqtr3i 3eqtr4g df-ss xpindi 3eqtr3g jaodan - imaundir sylan2b ralrimiva mpbir2and relopabi releldmi syl6sseqr pm2.18da + imaundir sylan2b ralrimiva mpbir2and relopabi releldmi sseqtrrdi pm2.18da elssuni snss ) AHHGUEZFUFZHNZAVVKUGZOZVVJUHZHPVVKVVMVVNHVVNUIZHVVNHUJZVVM VVOGUKZUMZHVVMVVOVVIHVVNULZUIZGQZVVOVVQNVVOVVRPVVMVWAVVOEPZVVTVVOVVOULZPZ OZVVOVVTUNZDUOZVVTVWGVWGULZUPZFUFZCUOZRZDVVTUQZVWKUHZURZUSZCVVOUTZOZVVMVW @@ -108772,7 +108772,7 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this fpwwe2 $p |- ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) ) $= ( wcel wa wceq wss cin vw vz wbr co cfv cdm wfun wb cxp fpwwe2lem11 ffund - cpw funbrfv2b syl simprbda adantrr cuni elssuni syl6sseqr wi simpl a1i c0 + cpw funbrfv2b syl simprbda adantrr cuni elssuni sseqtrrdi wi simpl a1i c0 cdif simplrr wne cv wn wral wrex cvv wfr adantr wwe ccnv cima fpwwe2lem12 wsbc funfvbrb mpbid fpwwe2lem2 ad2antrr simpld ssexd difexg simprd difssd csn wefr fri syl21anc ssdif0 indif1 eqeq1i vex eliniseg elv notbii ralbii @@ -130112,7 +130112,7 @@ nonnegative integers (cont.)". $) $( The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.) $) uznnssnn $p |- ( N e. NN -> ( ZZ>= ` N ) C_ NN ) $= - ( cn wcel cuz cfv c1 wss elnnuz uzss sylbi nnuz syl6sseqr ) ABCZADEZFDEZBMA + ( cn wcel cuz cfv c1 wss elnnuz uzss sylbi nnuz sseqtrrdi ) ABCZADEZFDEZBMA OCNOGAHFAIJKL $. ${ @@ -152416,7 +152416,7 @@ computer programs (as last() or lastChar()), the terminology used for ( wcel caddc co cfz cconcat cpfx cc0 cop csubstr cn0 wceq cfv cword w3a c1 cmin ccatcl 3adant3 cuz chash lencl eqeltrid elfzuz peano2nn0 anim1i wa syl2an 3adant2 eluznn0 pfxval syl2anc 3simpa 3ad2ant1 0elfz cz nn0zd - syl wss adantr uzid peano2uz fzss1 eqcomi oveq2i syl6sseqr sseld 3impia + syl wss adantr uzid peano2uz fzss1 eqcomi oveq2i sseqtrrdi sseld 3impia 3syl pfxccatin12 sylc opeq2i mpdan pfxid eqtr3d syl5eq oveq1d 3eqtrd jca ) AFUAZIZBWGIZECUCJKZCDJKZLKZIZUBZABMKZENKZWOOEPQKZAOCPZQKZBECUDKNK ZMKZAWTMKWNWOWGIZERIZWPWQSWHWIXBWMFABUEUFWNWJRIZEWJUGTIZUNZXCWHWMXFWIWH @@ -156949,7 +156949,7 @@ a function (ordinarily on a subset of ` CC ` ) and produces a new { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) $= ( vz vw cc wcel cv cmin co wbr wa copab cvv cshi wceq caddc wrex cdm ovex cab crn cxp wss breldm npcan eqcomd ancoms oveq1 rspceeqv syl2anr rexbidv - vex eqeq1 elab sylibr brelrn adantl jca ssopab2dv df-xp syl6sseqr abrexex + vex eqeq1 elab sylibr brelrn adantl jca ssopab2dv df-xp sseqtrrdi abrexex expl dmex rnex xpex ssexg sylancl breq anbi2d oveq2 breq1d df-shft ovmpog opabbidv mp3an1 mpdan ) CHIZAJZHIZWBCKLZBJZDMZNZABOZPIZDCQLWHRZWAWHFJZGJZ CSLZRZGDUAZTZFUCZDUDZUEZUFWSPIWIWAWHWBWQIZWEWRIZNZABOWSWAWGXBABWAWCWFXBWA @@ -159628,7 +159628,7 @@ reflection about the origin (under the map ` x |-> -u x ` ). (Contributed ( vm cz wcel cv cuz cfv wral wrex cle wbr wi cr wa adantl eluzelre eleq2s adantr wb eluzelz eluz syl2an biimprd expimpd imim1d ralimdv2 imp reximi2 exp4a jca cfl c1 caddc co cif simpl flcl peano2zd zre reflcl peano2re syl - ifcld max1 eluz2 syl3anbrc syl6eleqr impexp syl6sseqr sselda simplr simpr + ifcld max1 eluz2 syl3anbrc syl6eleqr impexp sseqtrrdi sselda simplr simpr wss uzss zred fllep1 max2 letrd eluzle syl5bir wceq raleqdv rspcev syl6an ex fveq2 rexlimdva cbvrexv syl6ib impbid2 ) DHIZACBJZKLZMZBENZWQCJZOPZAQZ CEMZBRNZWSXDBERWQEIZWSSWQRIZXDXFXGWSXGWQDKLZEDWQUAFUBUCXFWSXDXFAXCCWREXFX @@ -164207,7 +164207,7 @@ seq N ( + , F ) e. dom ~~> ) ) $= cuz crp wa wss c0 wne w3a frnd wfn ffnd cz syl syl6eleqr fnfvelrn syl2anc uzid ne0d wb breq1 ralrn rexbidv mpbird 3jca suprcl ltsubrp sylan resubcl adantr rpre syl2an suprlub mpbid breq2 rexrn biimpa syldan wi wf ad2ant2r - ffvelrn uztrn2 ad2antrr simprr cfz fzssuz uzss syl6sseqr eleq2s ralrimiva + ffvelrn uztrn2 ad2antrr simprr cfz fzssuz uzss sseqtrrdi eleq2s ralrimiva ad2antrl sstrid ssralv r19.21bi c1 caddc sselda weq fveq2 fvoveq1 breq12d sylc rspccva monoord lesub2dd resubcld ad2antlr lelttr syl3anc abssuble0d mpand ltsub23 suprub 3imtr4d anassrs ralrimdva reximdva mpd cvv fvexi fex @@ -169753,7 +169753,7 @@ attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof ( ( seq M ( x. , F ) ` N ) x. A ) ) $= ( cmul cfv co cc wcel wceq wi fveq2 oveq2d vx vn cseq c1 caddc cvv cuz cz eqid uzssz eqsstri peano2zd syl6eleq eluzel2 syl prodf ffvelrnd seqex a1i - sseldi cv wss peano2uz uzss 3syl syl6sseqr sselda syldan ffvelrnda imbi2d + sseldi cv wss peano2uz uzss 3syl sseqtrrdi sselda syldan ffvelrnda imbi2d eqeq12d weq wa adantr seqp1 seq1 adantl eqtr4d expcom syl6eleqr ralrimiva oveq1 wral eleq1d rspcv mpan9 mulassd 3eqtrd exp31 com12 uzind4 climmulc2 a2d impcom ) ABFLDEUCZMZCLDFUDUENZUCZWOWQUFWQUGMZWSUIZAFAGUHFGEUGMZUHHEUJ @@ -170898,7 +170898,7 @@ seq m ( x. , F ) ~~> x ) \/ cv wex cuz syl6eleq peano2uz syl syl6eleqr ax-1ne0 eqid cz eluzelz eleq2s cvv peano2zd seqex a1i 1cnd csn cxp simpr cfz csb wss ad2antrr w3a cle wn clt zred elfzelz adantl ltp1d elfzle1 ltletrd mpbid intnand elfz2 sylnibr - ltnled ssneldd iffalsed fzssuz adantr uzss syl6sseqr sstrid sselda ax-1cn + ltnled ssneldd iffalsed fzssuz adantr uzss sseqtrrdi sstrid sselda ax-1cn syl6eqel nfcv nfv nfcsb1v nfif weq eleq1w csbeq1a ifbieq1d fvmptf syl2anc cc elfzuz 1ex fvconst2 3eqtr4d seqfveq prodf1 eqtrd climconst neeq1 breq2 anbi12d spcev sylancr seqeq1 breq1d anbi2d exbidv rspcev ) AHMUBUCZINBUJZ @@ -184694,7 +184694,7 @@ reduced fraction representation (no common factors, denominator seqp1 sylibd mpan2d sylan2br wf1 wral moddvds coprmdvds elfzole1 elfzolt2 eleq2i clt modid sylan cfn mp2an sylancl mpbid caddc crp simp2d cfzo f1of eluzfz1 nnrpd seq1i exp1d seq1 ax-mp a1i oveq2i syl5eq nnre peano2re letr - jca mpand imdistanda imim1d nnnn0 simprl simprr letrd nnz fzss2 syl6sseqr + jca mpand imdistanda imim1d nnnn0 simprl simprr letrd nnz fzss2 sseqtrrdi eluz sselda zmulcl ssrab3 eulerthlem1 nnge1d elfz mpbir2and 3expia expp1d peano2nn mul4d modcld syl221anc recnd 3eqtr4d rpmul sylibrd anim12d an12s a2d syld nnind mpcom mpdan nnnn0d ccnv ccom mulcl mulcom w3a mulass ssidd @@ -190260,7 +190260,7 @@ with complex numbers (gaussian integers) instead, so that we only have ( wcel cfv cv cle wbr wi wal cn0 wss wral wa cxr sseldi cvv cuz crab wceq chash breq1 imbi1d albidv elrab2 simplbi eluznn0 ssrdv syl simprbi eluzle ex adantl cr nn0ssre ressxr sstri adantr vex hashxrcl mp1i xrletr syl3anc - sylan mpand imim1d ralrimdva alimdv mpd ralcom4 sylibr sylanbrc syl6sseqr + sylan mpand imim1d ralrimdva alimdv mpd ralcom4 sylibr sylanbrc sseqtrrdi ssrab ) DBGZDUAHZCIZEIZUDHZJKZALZEMZCNUBZBVRVSNOZWECVSPZVSWFOVRDNGZWGVRWI DWBJKZALZEMZWEWLCDNBVTDUCZWDWKEWMWCWJAVTDWBJUEUFUGFUHZUIZWICVSNWIVTVSGZVT NGZVTDUJZUOUKULVRWDCVSPZEMZWHVRWLWTVRWIWLWNUMVRWKWSEVRWKWDCVSVRWPQZWCWJAX @@ -199004,7 +199004,7 @@ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> ( vr vq vi cv cen wbr cun wcel wa cpw wrex c0 wceq cmre cfv adantr cdif csn wral wss animorrl mreexexlem3d wne n0 biimpi adantl wn mreexexlem2d wex simpr w3a 3anass cvv ad2antrr elfvexd simpr2 difsnb ssdifssd ssdifd - sylib difun1 syl6sseqr simpr1 uncom uneq2i unass difsnid uneq1d syl5eqr + sylib difun1 sseqtrrdi simpr1 uncom uneq2i unass difsnid uneq1d syl5eqr eqsstrrd syl5eq syl fveq2d sseqtrrd simpr3 csuc wo com wi simplr dif1en 3anan12 sylbir expcom syl2anc orim12d mpd mreexexlemd ad3antrrr difss2d wal ssexd simprl simplr1 snssd unssd sselpwd ad3antlr cin simprrl en2sn @@ -199114,7 +199114,7 @@ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> immediate consequence of ~ mreexexd . (Contributed by David Moews, 1-May-2017.) $) mreexdomd $p |- ( ph -> S ~<_ T ) $= - ( vi c0 cv cen wbr cun wcel wa cdom cpw cdif mrissd dif0 syl6sseqr fveq2i + ( vi c0 cv cen wbr cun wcel wa cdom cpw cdif mrissd dif0 sseqtrrdi fveq2i cfv un0 eqeltrid mreexexd simprrl wss simprl elpwid wi cmre elfvexd ssexd cvv ssdomg syl adantr mpd endomtr syl2anc rexlimddv ) AESUAZUBUCZVNTUDGUE ZUFZEFUGUCZSFUHZABCDEFTGHIJSKLMNAEIITUIZADEGIMKRUJIUKZULAFIVTPWAULAEFHUNF @@ -215821,7 +215821,7 @@ arbitrary magmas (then it should be called "iterated sum"). If the magma is wfun simpr sseldd seqfeq4 eqeq2d pm5.32da rexbidva exbidv iotabidv ccnv cvv cdif difeq2d imaeq2d 3eqtr4g fveq2d ad3antrrr f1ofun ad3antlr f1odm cima oveq2d eqtrd difpreima syl syl5eq difss syl6eqss dfdm4 dfrn4 eqtri - fvco syl6sseqr ad4ant14 wn c0 wfn 1z seqfn fndm mp2b eleq2i ndmfv bitrd + fvco sseqtrrdi ad4ant14 wn c0 wfn 1z seqfn fndm mp2b eleq2i ndmfv bitrd sylnibr eqid a1i gsumvalx wf f1of ffvelrnd eqeltrd caovclg cz pm2.61dan eqtr4d f1oeq2d f1oeq3d anbi1d ifeq12d ifbieq12d 3eqtr4d ) AEUHZKUIZBUIZ FUJUKZULZUUQUMZUUQUUPUURULZUUQUMZUTZBFUNUKZUOZKUVDUPZUQZFURUKZEUSZVAUHV @@ -234425,7 +234425,7 @@ elements of arbitrarily large orders (so ` E ` is zero) but no elements ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) $= ( vf vy vn vz vw c0 wceq cof co cgsu chash cfv cn wcel c1 cfz cv wex wa wf1o cmnd mndidcl syl mndlid syl2anc adantr cvv c0g fvexi a1i csupp cun - cmpt wf fex suppun syl6sseqr gsumcllem oveq2d gsumz eqtrd uncom oveq12d + cmpt wf fex suppun sseqtrrdi gsumcllem oveq2d gsumz eqtrd uncom oveq12d ad2antrr ex ccom cseq mndcl 3expb sylan cuz nnuz wf1 wss f1of1 ad2antll cdm suppssdm fdmd syl6eq fco ffvelrnda ffnd inidm wfn fnfco eqidd ofval adantl adantlr syldan seqcl ffvelrn syl2an cima cres csn cdif wral expr @@ -235630,7 +235630,7 @@ elements of arbitrarily large orders (so ` E ` is zero) but no elements ( j e. D |-> ( G gsum ( k e. ( A " { j } ) |-> ( j F k ) ) ) ) ) ) $= ( csupp co cdm cres cgsu cv csn cima cmpt gsum2dlem2 cvv cxp cin suppssdm fssdm wrel wss relss sylc crn relssdmrn ssv xpss2 ax-mp syl6ss syl df-res - ssind syl6sseqr gsumres dmss resmptd oveq2d wcel gsum2dlem1 adantr fmpttd + ssind sseqtrrdi gsumres dmss resmptd oveq2d wcel gsum2dlem1 adantr fmpttd sstrd cdif wa wceq cop vex elimasn biimpi ad2antll eldifn ad2antrl opeldm nsyl eldifd cfv df-ov ssidd c0g fvexi a1i suppssr syl5eq syldan mpteq2dva wn anassrs cmnd ccmn cmnmnd imaexg gsumz syl2anc eqtrd suppss2 cfsupp wbr @@ -236187,7 +236187,7 @@ Group sums over (ranges of) integers adantr syl3anc ralrimiva wceq wi rspsbca wb sbcimg sbcbr2g csbvarg breq2d wbr bitrd sbceq1g imbi12d elv sylib expcom imp31 cr nn0red nn0re ad2antlr wsbc ltp1d lttrd ex ovex ax-mp syld imp oveq12d grpidcl grpsubid syl2anc2 - eqtrd gsummptnn0fz wss cuz fzssuz nn0uz syl6sseqr ssralv sylc telgsumfz0s + eqtrd gsummptnn0fz wss cuz fzssuz nn0uz sseqtrrdi ssralv sylc telgsumfz0s cfv a1i syl3c oveq2d 0nn0 grpsubid1 3eqtrd ) AGEQFEUAZCUBZFXPUCUDUMZCUBZH UMZUEUFUMGEUGDUHUMXTUEUFUMFUGCUBZFDUCUDUMZCUBZHUMZYAABXTDEGIJMAGUIRZGUJRK GUKULAXTBRZEQAXPQRZUNZGUORZXQBRZXSBRZYFAYIYGAYEYIKGUPULZVDZYHYGCBRZFQUQZY @@ -238345,7 +238345,7 @@ factorization into prime power factors (even if the exponents are cacs subgacs acsmre eldifi adantl snssd mrcsscl syl3anc wb subgss syl 4syl sseldd mrcsncl syl2anc eqeltrid lsmsubg2 sselda sylan2 lsmlub wn mpbi2and wpss wi lsmub1 lsmub2 mrcssidd snssg mpbird eldifn ssnelpssd - syl6sseqr cv psseq1 anbi12d psseq2 notbid imbi12d wral rspcdva mpan2d + sseqtrrdi cv psseq1 anbi12d psseq2 notbid imbi12d wral rspcdva mpan2d eleq2 mt2d npss sylib mpd ) AEIHNGUMZUNUOZUPZXMEUQZLURZGUMZIUSZXRIUTZ XOXMIUSZXQIUSZXSAYAXNUKVAXOKVBURZDVCURUOZXPIUSIYCUOZYBAYDXNAKVDUOZKVE UOYCDVGURUOYDUDKVFDKRVHYCDVIVRZVAZXOEIXNEIUOZAEIXMVJZVKVLAYEXNUGVAZYC @@ -238430,7 +238430,7 @@ factorization into prime power factors (even if the exponents are cmre subgacs acsmred subgss sseldd mrcsncl eqeltrid syl3anc subg0cl cacs lsmsubg2 snssd adantr eleqtrd cmul nnne0d cz subgmulgcl mulgcl syl13anc mulgass eldifad grpidcl en1eqsn ex syld mt3d cdiv divcan1d - sylan eqtr4d nndivdvds nnzd zmulcld mrcssidd syl6sseqr snssg cplusg + sylan eqtr4d nndivdvds nnzd zmulcld mrcssidd sseqtrrdi snssg cplusg cin prmz eqid mulgdi oveq1d gexid 3eqtr3rd oveq12d 3eqtr2d eqeltrrd grplid elind elsni oddvds eqbrtrrd dvdscmulr syl112anc jca ) AFKUTV AZFNUTVAZAUVPEHPGVBZVCZAEJUVRUOVDAUVPVEZDVFVGVAZUVSAUVTFFKVHVBZVIVB @@ -238475,7 +238475,7 @@ factorization into prime power factors (even if the exponents are wb subgcl lsmsubg2 cvv oveq2 adantr ad3antrrr cmul oveq1d subgsubcl zcnd cc wn syl5eq eleq1d sylibd c1 zmulcld syl13anc mulcomd mulgass eqtrd eqtr3d oveq2d eqeltrd rexlimdvva sylbid elin subg0cl eqeq1d - zcn cprime cpgp pgpprm prmnn nnne0d mrcssidd syl6sseqr snssg mpbird + zcn cprime cpgp pgpprm prmnn nnne0d mrcssidd sseqtrrdi snssg mpbird prmz csg lsmelvalm cmpt crn cycsubg2 rexeqdv wral ovex rgenw eqeq2d cn rexrnmpt ax-mp syl6bb rexbidv bitrd simpr simplrl nncnd divcan1d simplrr eldifbd wi 3expia impancom oveq1i grppncan mtod coprm caddc @@ -238591,7 +238591,7 @@ factorization into prime power factors (even if the exponents are wi crab ccrd cdm c0 wne wss crpss wor w3a cuni wal cfn cpw sylib adantr pwfi subgss 3ad2ant2 velpw sylibr rabssdv ssfid syl cmre cgrp cacs cabl finnum ablgrp subgacs acsmre 3syl sseldd mrcsncl syl2anc eqeltrid simpr - snssd sstrd mrcssidd syl6sseqr snssg mpbird psseq1 eleq2 anbi12d rspcev + snssd sstrd mrcssidd sseqtrrdi snssg mpbird psseq1 eleq2 anbi12d rspcev syl12anc rabn0 simpr1 simpr2 simpr3 fin1a2lem10 syl3anc alrimiv zornn0g wb ex weq ralrab rexbii r19.29 elrab ineq2 oveq2 cbvrexv cdif ad3antrrr eqeq1d adantrr notbid impd rexlimdva simprrl ad2antrr psseq1d pssdif n0 @@ -250163,7 +250163,7 @@ division ring is an Abelian group (vectors) together with a division ring lspsolvlem $p |- ( ph -> E. r e. B ( X .+ ( r .x. Y ) ) e. ( N ` A ) ) $= ( va vx vy vs vt wcel cv cfv wrex csn cun clmod wss ssrab3 a1i crab c0g co adantr eqid lmod0cl syl wceq lmod0vs syl2anc oveq2d sselda lmod0vrid - eqtrd lspssid eqeltrd oveq1 eleq1d rspcev ssrabdv syl6sseqr cur cminusg + eqtrd lspssid eqeltrd oveq1 eleq1d rspcev ssrabdv sseqtrrdi cur cminusg cgrp lmodfgrp lmod1cl grpinvcl lmodvneg1 lmodgrp grprinv lss0cl rexbidv wa lspcl elrab2 sylanbrc snssd unssd lspss syl3anc csca cbs cplusg clss cvsca ne0d weq cbvrexv syl6bb anbi12i an4 bitri simp1ll simp1lr simp1rl @@ -250607,7 +250607,7 @@ U C_ ( N ` { X } ) ) -> ( U = ( N ` { X } ) \/ U = { .0. } ) ) $= sspwuni mp1i lspss syl3anc simp3l sseldd ssun2 simp3r eqid lsscl eliuni syl13anc syl6eleqr 3expia rexlimdvva syl5bi exp4b 3imp2 islssd eldifi adantl eldifn eldif lspssid adantlr sseld syl5bir mpan2d eluni2 3imtr4g - ad2antlr reximdva mpd ex ssrdv syl6sseqr jca ) AIGULEUMZBUNZUOZUPZIUQAU + ad2antlr reximdva mpd ex ssrdv sseqtrrdi jca ) AIGULEUMZBUNZUOZUPZIUQAU FMURUSZUTUSZMVAUSZGMVBUSZIUVBLMUGUHAUVBVCAUVCVCLMUTUSVDANVEAUVDVCAUVEVC GMVFUSVDAUAVEAIDEDUNZUUTUPZKUSZVGZLUEAUVHLUQZDEVHUVILUQAUVJDEAMVIULZUVF EULZUVGLUQZUVJAMVJULUVKQMVKVLZAUVLVMZUVFLUUTUVOUVFLAELVNZUVFAEHUVPUBFCU @@ -266242,7 +266242,7 @@ is based on direct sums of abelian groups ("We define on [the direct sum of mpbid simpld prdsplusgcl cplusg adantr wfn simpr prdsplusgfval rabbidva wa neeq1d cun simprd unfi syl2anc wceq neorian bicomi con1bii ffvelrnda wo wn mndlid syl2anc2 oveq12 eqeq1d syl5ibrcom syl5bi necon1ad ss2rabdv - mndidcl unrab syl6sseqr ssfid eqeltrd mpbir2and ) AHICUBZFTWKBUCUDZTUAU + mndidcl unrab sseqtrrdi ssfid eqeltrd mpbir2and ) AHICUBZFTWKBUCUDZTUAU EZWKUDZWMDUDZUFUDZUGZUAGUHZUITAWLCDEHIGJKBLWLUJZSONPAHWLTZWMHUDZWPUGZUA GUHZUITZAHFTWTXDVDQAWLEDUKUBZBDEFGKHUALXEUJZWSMNAGULDPUMZUNUOZUPZAIWLTZ WMIUDZWPUGZUAGUHZUITZAIFTXJXNVDRAWLXEBDEFGKIUALXFWSMNXGUNUOZUPZUQAWRXAX @@ -281963,7 +281963,7 @@ _Introduction to General Topology_ (1983), p. 114) and it is convenient $( A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) $) eltopss $p |- ( ( J e. Top /\ A e. J ) -> A C_ X ) $= - ( wcel wss ctop cuni elssuni syl6sseqr adantl ) ABEZACFBGELABHCABIDJK $. + ( wcel wss ctop cuni elssuni sseqtrrdi adantl ) ABEZACFBGELABHCABIDJK $. $( A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) $) @@ -283299,7 +283299,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on $( The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.) $) difopn $p |- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A \ B ) e. J ) $= - ( wcel ccld cfv wa cin cdif wss wceq elssuni syl6sseqr adantr df-ss sylib + ( wcel ccld cfv wa cin cdif wss wceq elssuni sseqtrrdi adantr df-ss sylib cuni adantl difeq1d indif2 cldrcl simpl cldopn syl3anc eqeltrrid eqeltrrd ctop inopn ) ACFZBCGHFZIZADJZBKZABKCUMUNABUMADLZUNAMUKUPULUKACSDACNEOPADQ RUAUMUOADBKZJZCADBUBUMCUIFZUKUQCFZURCFULUSUKBCUCTUKULUDULUTUKBCDEUETAUQCU @@ -284780,7 +284780,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on ( topGen ` ( B |`t A ) ) = ( ( topGen ` B ) |`t A ) ) $= ( vx vy vz vw wcel wa crest ctg cv wss cuni wceq wex cvv cin crn cfv ovex co wb eltg3 ax-mp cmpt cima wfun simpll funmpt restval sseq2d biimpa wral - a1i wfn inex1 rgenw eqid fnmpt fnima mp2b syl6sseqr ssimaexg syl3anc ciun + a1i wfn inex1 rgenw eqid fnmpt fnima mp2b sseqtrrdi ssimaexg syl3anc ciun vex wi cres df-ima resmpt adantl rneqd syl5eq unieqd dfiun3 iunin1 syl6eq syl6eqr fvex simpr uniiun eltg3i eqeltrrid adantlr elrestr eqeltrd eleq1d mp3an2ani unieq syl5ibrcom expimpd exlimdv adantr mpd eleq1 ssrdv sylancr @@ -285190,7 +285190,7 @@ we show (in ~ tgcl ) that ` ( topGen `` B ) ` is indeed a topology (on Carneiro, 25-Dec-2016.) $) perfopn $p |- ( ( J e. Perf /\ Y e. J ) -> K e. Perf ) $= ( vx cperf wcel wa ctop cv wn cuni wral ctopon cfv wss adantr syl perftop - csn crest co toptopon elssuni adantl syl6sseqr resttopon syl2anc eqeltrid + csn crest co toptopon elssuni adantl sseqtrrdi resttopon syl2anc eqeltrid sylib topontop sselda perfi adantlr syldan eleq2i wb restopn2 sylan simpl syl6bi syl5bi mtod ralrimiva wceq toponuni raleqdv mpbid isperf3 sylanbrc eqid ) AHIZDAIZJZBKIZGLZUBZBIZMZGBNZOZBHIVPBDPQZIZVQVPBADUCUDZWDFVPACPQIZ @@ -285767,7 +285767,7 @@ information ensuring that it is not too fine (and of course ~ iooordt ifcl w3a breq1 ifboth xrre2 syl32anc xrmax2 df-ioc xrlelttr ixxss1 simplr eqsstrrd sstrd oveq1 sseq1d rspcev rexlimdvaa com12 wn pnfnlt elico1 mpan sylbi simp3 syl6bi mtod notbid syl5ibrcom rexlimiv pm2.21d adantrd pnfnre - eleq2 jaoi neli cuni elssuni unirnioo syl6sseqr sseld mtoi syl sylanb ) B + eleq2 jaoi neli cuni elssuni unirnioo sseqtrrdi sseld mtoi syl sylanb ) B EUDUEZFBCGCUFZHIJZUGZUHZCGKYEUIJZUGZUHZUJZUKUHZUJZULUEZFZHBFZAUFZHIJZBLZA MNZYDYOBCYHYKYMYHOYKOYMOUMUNYPYQPHDUFZFZUUBBLZPZDYNNUUADBYNHUQUUEUUADYNUU BYNFUUBYLFZUUBYMFZUOUUEUUAURZUUBYLYMUPUUFUUHUUGUUFUUBYHFZUUBYKFZUOUUHUUBY @@ -285796,7 +285796,7 @@ information ensuring that it is not too fine (and of course ~ iooordt cif a1i 0xr simprl mnflt0 simpll simprr eleqtrd elico1 mpbid simp3d breq2 ifcl ifboth xrmin1 0re ltpnf mp1i xrlelttrd syl32anc xrmin2 df-ico ixxss2 xrre2 xrltletr simplr eqsstrrd sstrd oveq2 sseq1d rspcev rexlimdvaa com12 - syl2anc jaoi mnfnre neli cuni elssuni unirnioo syl6sseqr sseld syl sylanb + syl2anc jaoi mnfnre neli cuni elssuni unirnioo sseqtrrdi sseld syl sylanb mtoi ) BEUDUEZFBCGCUFZHUGIZUHZUIZCGJYGKIZUHZUIZUJZUKUIZUJZULUEZFZJBFZJAUF ZKIZBLZAMNZYFYQBCYJYMYOYJTYMTYOTUMUNYRYSOJDUFZFZUUDBLZOZDYPNUUCDBYPJUPUUG UUCDYPUUDYPFUUDYNFZUUDYOFZUOUUGUUCUQZUUDYNYOURUUHUUJUUIUUHUUDYJFZUUDYMFZU @@ -287924,7 +287924,7 @@ require the space to be Hausdorff (which would make it the same as T_3), ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> E. x e. J E. y e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) ) $= ( wcel cfv w3a wa cv wss cin c0 wceq wrex cdif syl2anc syl creg ccld ctop - ccl regtop ad2antrr cuni elssuni syl6sseqr ad2antrl clscld cldopn simprrr + ccl regtop ad2antrr cuni elssuni sseqtrrdi ad2antrl clscld cldopn simprrr wn wb clsss3 simplr1 cldss ssconb mpbid simprrl sscls sslin incom disjdif eqtri sseq0 sseq2 ineq1 eqeq1d 3anbi13d rspcev simpl simpr1 simpr2 simpr3 sylancl syl13anc eldifd regsep syl3anc reximddv rexcom sylib ) EUAHZDEUBI @@ -288208,7 +288208,7 @@ require the space to be Hausdorff (which would make it the same as T_3), ccmp co w3a ctop cpw cin wrex wi cntop2 3ad2ant3 elpwi ccnv simpl1 simpl3 cmpt crn simprl sselda cnima syl2an2r fmpttd frnd simprr imaeq2d eqid cnf wf fimacnv ciun cab ralrimiva dfiun2g imauni rnmpt unieqi 3eqtr4g 3eqtr3d - cmpcov syl3anc simprll simpll2 elssuni syl6sseqr foimacnv syl2anc eqeltrd + cmpcov syl3anc simprll simpll2 elssuni sseqtrrdi foimacnv syl2anc eqeltrd elfpw simpr imaeq2 eleq1d ralrnmpt mpbird adantr r19.21bi simprlr abrexfi wb syldan eqeltrid sylanbrc cdm fdmd fof fdm foima unieq rspceeqv sylan2b 3syl expr rexlimdva mpd sylan2 iscmp ) BUFKZDEAUDZABCUEUGKZUHZCUIKZEGLZMZ @@ -288502,7 +288502,7 @@ require the space to be Hausdorff (which would make it the same as T_3), crest cpw cin simpll wb ssun1 sseq2 mpbiri ad2antlr cmpsub syl2anc simprr wral sseqtrd unieq sseq2d pweq ineq1d rexeqdv imbi12d rspcv ad2antrl mpid sylbid ssun2 reeanv elinel1 elpwid anim12i unss sylib elinel2 unfi syl2an - jca elin vex elpw2 anbi1i bitr2i simpllr ssun3 ad2antll eqsstrd syl6sseqr + jca elin vex elpw2 anbi1i bitr2i simpllr ssun3 ad2antll eqsstrd sseqtrrdi ssun4 uniun elpwi adantr sstrd uniss syl eqssd rspceeqv rexlimdvv syl5bir exp32 syl2and impancom expd ralrimiv iscmp sylanbrc ) CUALZDABUBZMZNZCAUE UCUDLZCBUEUCUDLZNZNZXHDFOZPZMZDGOZPZMGXPUFZQUGZRZSZFCUFZUQCUDLXHXJXNUHXOY @@ -288605,7 +288605,7 @@ require the space to be Hausdorff (which would make it the same as T_3), id anbi2d elrab2 simprbi syl6 ralrimiv ac6sfi syl2anr ad2antlr crn cint sylbi frn ad2antrl simprr simpl cdm dm0rn0 fdm eqeq1d necon3bid biimpac syl5rbbr syl2an wfo wfn ffn dffn4 adantr w3a syl13anc ad2antll wb eliin - ciin elssuni syl6sseqr syl2anc ralrimiva adantrr ssel ral2imi cvv ssrdv + ciin elssuni sseqtrrdi syl2anc ralrimiva adantrr ssel ral2imi cvv ssrdv elv 3imtr4g eqsstrd clsss2 wi sstrd ex anim2d reximdva mpd fofi fiinopn sylib imp ralimi mpbird fnrnfv inteqd fvex dfiin2 syl6eqr eleqtrrd ccld ad4antr ffvelrn adantll clscld iincld sscls ciun iindif2 simplrl uniiun @@ -288667,7 +288667,7 @@ require the space to be Hausdorff (which would make it the same as T_3), ( J |`t S ) e. Comp ) -> S e. ( Clsd ` J ) ) $= ( vx vz vy vw cha wcel wss cfv cdif wel cv wa wrex wi syl wb crest co w3a ccmp ccld simp2 wral crab eqid simpl1 simpl2 simpl3 simpr hauscmplem ctop - ccl haustop 3ad2ant1 elssuni syl6sseqr sscls syl2an sstr2 anim2d reximdva + ccl haustop 3ad2ant1 elssuni sseqtrrdi sscls syl2an sstr2 anim2d reximdva cuni adantr mpd ralrimiva eltop2 mpbird iscld mpbir2and ) BIJZACKZBAUAUBU DJZUCZABUELJZVOCAMZBJZVNVOVPUFVQVTEFNZFOZVSKZPZFBQZEVSUGZVQWEEVSVQEOZVSJZ PZWAWBBUPLZLZVSKZPZFBQZWEWIGFHWGABEHNHOWJLCGOMKPHBQGBUHZCDWOUIVNVOVPWHUJV @@ -288868,7 +288868,7 @@ require the space to be Hausdorff (which would make it the same as T_3), two nonempty non-overlapping open sets. (Contributed by FL, 16-Nov-2008.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) $) conndisj $p |- ( ph -> ( A u. B ) =/= X ) $= - ( c0 wne wceq cdif wss cin wcel adantr cun wb elssuni syl6sseqr uneqdifeq + ( c0 wne wceq cdif wss cin wcel adantr cun wb elssuni sseqtrrdi uneqdifeq cuni syl syl2anc simpr difeq2d dfss4 sylib cconn ccld cfv ctop cpr isconn wa simplbi opncld eqeltrrd connclo difid syl6eq 3eqtr3d ex sylbid necon3d mpd ) ABMNBCUAZENIAVKEBMAVKEOZEBPZCOZBMOZABEQZBCRMOVLVNUBABDUFZEABDSZBVQQ @@ -288966,7 +288966,7 @@ require the space to be Hausdorff (which would make it the same as T_3), K e. Conn ) $= ( vx cconn wcel ccld cfv cin c0 wss wa wceq wne cima syl2anc syl wfo ctop ccn co w3a cpr cntop2 3ad2ant3 cv wo wn df-ne ccnv cuni cdm simpl1 simpl3 - eqid simprl elin1d cnima crn elssuni syl6sseqr simpl2 forn sseqtrrd df-rn + eqid simprl elin1d cnima crn elssuni sseqtrrdi simpl2 forn sseqtrrd df-rn syl6sseq sseqin2 sylib simprr eqnetrd imadisj necon3bii sylibr cnclima wf elin2d connclo cnf fdm fof 3eqtr2d imaeq2d foimacnv foima 3eqtr3d syl5bir 3syl expr orrd vex elpr ex ssrdv isconn2 sylanbrc ) BHIZDEAUAZABCUCUDIZUE @@ -289197,7 +289197,7 @@ require the space to be Hausdorff (which would make it the same as T_3), ( ( T C_ X /\ A e. T /\ ( J |`t T ) e. Conn ) -> T C_ S ) $= ( vy wss wcel crest co cconn cv wa cvv wceq eleq2 oveq2 eleq1d crab simp1 w3a cuni ctop wb conntop 3ad2ant3 restrcl simprd elpwg 3syl mpbird 3simpc - cpw anbi12d cbvrabv elrab2 sylanbrc elssuni syl syl6sseqr ) DFIZBDJZEDKLZ + cpw anbi12d cbvrabv elrab2 sylanbrc elssuni syl sseqtrrdi ) DFIZBDJZEDKLZ MJZUCZDBANZJZEVHKLZMJZOZAFUOZUAZUDZCVGDVNJZDVOIVGDVMJZVDVFOZVPVGVQVCVCVDV FUBVGVEUEJZDPJZVQVCUFVFVCVSVDVEUGUHVSEPJVTDEUIUJDFPUKULUMVCVDVFUNBHNZJZEW AKLZMJZOZVRHDVMVNWADQZWBVDWDVFWADBRWFWCVEMWADEKSTUPVLWEAHVMVHWAQZVIWBVKWD @@ -289543,7 +289543,7 @@ require the space to be Hausdorff (which would make it the same as T_3), relopabi eqeltrrd df-br fvex simpl sseq1 sseq2 bi2anan9 rexbidv 3anbi123d eleq1d bitr3i simp3bi syl fvi ad3antrrr rexeqdv mpbird ralrimiva axcc4dom braba anbi12d ad2antrr feq3d anbi1d crn 2ndctop adantl frn ad2antrl bastg - ctop syl6sseqr sstrd simprrl simprr ad2antlr eleqtrrd simprrr tg2 sseqtrd + ctop sseqtrrdi sstrd simprrl simprr ad2antlr eleqtrrd simprrr tg2 sseqtrd simprl sseldd simplrl weq rspcev syl12anc syl3anbrc wi fveq2 ex rexlimddv sseq12d eqeq2i biimpi syl6req wfn ffn fnfvelrn simplll rspcv op1st sseq1i op2nd sseq2i anbi12i simplrr jca syl5bi syldc exp4c imp41 eleq2 ralrimivv @@ -290143,7 +290143,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually E. u e. J ( y e. u /\ ( J |`t u ) e. A ) ) ) ) $= ( vv vz wcel cv crest co wa wral syl3anc wceq clly ctop llytop adantl wss wrex w3a simplr adantr topopn syl simpr llyi 3simpc ralrimiva jca cpw cin - reximi simprl cuni elssuni syl6sseqr ssralv simpllr simplrl inopn cvv vex + reximi simprl cuni elssuni sseqtrrdi ssralv simpllr simplrl inopn cvv vex wi inss1 elpwi2 a1i elind simplrr simprrl inss2 restabs eleq1d raleqbi1dv oveq2 oveq1 ralrimivva ad3antrrr simprrr rspcdva elrestr eqeltrrd anbi12d eleq2 rspcev syl12anc rexlimdvaa anassrs ralimdva syld ralrimdva sylanbrc @@ -290877,7 +290877,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually vx vf cptfin wrex cpw elpwi w3a cin cmpcov elfpw finptfin anassrs ancom1s anim1i sylanb reximi2 3exp syl5 ralrimiv 0elpw 0fin elini syl6eq rspceeqv unieq uni0 mpan a1i13 wne wex n0 wel eleq2d biimpd eluni2 syl6ib cun cmpt - simp2 ciun simpl3 simprl sseldd elssuni syl6sseqr ralrimivw iunss ssequn1 + simp2 ciun simpl3 simprl sseldd elssuni sseqtrrdi ralrimivw iunss ssequn1 crn sylibr sylib simpl2 uniiun uneq2d eqtr3d iunun vex unex dfiun3 eqtr3i simpll1 adantr sselda unopn syl3anc fmpttd frnd wb elpw2g 3ad2ant1 mpbird eqeq2d sseq2 anbi1d rexbidv imbi12d rspcv mpid crab ssel2 adantrr syl2anc @@ -291216,7 +291216,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually eleq1d sylan elun2 anassrs ad2antlr cz nnz ralrimiva rexlimddv elun1 wo adantlr elnnuz anbi1i elfzuzb bitr4i funimass4 uztric mpjaodan fnfvrnss sylan2b syl2an uniun unisn uneq2i eqtri unieq sseq2d rspcev expr mpbird - syl6sseqr ) ADCUDZBUEZUFZUIUJUKKZUVFILZMZNZUVFUALZMZNZUAUVHULZOUMZUNZUO + sseqtrrdi ) ADCUDZBUEZUFZUIUJUKKZUVFILZMZNZUVFUALZMZNZUAUVHULZOUMZUNZUO ZIDULZUPZAUVQIUVRAUVHUVRKZUVJUVPAUVTUVJPZPZBUBLZKZUVPUBUVHUWBBUVIKUWDUB UVHUNUWBUVFUVIBAUVTUVJUQABUVFKZUWAAUWEUVEUVFNZUVEUVDURABEKZUWEUWFUSADEU TQKZCBDVAQVBZUWGFHBCDEVCRZBUVFEVDSVEVFVGUBBUVHVHVIUWBUWCUVHKZUWDPZPZUCL @@ -291440,7 +291440,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually ( vz vr vs cxp cv wcel wa wrex wss wceq vw cuni relxp cop eleq2i eluni2 bitri anbi12i opelxp reeanv 3bitr4i eqid xpeq1 eqeq2d xpeq2 rspc2ev vex mp3an3 xpex eqeq1 2rexbidv crn cab rnmpo eqtri elab2 sylibr elssuni syl - cmpo sseld syl5bir rexlimivv relssi cpw wf wral syl6sseqr xpss12 syl2an + cmpo sseld syl5bir rexlimivv relssi cpw wf wral sseqtrrdi xpss12 syl2an sylbi elpw rgen2 fmpo mpbi frn ax-mp eqsstri sspwuni eqssi ) FGNZCUBZKU AWKWLFGUCKOZUAOZUDZWKPZWMLOZPZWNMOZPZQZMERLDRZWOWLPZWMFPZWNGPZQWRLDRZWT MERZQWPXBXDXFXEXGXDWMDUBZPXFFXHWMIUELWMDUFUGXEWNEUBZPXGGXIWNJUEMWNEUFUG @@ -291721,7 +291721,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually inss1 simpr adantlr cdm cnvimass eqid dmmptss sstri sseqtri rgenw sylancl r19.2z iinss wi wn elssuni syl5ibrcom sylibr eqtrd eqssd eleq1 pm2.61dane adantr sylanbrc cint a1i ctb ciun eqeltrd ad3antrrr nfcv syl2anc eqeltrid - syl5eq cxp snssd sspwuni unssd sseqtrd syl6sseqr ssralv ax-mp sseq2d ssid + syl5eq cxp snssd sspwuni unssd sseqtrd sseqtrrdi ssralv ax-mp sseq2d ssid sseqin2 iffalse iftrue pm2.61d2 ralrimivw ssiin equcoms sseq1d mpan2 3syl rspcev ralimiaa eldifn ad2antlr inss2 mtod iinconst eqtr2d eqeq1 ralimdva mpan9 inundif raleqi ralunb bitr3i ixpiin 3eqtr4rd ixpexg fvex uniex mprg @@ -292307,7 +292307,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually ptpjopn $p |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) e. ( F ` I ) ) $= ( vy vz vs vw vn wcel wa cv cfv wceq vg vk ctop wf w3a cmpt cima crn cres - df-ima wss cuni elssuni syl6sseqr adantl resmptd syl5eq wel wrex wral wfn + df-ima wss cuni elssuni sseqtrrdi adantl resmptd syl5eq wel wrex wral wfn rneqd cdif cfn cixp wex cab ctg cpt ffn eqid sylan2 3adant3 eleq2d biimpa ptval tg2 sylan wi vex weq eqeq1 anbi2d exbidv elab fveq2 eleq12d simplr2 simpl3 ad3antrrr rspcdva simprbi ad2antrl cif simplrr simplrl eleqtrrd wn @@ -293096,7 +293096,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually txindis $p |- ( { (/) , A } tX { (/) , B } ) = { (/) , ( A X. B ) } $= ( vx vy vz vw c0 cpr cid cfv cxp cv wcel wceq wo wn wss wa ctop wne co wi ctx wex neq0 wrex wral wb indistop eltx mp2an sylbi cuni elssuni indisuni - rsp txunii syl6sseqr ad2antrr ne0i ad2antrl sylibr simpld neneqd indislem + rsp txunii sseqtrrdi ad2antrr ne0i ad2antrl sylibr simpld neneqd indislem xpnz simpll syl6eleqr elpri syl ord simprd simplr xpeq12d simprr eqsstrrd mpd adantll eqssd ex rexlimdvva syld exlimdv syl5bi orrd vex ssriv ctopon elpr toptopon txtopon topgele ax-mp simpli eqssi txindislem preq2i 3eqtri @@ -293339,7 +293339,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually wb csn snidg syl opelxpi syl2anr sseldd rspcdva opelxp anbi1i anass bitri id rexbii r19.42v sylib ralrimiva eleq2 xpeq2 sseq1d anbi12d cmpcovf cint crn c0 rint0 adantl topopn ad3antrrr eqeltrd wne simprrl simpr wfo simplr - frnd elin2d wfn ffnd dffn4 fofi w3a fiinopn imp elssuni syl6sseqr sseqin2 + frnd elin2d wfn ffnd dffn4 fofi w3a fiinopn imp elssuni sseqtrrdi sseqin2 syl13anc pm2.61dane ad2antrr ciin simprrr simpl ralimi eliin mpbird elind fniinfv eleqtrd ciun simprl uniiun syl6eq xpeq1d xpiundir wi inss2 iinss2 eqsstrrd sstrid xpss2 sstr2 3syl ralimdva sylc sylibr eqsstrd rspcev expr @@ -293493,7 +293493,7 @@ arbitrary neighborhoods (such as "locally compact", which is actually cxp txuni eqid iscld2 syl2anc eltx cop eqcomd eleq2d anbi1d syl5bb imbi1d eldif impexp syl6bb ralbidv2 eleq1 notbid 2rexbidv imbi12d ralxp opelresi wn vex wbr df-br ideq bitr3i ibar adantr adantl necon3bbid elssuni xpss12 - syl5rbbr syl2an xpeq12i syl6sseqr ad2antrr sseqtrd reldisj syl cvv df-res + syl5rbbr syl2an xpeq12i sseqtrrdi ad2antrr sseqtrd reldisj syl cvv df-res ineq2i inass inss1 sstrid ssv xpss2 ax-mp syl6ss df-ss syl5eqr syl5eq wal sylib eqeq1d opelxp elin 3bitr4i notbii albii intirr bitr3d anbi2d anbi1i eq0 df-3an 3bitr4g 2rexbidva 2ralbidva bitrd 3bitrrd pm5.32i bitri ) AUAI @@ -294800,7 +294800,7 @@ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) $= ccn wf ccnv cima ccmp cuni cpw crab cmpo crn wral cop cmpt simplr cnmptid crest simpll simpr cnmptc cnmpt1t fmptd wrex xkobval abeq2i csn cxp sylan eqid wb imaeq1 sseq1d elrab3 wfun funmpt simplrl elpwid toponuni sseqtrrd - cdm simprd adantr dmmptg opex a1i mprg syl6sseqr funimass4 sylancr sselda + cdm simprd adantr dmmptg opex a1i mprg sseqtrrdi funimass4 sylancr sselda wel opeq1 fvmpt eleq1d vex opeq2 ralsn syl6bbr ralbidva dfss3 eleq1 ralxp weq bitri 3bitrd rabbidva sneq xpeq2d elrab ctop ad2antrr topontop adantl cin txtop syl2anc ad3antrrr toponmax xpexg simprr elrestr txrest syl22anc @@ -295227,7 +295227,7 @@ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) $= f1ofun f1ofo forn syl5eqr sseqtrrd funimass4 simprl elin1d elqtop2 sylan2 dfss3 ad3antrrr mpbid simprd elin2d elpwid imass2 elpwd elind wfn simp-4r wrex f1ofn sstrd simprr fnfvima syl3anc eleq2 rspcev rexlimdvaa funimass2 - ad2antrr wf1 f1of1 elssuni syl6sseqr f1imacnv eqeltrd mpbir2and vex elpw2 + ad2antrr wf1 f1of1 elssuni sseqtrrdi f1imacnv eqeltrd mpbir2and vex elpw2 sylibr sselda adantr f1ocnvfv2 adantl impbid eluni2 3bitr4g syl5bb bitr4d eqeltrrd ralbidva eltg cvv ovex 3bitr4d pm5.32da ctopon tgtopon syl6eleqr mp1i fveq2i elqtop3 unitg ax-mp simpl velpw syl6bi ssrdv sspwuni eqsstrid @@ -297943,7 +297943,7 @@ also T_1 (because they are homeomorphic). (Contributed by Mario Carneiro, ( vx vy cfil cfv wcel cuni c0 cun cin wss wral wa wn wo elun syl wceq cvv csn cconn id filunibas fveq2d eleqtrrd ctop ccld cpr cv wi wal wex simpll nss ssel2 adantll sylib orcomd ord impr uniss ad2antlr uniun unisn uneq2i - 0ex un0 3eqtrri syl6sseqr elssuni ad2antrl filss syl13anc elun1 ex syl5bi + 0ex un0 3eqtrri sseqtrrdi elssuni ad2antrl filss syl13anc elun1 ex syl5bi exlimdv uni0b ssun2 sselii eleq1 mpbiri sylbir pm2.61d2 alrimiv w3a filin snid 3expa ralrimiva elsni ineq2 syl6eq syl6eqel rgen ralun sylancl ineq1 in0 0in ralrimivw wb p0ex unexg mpan2 istopg mpbir2and cdif cfbas filfbas @@ -299018,7 +299018,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the elfm2 $p |- ( ( X e. C /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( X FilMap F ) ` B ) <-> ( A C_ X /\ E. x e. L ( F " x ) C_ A ) ) ) $= - ( vy wcel cfbas cfv co wss cv cima wrex wa wi w3a cfm elfm ssfg syl6sseqr + ( vy wcel cfbas cfv co wss cv cima wrex wa wi w3a cfm elfm ssfg sseqtrrdi wf cfg sselda adantrr 3ad2antl2 simprr imaeq2 sseq1d rspcev rexlimdvaa wb weq syl2anc eleq2i elfg syl5bb 3ad2ant2 sstr2 com12 ad2antll syl5 reximdv imass2 expr com23 expimpd sylbid rexlimdv impbid anbi2d bitrd ) GDKZCHLMK @@ -299731,7 +299731,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the simp3 expr syl21anc imp elsni ineq2d neeq1d syl5ibrcom ralrimiv ralrimiva clsss3 sseldd eleqtrrd 3ad2ant3 neifil syl3anc filfbas ne0i cls0 neeqtrrd simp1 fveq2 necon3i snfbas fbunfip mpbird fsubbas mpbir3and fgcl eqeltrid - fvex snex unex ssfii ax-mp syl6sseqr sstrid snssg mpbiri unssad mpbir2and + fvex snex unex ssfii ax-mp sseqtrrdi sstrid snssg mpbiri unssad mpbir2and ssfg elflim 3jca ) DEUAIJZBEKZABDUBIZIZJZLZCEUCIZJZBCJADCUDUQJZYJCEAUEZDU FIZIZBUEZUGZUHIZUIUQZYKFYJYSEUJIZJZYTYKJYJUUBYREUKZKZYRMNZMYSJURZYJYPYQUU CYJYPDULZUKZUUCYJDUMJZYPUUHKYEYFUUIYIEDUNOZYNDUUGUUGUOZUPPYJEUUGYEYFEUUGV @@ -299957,7 +299957,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the A. o e. J ( A e. o -> E. s e. B ( F " s ) C_ o ) ) ) ) $= ( vt cfv wcel co cv cima wss wrex wi wa ctopon cfbas wf cflf wral cfil wb w3a cfg fgcl eqeltrid isflf syl3an2 eleq2i elfg sstr2 imass2 syl11 adantl - 3ad2ant2 reximdv ex com23 adantld sylbid adantr syl5bi rexlimdv syl6sseqr + 3ad2ant2 reximdv ex com23 adantld sylbid adantr syl5bi rexlimdv sseqtrrdi ssfg sselda 3ad2antl2 ad2ant2r simprr weq imaeq2 sseq1d rspcev rexlimdvaa syl2anc impbid imbi2d ralbidv pm5.32da bitrd ) EGUALMZBHUBLMZHGDUCZUHZADE FUDNLMZAGMZACOZMZDKOZPZWLQZKFRZSZCEUEZTZWKWMDIOZPZWLQZIBRZSZCEUEZTWGWFFHU @@ -300421,7 +300421,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. B ( o i^i s ) =/= (/) ) ) ) ) $= ( vt cfv wcel wa co cv c0 wral wi wb wss syl cfbas cfcls cin wne cfil cfg - ctopon fgcl adantl eqeltrid fclsopn syldan ssfg ad3antlr syl6sseqr ssralv + ctopon fgcl adantl eqeltrid fclsopn syldan ssfg ad3antlr sseqtrrdi ssralv weq ineq2 neeq1d cbvralv syl6ib wrex eleq2i syl5bb simplbda r19.29r sslin elfg ssn0 sylan rexlimivw ex ralrimdva anassrs pm5.74da ralbidva pm5.32da impbid bitrd ) EFUGJKZBFUAJKZLZAEDUBMKZAFKZACNZKZWEINZUCZOUDZIDPZQZCEPZLZ @@ -300583,7 +300583,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the cdif crab cun cfi cfg simplrl topopn pwexg 3syl unexg ssfii cfbas filsspw rabexg ssrab2 a1i unssd ssun2 difss wb elpw2g mpbiri elrabd elrab simprbi ne0d ad2antll sslin simprrr adantr inssdif0 simplll simprl filelss sseq1d - df-ss cuni elssuni syl6sseqr ad2antrl filss syl13anc syl5bir necon3bd mpd + df-ss cuni elssuni sseqtrrdi ad2antrl filss syl13anc syl5bir necon3bd mpd sylbid ralrimivva filfbas filtop eleq1 syl5ibrcom pssdifn0 supfil fbunfip ssn0 mpbird w3a fsubbas mpbir3and ssfg com23 unssad fgcl simprrl fclsopni sstrd mpid syld necon2bd anassrs expr con4d ralrimdva simprr jctild simpl @@ -301262,7 +301262,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the ax-mp elfpw wf sseq1 rexbidv simprbi syl6 ralrimiv ac6sfi syl5 adantl crn elrab simprll frn syl cdom wbr simplr wfo wfn dffn4 sylib adantr ad2antrl ffn fodomfi syl2anc jca elin vex anbi1i bitr2i simprr ciun uniiun simprlr - domfi ss2iun eqsstrid fniunfv sseqtrd eqsstrd sstrd uniss syl6sseqr eqssd + domfi ss2iun eqsstrid fniunfv sseqtrd eqsstrd sstrd uniss sseqtrrdi eqssd 3syl simpll2 exp32 rexlimdv 3exp com34 syl7bi ralrimdv fibas eleq1 mpbiri ctb tgcl jctild iscmp syl6ibr imp exlimiv impbii ) BUBLZBAMZUCUDZUEUDZNZC DMZOZNZCEMZOZNZEUVMUGZPUHZQZRZDUVIUGUIZSZAUJABCDEFUKUWDUVHAUVLUWCUVHUVLUW @@ -302276,7 +302276,7 @@ given an amorphous set (a.k.a. a Ia-finite I-infinite set) ` X ` , the eqeltrid mpancom oveq1d eqtrd oveq12d eleqtrd crn cplusf wfn coex plusfeq vex fnmpoi ax-mp eqcomi grpplusf frn cnrest2 mpbid oveq2d istmd syl3anbrc 3syl ccnv wral biimpa f1ocnv cima wi adantr weq fvex ad2antlr crab simplr - fvconst2g fveq1 eqeq1d ralrimiva syl6sseqr mpbir2and feqmptd id ffvelrnda + fvconst2g fveq1 eqeq1d ralrimiva sseqtrrdi mpbir2and feqmptd id ffvelrnda fconst6g ccnp an32s fmpttd wrex cnveq fveq1d fvmpt cvv mptiniseg elv cuni eleq1d toponuni mpteq1 simpll ffvelrnd ptpjcn eqeltrd cnmpt1res eqeltrrid snelpwi cnima simpllr f1ocnvfv2 elrabd ssrab2 a1i ad3antrrr simplrr eleq1 @@ -304613,7 +304613,7 @@ unit group (that is, the nonzero numbers) to the field. (Contributed ustssco $p |- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( V o. V ) ) $= ( cust cfv wcel wa cid cres cun ccom ssun1 coires1 wrel cdm wss wceq ustrel cxp ustssxp dmss syl dmxpid syl6sseq syl2anc syl5eq uneq1d sseqtrrid coundi - relssres syl6sseqr ustdiag ssequn1 sylib coeq2d sseqtrd ) ACDEFBAFGZBBHCIZB + relssres sseqtrrdi ustdiag ssequn1 sylib coeq2d sseqtrd ) ACDEFBAFGZBBHCIZB JZKZBBKZUQBBURKZVAJZUTUQBVAJBVCBVALUQVBBVAUQVBBCIZBBCMUQBNBOZCPVDBQABCRUQVE CCSZOZCUQBVFPVEVGPABCTBVFUAUBCUCUDBCUJUEUFUGUHBURBUIUKUQUSBBUQURBPUSBQABCUL URBUMUNUOUP $. @@ -305694,7 +305694,7 @@ unit group (that is, the nonzero numbers) to the field. (Contributed /\ A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) ) $= ( wi wa vu vv cucn co wcel wf cv wbr cfv wral wrex cust isucn syl2anc weq - wb breq imbi2d ralbidv rexralbidv simplr wss cxp cfg cfbas ssfg syl6sseqr + wb breq imbi2d ralbidv rexralbidv simplr wss cxp cfg cfbas ssfg sseqtrrdi syl adantr sselda rspcdva simpr syl6eleq elfg simplbda syldan ssbr imim1d adantl ralrimivw ralim ralimi ex reximdva mpd r19.37v rexlimdva ad3antrrr 3syl ralrimiva ssrexv imbi1d 2ralbidv cbvrexv ralimdv nfv nfra1 nfan rspa @@ -305745,7 +305745,7 @@ unit group (that is, the nonzero numbers) to the field. (Contributed syl6bbr c1st c2nd cvv opex ucnimalem fvmpt2 sylancl 1st2nd2 eqtr3d simpld syl vex fveq2d opeq12d eqtr4d imbi12d exbiri reximdv mpd r19.29d2r pm3.35 opth rexlimivw imp syl1111anc ralrimiva ex reximdva wfun cdm mpofun dmmpo - syl6sseqr funimass4 sylancr biimprd r19.29r reximi ) AUAUCZFQZHRZUAKUCZUD + sseqtrrdi funimass4 sylancr biimprd r19.29r reximi ) AUAUCZFQZHRZUAKUCZUD ZXTFXSUEHUFZUGZSZKDTZYAKDTAXTKDTZYBKDUDYDABUCZCUCZXSUHZYFEQZYGEQZHUHZUGZC IUDZBIUDZKDTZYEAYHYIYJUBUCZUHZUGZCIUDZBIUDKDTZYOUBGHYPHUIZYSYMKBDIUUAYRYL CIUUAYQYKYHYIYJYPHUJUKULUMAIJEUNZYTUBGUDZAEDGUOUPRZUUBUUCSZNADIUQQRZGJUQQ @@ -305770,7 +305770,7 @@ unit group (that is, the nonzero numbers) to the field. (Contributed 19-Nov-2017.) $) ucnprima $p |- ( ph -> ( `' G " W ) e. U ) $= ( vr cv wss wcel cfv ccnv cima wrex ucnima wa wfun cdm wb cop mpofun cust - cxp ustssxp sylan dmmpo syl6sseqr funimass3 sylancr rexbidva mpbid adantr + cxp ustssxp sylan dmmpo sseqtrrdi funimass3 sylancr rexbidva mpbid adantr opex wi simpr cnvimass sseqtri a1i ustssel syl3anc rexlimdva mpd ) APQZFU AHUBZRZPDUCZVMDSZAFVLUBHRZPDUCVOABCDEFGHIJPKLMNOUDAVQVNPDAVLDSZUEZFUFVLFU GZRVQVNUHBCIIBQETZCQETZUIZFOUJVSVLIIULZVTADIUKTSZVRVLWDRKDVLIUMUNBCIIWCFO @@ -309091,7 +309091,7 @@ S C_ ( P ( ball ` D ) T ) ) $= ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ S ) $= ( cxmet cfv wcel cxr w3a ccld co wss wbr wa syl2anc cbl ccl blcld cv crab cle wral blssm elbl wi xmetcl 3expa 3adantl3 simpl3 xrltle expimpd sylbid - clt ralrimiv ssrab sylanbrc syl6sseqr cuni eqid clsss2 ) BGJKLZCGLZDMLZNZ + clt ralrimiv ssrab sylanbrc sseqtrrdi cuni eqid clsss2 ) BGJKLZCGLZDMLZNZ EFOKLCDBUAKPZEQVJFUBKKEQABCDEFGHIUCVIVJCAUDZBPZDUFRZAGUEZEVIVJGQVMAVJUGVJ VNQBCDGUHVIVMAVJVIVKVJLVKGLZVLDURRZSVMVKBCDGUIVIVOVPVMVIVOSVLMLZVHVPVMUJV FVGVOVQVHVFVGVOVQCVKBGUKULUMVFVGVHVOUNVLDUOTUPUQUSVMAGVJUTVAIVBEVJFFVCZVR @@ -309643,7 +309643,7 @@ S C_ ( P ( ball ` D ) T ) ) $= w3a wa wex wi wne co cxr cxmet wb syl adantr simprl syl3anc cds cbs cxp cixp cres cmpt 3ad2ant1 ovex eqid ffvelrnda cprds feqmptd oveq2d syl5eq ralrimiva fveq2d eleqtrd blopn 2fveq3 syl6eqr fveq2 sylan eqtrd anbi12d - fveq1 eleq1d ixpeq2dva syl121anc sylbid syl6eq raleqdv rspcev syl6sseqr + fveq1 eleq1d ixpeq2dva syl121anc sylbid syl6eq raleqdv rspcev sseqtrrdi weq syl5bi cfi ccnv cima xmstps eqeltrd ctopon eqeltrrd ad2antrr cnveqd ctop ctps crp ccom cpt ffnd dffn2 fnfco cab wal eldifsn prdsxmslem1 cc0 ptval blrn clt simprr xbln0 mptexd rgenw fnmpt xmsxmet simp2l prdsbascl @@ -311023,7 +311023,7 @@ function based on the norm (the distance ` D ` between two elements is the norm ( wcel wss w3a wceq wa cres cr wf cvv cngp cgrp cms isngp resss eqsstri ccom cxp sseq1 mpbiri cdm cmet cfv cds reseq1i eqtri msmet nmf2 grpsubf sylan2 ad2antrr fco syl2an2r fdmd reseq2d wfun msf ad2antlr ffund simpr - cin ssv fss sylancl fssxp syl df-res syl6sseqr funssres syl2anc wfn ffn + cin ssv fss sylancl fssxp syl df-res sseqtrrdi funssres syl2anc wfn ffn ssind fnresdm 3syl 3eqtr3d ex impbid2 pm5.32i df-3an 3bitr4i bitr4i ) C UALCUBLZCUCLZEDUGZAMZNZWMWNWOBOZNZACDEGHIUDWMWNPZWRPWTWPPZWSWQWTWRWPWTW RWPWRWPBAMBAFFUHZQZAKAXBUEUFWOBAUIUJWTWPWRXABWOUKZQZBXBQZWOBXAXDXBBXAXB @@ -313698,7 +313698,7 @@ Normed space homomorphisms (bounded linear operators) tgioo $p |- ( topGen ` ran (,) ) = J $= ( vz cioo cr wcel wceq wss cv co wrex wa c1 cxr syl cle wbr cmnf vv cbl vx vy va vb cfv crn ctg cxmet rexmet mopnval ax-mp blssioo wral elssuni - crp cuni unirnioo syl6sseqr cin ctb retopbas a1i simpl sselda caddc 1re + crp cuni unirnioo sseqtrrdi cin ctb retopbas a1i simpl sselda caddc 1re cmin bl2ioo mpan2 cxp wfn cpw ioof ffn peano2rem rexrd peano2re mp3an2i wf fnovrn eqeltrd simpr 1rp blcntr mp3an13 elind basis2 syl22anc ovelrn wb wi eleq2 sseq1 anbi12d inss2 sstr adantl elioore adantr sseqtrd dfss @@ -313910,7 +313910,7 @@ Normed space homomorphisms (bounded linear operators) wo rexr elixx3g baib syl3anc pnfge syl biantrud 3bitr2d pm5.32da biancomi ltpnf elin 3anass 3bitr4g elioo2 mpan2 bitr4d eqrdv ioorebas ineq1 eleq1d syl6eqel syl5ibrcom rexlimiv sylbi mnfxr df-ico mnfle biantrurd jaoi cuni - mnflt elssuni unirnioo syl6sseqr df-ss sylib eqeltrd eleq1 eqsstri eqssi + mnflt elssuni unirnioo sseqtrrdi df-ss sylib eqeltrd eleq1 eqsstri eqssi id ) FUEZUFGZHUGGZIUHJZAUUJUULCUUJUULCUIZUUJKZUUMUUKKZUUMILZUUMUULKZUUJUU KUUMUUJUUKUFGZUUKUUKUJKZUUIUUKLZUUJUURLUKMMULZUUKFURZUUTUVBFUVAUMZUUMDUIZ FJUUKKZDMUNCMUNUVAIUOZFURUVCUPUVAUVFFUSUQUVECDMMUUMUVDUTVACDMMUUKFVBVCUVA @@ -314052,7 +314052,7 @@ Normed space homomorphisms (bounded linear operators) Carneiro, 4-Sep-2015.) $) xrsmopn $p |- ( ordTop ` <_ ) C_ J $= ( vx vy vr vz cfv cv wcel cxr wss co crp wa cr mp3an2i wceq c1 cordt wrex - cle cbl wral cuni elssuni letopuni syl6sseqr wel cabs cmin ccom cxp cxmet + cle cbl wral cuni elssuni letopuni sseqtrrdi wel cabs cmin ccom cxp cxmet cres cin crest eqid rexmet ctop cvv reex elrestr mp3an12 ad2antrr biimpri letop elin adantll cioo crn ctg cmopn xrtgioo tgioo eqtr3i mopni2 xrsxmet simplr ressxr sseqin2 mpbi syl6eleqr adantl xrsdsre eqcomi xrsblre sylan2 @@ -314546,7 +314546,7 @@ Normed space homomorphisms (bounded linear operators) opnreen $p |- ( ( A e. ( topGen ` ran (,) ) /\ A =/= (/) ) -> A ~~ ~P NN ) $= ( vx vy cioo cfv wcel cdom wbr cen cr cvv wss ssdomg wa cmin co crp caddc - clt sylan2 crn ctg cn cpw wne reex cuni elssuni uniretop syl6sseqr rpnnen + clt sylan2 crn ctg cn cpw wne reex cuni elssuni uniretop sseqtrrdi rpnnen c0 mpsyl domentr sylancl cv wex n0 cabs ccom cxp cres sselda c2 cdiv cicc cbl c1 rpnnen2 rphalfcl rpred resubcl readdcl simpl ltsubrp ltaddrp lttrd cc0 iccen syl3anc sylancr ovex rpre rexrd adantl subsub4d 2halvesd oveq2d @@ -316793,7 +316793,7 @@ extended reals extends the topology of the reals (by ~ xrtgioo ), this cim simprl opeq12d cnrecnv opex fvmpt eqtr3d fveq2d fvex syl6eq absrele syl op1st eqbrtrd breq1d simplrr rspcdva letrd absled simpld simprd w3a mpbid renegcl elicc2 syl2anc mpbir3and xp2nd absimle opelxpd eqeltrd ex - op2nd syl5bi ssrdv wfun crn f1ofun ax-mp f1ofo forn syl6sseqr funimass1 + op2nd syl5bi ssrdv wfun crn f1ofun ax-mp f1ofo forn sseqtrrdi funimass1 wi wfo mpd cioo ctg ctx eqid mp3an2i syl6eqr ccn mpancom retop eqeltrrd chmeo cnrehmeo imaexg eqeltri restabs oveq2i ishmeo mpbi simpli iccssre rerest oveq12d ovex txrest mp4an icccmp imacmp eqeltrid imassrn eqsstri @@ -316890,7 +316890,7 @@ extended reals extends the topology of the reals (by ~ xrtgioo ), this ( vu vy vx vz ccmp wcel cv co cfv wral wa cabs wss cc syl3anc wbr cle cr vr vs cnlly ctop crest csn cnei cpw cin wrex cnfldtop cmin ccom cbl cxmet crp cnxmet cnfldtopn mopni2 mp3an1 cdiv ccl a1i cxr cuni elssuni ad2antrr - vw c2 cnfldtopon toponunii syl6sseqr simplr rphalfcl ad2antrl rpxrd blopn + vw c2 cnfldtopon toponunii sseqtrrdi simplr rphalfcl ad2antrl rpxrd blopn sseldd blcntr opnneip blssm syl2anc rpxr rphalflt blsscls syl23anc simprr sscls clt sstrd ssnei2 syl22anc vex elpw2 sylibr elind ccld clscld abscld caddc rpred readdcld crab eqid blcls wi simpr adantr abs2difd subcld letr @@ -321720,7 +321720,7 @@ vector spaces which are also normed vector spaces (that is, normed groups syl6bb imp tcphcphlem1 oveqan12d 3brtr4d tngngpd cnnrg simp3d tcphcphlem2 subrgnrg eqeltrd lmodvscl csubg subrgsubg cnfldnm subgnm2 oveq12d 3eqtr4d fveq1d eqtrd tcphbas tcphvsca tcphsca isnlm sylanbrc elrege0 anbi2i bitri - ralrimivva ralrimiv wfun ffun ax-mp inss1 sstrid fdmi syl6sseqr funimass4 + ralrimivva ralrimiv wfun ffun ax-mp inss1 sstrid fdmi sseqtrrdi funimass4 cdm mpbird cnex tngnm syl2anc eqcomd tcphip iscph syl3anbrc ) ADUCQZDUDQZ CUECUFRZUGUHZSZUIUJUWPUKULUMUHZUNZUOUWPUPZDVGRZUAGUAVHZUXCEUHZUJRZUQZSDUR QAUWNUWOUWRAHUCQZUWNLDHIUSUTZADVAQZDVBQZCVCQZUIUXCUBVHZHVDRZUHZUXBRZUXCCV @@ -325189,7 +325189,7 @@ need not be complete (for instance if the given set is infinite ( vx wcel cfv co c2 cexp cc0 crab wa wceq cc cr w3a cv cmin wne cun csupp cmpt wo wn simprl 0cn syl6eqel simprr eqtr4d subeq0bd sq0id ex wb anbi12i ioran nne bitri a1i eqidd fveq2d oveq12d oveq1d ovex fvmptd neeq1d bicomd - simpr necon1bbid 3imtr4d con4d ss2rabdv unrab syl6sseqr simp1 eqid fnmpti + simpr necon1bbid 3imtr4d con4d ss2rabdv unrab sseqtrrdi simp1 eqid fnmpti cvv wfn suppvalfn mp3an13 syl cmap wf cfsupp wbr elrabi eleq2s elmapi ffn 3syl 3ad2ant2 syl3anc 3ad2ant3 uneq12d 3sstr4d ) EFJZCGJZDGJZUAZIUBZBEBUB ZCKZXFDKZUCLZMNLZUGZKZOUDZIEPZXECKZOUDZIEPZXEDKZOUDZIEPZUEZXKOUFLZCOUFLZD @@ -330041,7 +330041,7 @@ Hilbert space (in the algebraic sense, meaning that all algebraically c2nd 1st2nd2 df-ov ioombl syl6eqel adantlr finiunmbl eqsstrid ioossre inmbl syl6eqss ovolfcl ovolioo simp2d resubcld mblsplit 3sstr4i sslin w3a simp1d sseqin2 indifdir difeq12i eqcomd wb ineq1d 2fveq3 cbvdisjv - mp1i fz1ssnn uzss syl6sseqr uzdisj syl5reqr disjiun uneqdifeq syl5eqr + mp1i fz1ssnn uzss sseqtrrdi uzdisj syl5reqr disjiun uneqdifeq syl5eqr syl13anc oveq12d absdifltd ltled mblvol rgenw disjss2 mpsyl volfiniun cabs disjss1 sumeq2dv 3eqtr3d breqtrrd eqbrtrrd leadd2d mpbird fsumle lesubaddd chash recnd fsumconst hashfz1 oveq1d nnne0d divcan2d 3eqtrd @@ -330471,7 +330471,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by wral wne simprl ssid fveq2 sseq2d rspcev sylancl sylibr dyadmax syl2anc rabn0 elrab simprlr simplrr sseldd simprll imbi1i impexp bitri ad2antll sstr2 imim1d syl5bir imim2d syl5bi ralimdv2 impr sseq1d equequ1 imbi12d - ancrd ralbidv elrab2 sylanbrc wfun ffun ssrab3 fdmi syl6sseqr funfvima2 + ancrd ralbidv elrab2 sylanbrc wfun ffun ssrab3 fdmi sseqtrrdi funfvima2 cdm ad2antrr elunii exp32 rexlimdv rexlimdvaa sylbid ssrdv imass2 uniss mpd mp1i eqssd ) ANFUBZUCZNHUBZUCZALYLYNLOZYLPYOUAOZPZUAYKUDZAYOYNPZUAY OYKUEAYRYOUIOZNUFZPZUIFUDZYSANUGUGUHZUJZFUUDQYRUUCUKUUDUGULZNUMZUUEUNUU @@ -330549,7 +330549,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by elrab sylan2b ralrimiva wfun wb cxr cxp wf iccf ffun ax-mp ssrab2 cle cin cz cn0 dyadf inss2 rexpssxrxp sstri fdmi sseqtrri funimass4 mp2an sspwuni frn sylib cabs cmin ccom cres cbl crp wrex cxmet eqid rexmet cmopn mopni2 - tgioo mp3an1 wceq elssuni uniretop syl6sseqr sselda rpre bl2ioo syl2an c1 + tgioo mp3an1 wceq elssuni uniretop sseqtrrdi sselda rpre bl2ioo syl2an c1 caddc c2 cexp cdiv cn 2re 1lt2 expnlbnd mp3an23 ad2antrl cfl ad2antrr 2nn nnnn0 nnexpcl sylancr nnred remulcld fllelt syl syl112anc mpbird nndivred cmul syl2anc rexrd readdcld recnd ltadd2dd eqbrtrd wi simpld cc0 peano2re @@ -331843,7 +331843,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by cvol cdm wex ctg cfv cioo crn ctx ccn chmeo cnrehmeo hmeocn ax-mp cnima co eqid cq cxp fveq2i tgqioo oveq12i ctb qtopbas eqeltri txbasval txval mpan 3eqtri syl6eleq wb txbas eltg3 sylib adantl ciun cr wfo wf1o f1ofo - cnref1o elssuni cnfldtopon toponunii syl6sseqr ad2antlr foimacnv simprr + cnref1o elssuni cnfldtopon toponunii sseqtrrdi ad2antlr foimacnv simprr sylancr imaeq2d syl6eq com cen omelon nnenom isnumi qnnen xpnnen cxr wf wral ioof fodomnum mp2 eqbrtri domentr wfn vex wrex eleq2i cre ccom cim domtr adantr fvco3 sylan eleq1d anbi12d cop fveq2 syl elpreima fco 3syl @@ -332217,7 +332217,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by mpbird ralbidv rspcev syl2anc infxrre sseli syl2an adantll syl12anc simpr cres eqid adantlr limsupgle syl211anc adantl ralbidva ralrimiva mpteq2dva 3syl wi syl5eq simpll an32s df-ima feqmptd reseq1d resmpt ffvelrn simplll - uztrn2 simpllr dmmptd syl6eleq eluzelz ne0i dm0rn0 sylib syl6sseqr sseldi + uztrn2 simpllr dmmptd syl6eleq eluzelz ne0i dm0rn0 sylib sseqtrrdi sseldi uzss sylc fveq1d fvres eqtr3d breq1d eluzle biimt bitrd ralrn brralrspcev resmptd suprcld eluz biimprd impr fnfvelrn eqeltrrd suprubd expr suprleub syldan syl31anc xrletrid infeq1d 3eqtrd ad2ant2lr simprr ralrnmpt rexbidv @@ -332716,7 +332716,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by vw cof co cvv readdcl adantl citg1 cdm wf i1ff reex a1i inidm off crn cxp cmpo cfn wfo i1frn xpfi syl2anc wfn eqid ovex fnmpoi dffn4 mpbi fofi wrex sylancl cab mp3an3 eqeq1 2rexbidv elab sylibr ffnd dffn3 sylib frnd rnmpo - rspceov syl6sseqr ssfid csn cdif ccnv cima cmin cin ssdifssd sselda recnd + rspceov sseqtrrdi ssfid csn cdif ccnv cima cmin cin ssdifssd sselda recnd ciun cc i1faddlem syldan wral adantr cmbf i1fmbf eldifi ad2antlr resubcld sseldd mbfimasn syl3anc inmbl ralrimiva finiunmbl eqeltrd wss csu cle wbr mblvol mblss inss1 adantrr simprr oveq2d subid1d imaeq2d fveq2d i1fima2sn @@ -332757,7 +332757,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ( vu vv vz cmul cr cvv cv wcel wa syl cfn wceq wss cfv covol vy vx vw cof co remulcl adantl citg1 cdm wf i1ff reex a1i inidm off crn cmpo cxp i1frn wfo xpfi syl2anc wfn eqid ovex fnmpoi dffn4 mpbi fofi sylancl cab rspceov - wrex mp3an3 eqeq1 elab sylibr ffnd dffn3 sylib frnd rnmpo syl6sseqr ssfid + wrex mp3an3 eqeq1 elab sylibr ffnd dffn3 sylib frnd rnmpo sseqtrrdi ssfid 2rexbidv cc0 csn cdif ccnv cima cdiv ciun cvol cc ax-resscn syl6ss ssdifd cin sselda i1fmullem syldan wral difss ssfi i1fima inmbl ralrimivw adantr finiunmbl eqeltrd mblvol csu cle wbr mblss inss2 ad2antrr i1fima2sn sylan @@ -332827,7 +332827,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by cv cmul csu ccnv cima cvol cdm cfn wss i1fadd cxp wfo i1frn syl syl2anc xpfi wfn cres cc wf ax-addf ffn ax-mp i1ff frnd ax-resscn syl6ss xpss12 fnssres sylancr fneq1i sylibr dffn4 sylib fofi difss sylancl cvv cop wi - ssfi syl6sseqr funfvima2 df-ov 3eltr4g ffnd dffn3 ssdifd wral sselda wb + ssfi sseqtrrdi funfvima2 df-ov 3eltr4g ffnd dffn3 ssdifd wral sselda wb a1i cin adantr inss2 i1fima ad2antrr sstrid adantlr resubcld wne npcand wn recnd oveq12 00id syl6eq itg1addlem3 syl21anc fovrnd syldan sumeq2dv fveq2d 3eqtr4d oveq2d eqtrd anasss fsumcom oveq12d ex readdcld remulcld @@ -332998,7 +332998,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by cof cdm reex a1i i1ff 0red cv simplr oveq1d mul02lem2 adantl caofid2 i1f0 eqtrd syl6eqel wne remulcl fconst6g inidm off crn cfn cmpt wfo i1frn ovex wfn eqid fnmpti dffn4 mpbi fofi sylancl wrex elsni oveq2 rspceeqv syl2anr - cab id eqeq1 rexbidv elab sylibr fconstg ffnd dffn3 sylib rnmpt syl6sseqr + cab id eqeq1 rexbidv elab sylibr fconstg ffnd dffn3 sylib rnmpt sseqtrrdi frnd ssfid cdif ccnv cima cdiv cvol wss ssdifssd sselda i1fmulclem syldan i1fima ad2antrr eqeltrd fveq2d redivcld eldifsni divne0d eldifsn sylanbrc cfv recnd i1fima2sn syl2anc i1fd pm2.61dane ) AIBJZUBZCKUDLZUCUEZMBNABNOZ @@ -337906,7 +337906,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ciin limccl limcresi rgenw ssiin mpbir ssini a1i elriin ciun ccnfld ctopn csn cdif cfv wrex wi simprl wf cfn wex ad2antrr csb simplrr nfcsb1v nfres nfov nfcri wceq csbeq1a reseq2d oveq1d eleq2d rspc mpan9 wb ssiun2 cbviun - syl6sseqr adantl fssresd simpr nfss sseq1d sylc eqid ellimc2 mpbid simprd + sseqtrrdi adantl fssresd simpr nfss sseq1d sylc eqid ellimc2 mpbid simprd adantlr simplrl rsp syl3c ralrimiva nfdif nfin nfima nfrex difeq1d ineq2d nfv nfan imaeq12d anbi2d rexbidv cbvral sylibr eleq2 ineq1 imaeq2d ac6sfi anbi12d syl2anc crn cint cnfldtop frn ad2antrl wfo adantr wfn dffn4 sylib @@ -340679,7 +340679,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by wf sstrd sseqtrd dvres eqeltrrd dmeqd cin dmres oveq1d df-ss sylib fveq1d eleq2d syl2an3an caddc ioossicc simprll resubcld readdcld simprlr oveq12d simplr elicc2 simp1d eleqtrrd simp2d simp3d absdifled mpbir2and xrlelttrd - cicc elbl3 mpbird ssrdv syl6sseqr resabs1d dvbss fssresd eqsstrid crn ctg + cicc elbl3 mpbird ssrdv sseqtrrdi resabs1d dvbss fssresd eqsstrid crn ctg blssm cnt ccnfld ctopn tgioo2 ctop retop cmopn tgioo eqeltrd isopn3i dvcn blopn syl31anc rescncf sylc oveq2d iccntr 3eqtr3d sseqtrrd fvres sylan9eq sstrid reseq1d eqtr4d sselda syl2an2r dvlip mp2and exp32 sylbid rexlimdva @@ -340925,7 +340925,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) $= ( cv cr cfv cmin co cabs wral wcel cres cmul cle wbr cicc wrex crn df-ima - cima eqsstrrid cdm cin iccssre syl2anc ssind dmres syl6sseqr c1lip2 wa wi + cima eqsstrrid cdm cin iccssre syl2anc ssind dmres sseqtrrdi c1lip2 wa wi wss sseld anim12d imp fvres oveqan12rd fveq2d breq1d biimpd syl ralimdvva reximdv mpd ) ACMZGNUAZOZBMZVOOZPQZROZFMVNVQPQROUBQZUCUDZCDEUEQZSBWCSZFNU FVNGOZVQGOZPQZROZWAUCUDZCWCSBWCSZFNUFABCDEFVOHIJAVOUGGNUINGNUHKUJAWCNGUKZ @@ -341777,7 +341777,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by lhop $p |- ( ph -> C e. ( ( z e. D |-> ( ( F ` z ) / ( G ` z ) ) ) limCC B ) ) $= ( vr cv cmin cr cres cfv co wss crp cdiv cmpt climc wcel cioo crn syl3anc - eqid a1i wa wceq syl6sseqr syl sseldd cdif cin adantr rexrd wf cun uneq1i + eqid a1i wa wceq sseqtrrdi syl sseldd cdif cin adantr rexrd wf cun uneq1i cxr clt wbr syl5eq c0 wb syl2anc wn eqtri sylancl mpbid sseqtrrid cdv cdm cc ax-resscn fss sstrd fssresd ioossre dvres syl22anc ctop retop iooretop cnt isopn3i mp2an reseq2i syl6eq dmeqd ssdmres sylib limcresi sseldi cima @@ -342445,7 +342445,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by sseldi elioopnf simpld reflcl dvmptrecl fzfid cuz syl6eleqr rspccva elfzuz syl2an fsumrecl ccnfld ctopn cicc eqid mulcn simprd iccssioo pnfxr ltpnfd syl22anc cncfmptid sylancl cpr reelprrecn ioossicc crn - ctg simpr dvmptid tgioo2 iooretop cres syl6sseqr resmptd dmeqd dvcn + ctg simpr dvmptid tgioo2 iooretop cres sseqtrrdi resmptd dmeqd dvcn dmmptg syl31anc cncffvrn sylancr eqeltrrid rescncf eqeltrrd 3eqtr3g sylc oveq2i sseli elicc2 syl2anc biimpa simp1d simp2d simp3d simp2r simpl csbie breq1d nfv nfbr nfim anbi1d 3anbi12d chvar vtoclg mpcom @@ -342705,7 +342705,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ( vu vv vw vz cv wcel cle wbr wa cpnf cico cc0 cxr wne clt csup wceq cioo co cr ioossre eqsstri simprl sseldi rexrd renepnfd icopnfsup wss syl6eleq syl2anc wb adantr elioopnf syl mpbid simprd df-ioo df-ico xrltletr ixxss1 - syl2an2r syl6sseqr cmpt crli cbvmptv eqbrtrrid rlimres2 dvmptrecl adantrr + syl2an2r sseqtrrdi cmpt crli cbvmptv eqbrtrrid rlimres2 dvmptrecl adantrr cc recnd rlimconst ralrimiva sselda eleq1d rspccva simpll simplrl simplrr a1i wral elicopnf simplbda syl122anc rlimle ) ABULZGUMZFXMUNUOZUPZUPZIXMU QURVFZEDUSDXQXMUTUMXMUQVAXRUTVBVCUQVDXQXMXQGVGXMGHUQVEVFZVGNHUQVHVIZAXNXO @@ -342787,7 +342787,7 @@ or are almost disjoint (the interiors are disjoint). (Contributed by ( vy vu vv vw vz crli wbr wa cpnf cico co cfv cv cmin cabs csb cxr csup clt wceq wcel wne cr cioo ioossre eqsstri sseldi rexrd renepnfd syl2anc icopnfsup adantr cc wf dvfsumrlimf ad2antrr ffvelrnd recnd wss syl6eleq - wb elioopnf mpbid simprd df-ioo df-ico xrltletr ixxss1 syl6sseqr sselda + wb elioopnf mpbid simprd df-ioo df-ico xrltletr ixxss1 sseqtrrdi sselda syl cle subcld cmpt pnfxr icossre sylancl cdm rlimf adantl cfl cfz ovex csu dmmpti feq2i sylib rlimconst feqmptd simpr eqbrtrrd rlimsub rlimabs rlimres2 wral a1i dvmptrecl ralrimiva nfcsb1v nfel1 csbeq1a eleq1d rspc @@ -351062,7 +351062,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the mpan2 syl5 rexlimdvw wb copab df-ulm oveq2 feq3d raleq rexralbidv ralbidv wceq feq2 3anbi123d rexbidv opabbidv elex cpm cxp wss simpr1 uzssz elpm2r ovex zex mpanl12 sylancl simpr2 simpl elmapg sylancr mpbird jca ssopab2dv - cnex ex df-xp syl6sseqr xpex syl fvmptd3 breqd feq1d simpr fveq1d oveq12d + cnex ex df-xp sseqtrrdi xpex syl fvmptd3 breqd feq1d simpr fveq1d oveq12d ssex fveq2d breq1d eqid brabga sylan9bb pm5.21ndd ) CILZGMLZHMLZNZGHCUBOZ UCZFPZUDOZQCUEUFZGRZCQHRZBPZEPZGOZOZYFHOZUGUFZUIOZAPZUHUCZBCSZEDPUDOZSDYB UJZAUKSZULZFTUJZXTXRUMXOGHXSCUNUOUPXOYSXRFTYSYDYENXOXRYDYEYRUQXOYDXPYEXQY @@ -352495,7 +352495,7 @@ evaluate the derivatives (generally ` RR ` or ` CC ` ), ` F ` is the cr clt abscld absge0d crp simp2d cxr w3a wb 0re simp1d elico2 sylancr rpxrd mpbir3and wf wfn ffn elpreima mp2b sylanbrc wceq eqid cnbl0 syl eleqtrd icossicc imass2 mp1i cpnf iccssxr adantr sseldi simp3d df-ico - eqsstrrd radcnvcl df-icc xrlelttr ixxss2 syl2anc syl6sseqr 3jca ) AMU + eqsstrrd radcnvcl df-icc xrlelttr ixxss2 syl2anc sseqtrrdi 3jca ) AMU EZFTZUFZXMUGKUHUIUJZUKULUMZTXQUHUNZUGKUOUMZUPZUQXTFUQXOXMXRUGKURUMZUP ZXQXOXMUSTZXMUHULZYATZXMYBTZAFUSXMFUSUQAFXRUGEURUMZUPZUSRYHUHUTUSUHYG VAUSVJUHVBVCVDVEVFVGZXOYEYDVJTZUGYDVHVIZYDKVKVIZXOXMYIVLXOXMYIVMXOKVN @@ -356660,7 +356660,7 @@ imaginary part lies in the interval (-pi, pi]. See cioo cnxmet 0cnd rpxr adantr blssm mp3an2i sselda cr imcld efopnlem1 pire cxr abslt sylancl mpbid simpld simprd w3a renegcli rexri elioo2 syl3anbrc wb mp2an wf imf ffn elpreima sylanbrc ssrdv df-ima wfo eqid logf1o2 f1ofo - ex forn syl6sseqr resima2 syl5eq ccncf logcn difss cnfldtopon toponrestid + ex forn sseqtrrdi resima2 syl5eq ccncf logcn difss cnfldtopon toponrestid syl ccn ssid eleqtri cnfldtopn blopn cnima sylancr eqeltrrd ctop cnfldtop cncfcn ccnfld ctopn logdmopn eleqtrri restopn2 sylib ) AUADZAEFGZHZIJAUBU CUDZUEKLZMZBDZUUHNUFJUGLZUHZOZUUEUUHBUUKUILZDZUUIUULHZUUEPUUKQZRZUUGMZUUH @@ -356692,7 +356692,7 @@ imaginary part lies in the interval (-pi, pi]. See a1i eqcom simplr efcl syl mp3an12i wne efne0 divmuld syl5bb caddc pncan2d eqtr4d addcld efadd eqeq2 sylbid impbid wfn ffn sylancr 3bitr4d rabbi2dva fvelimab syl5eqr mptpreima syl6eqr ccn divccncf cncfcn1 efopnlem2 adantll - ccncf syl6eleq cnima eqeltrd blcntr wfun cdm ffun syl6sseqr funfvima2 mpd + ccncf syl6eleq cnima eqeltrd blcntr wfun cdm ffun sseqtrrdi funfvima2 mpd fdmi eleq2 sseq1 anbi12d expr syl5 expimpd sylc ralrimiva anbi1d cnfldtop eleq1 ralima ctop eltop2 sylibr ) ABGZDUDZEUDZGZUVOHAUEZIZJZEBKZDUVQUFZUV QBGZUVMUWAUBUDZHLZUVOGZUVRJZEBKZUBAUFZUVMUWGUBAUVMUWCAGZJUWCMGZUCUDZUANUG @@ -403707,7 +403707,7 @@ this vertex from a simple graph (see ~ uhgrspan1 ) is a simple graph. -> ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) $= ( wcel wa cv cfv cpw crab wi wss simpr adantr cumgr cid cres crn chash c2 wceq cdif rnresi wnel wral cuhgr cedg umgruhgr eleq2i biimpi cvtx edguhgr - csn elpwi syl6sseqr syl syl2an ad4ant13 elpwdifsn syl3anc ralrimiva rabss + csn elpwi sseqtrrdi syl syl2an ad4ant13 elpwdifsn syl3anc ralrimiva rabss ex sylibr eqsstrid elrabi syl6eleq edgumgr simprd syl5com eleq2s ssrabdv impcom ) DUAKZEFKZLZUBCUCUDCGMZUENUFUGZGFEUSUHOZPCUIWBWDGWECWBCEAMZUJZABP ZWEJWBWGWFWEKZQZABUKWHWERWBWJABWBWFBKZLZWGWIWLWGLWKWFFRZWGWIWLWKWGWBWKSTV @@ -403738,7 +403738,7 @@ this vertex from a simple graph (see ~ uhgrspan1 ) is a simple graph. upgrres1 $p |- ( ( G e. UPGraph /\ N e. V ) -> S e. UPGraph ) $= ( vp vx wcel wa cv chash cfv c2 cle cid cres cdm wbr csn cdif cpw c0 crab cupgr wf wf1o f1oi f1of mp1i ffdmd wnel wral wss simpr adantr cedg eleq2i - wi cvtx wne w3a edgupgr syl6sseqr 3ad2ant1 syl sylan2b ad4ant13 elpwdifsn + wi cvtx wne w3a edgupgr sseqtrrdi 3ad2ant1 syl sylan2b ad4ant13 elpwdifsn elpwi syl3anc wn simpl biimpi simp2d syl2an nelsn eldifd ralrimiva sylibr rabss eqsstrid elrabi ciedg crn edgval eqtri eqid upgrf frnd sseld syl5bi ex weq fveq2 breq1d elrab simprbi syl6 syl5com eleq2s impcom ssrabdv fssd @@ -404421,7 +404421,7 @@ function instead of the edges themselves (see also ~ nbgrval ). nbgrssvwo2 $p |- ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( V \ { M , X } ) ) $= ( cnbgr co wnel csn cdif cpr wss wi nbgrssovtx cin c0 wceq wcel wn df-nel - disjsn sylbb2 reldisj syl5ib ax-mp prcom difeq2i difpr eqtri syl6sseqr ) + disjsn sylbb2 reldisj syl5ib ax-mp prcom difeq2i difpr eqtri sseqtrrdi ) BADFGZHZUKCDIJZBIZJZCBDKZJZUKUMLZULUKUOLZMACDENULUKUNOPQZURUSULBUKRSUTBUK TUKBUAUBUKUNUMUCUDUEUQCDBKZJUOUPVACBDUFUGCDBUHUIUJ $. $} @@ -432632,7 +432632,7 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the cpw an32s nvcl simpllr simplrl letr syl3anc mpan2d fvexi rabex fvmpt2 expr mpan2 eleq2d ralbidv syl6bb bicomd sylan9bbr ffnd fnfvelrn syl6d sylbird dfss3 eqssd ne0i mpanl12 syl2anc ffvelrn sseldi elpwid ntrss3 - bcth2 cbl ntropn mopni2 mp3an1 syl6sseqr cdiv ntrss2 syl5com ad2antrr + bcth2 cbl ntropn mopni2 mp3an1 sseqtrrdi cdiv ntrss2 syl5com ad2antrr c2 w3a jctil rphalfcl rpxrd rpxr rphalflt 3jca blsscls2 breq2 rabbidv sseq1d rspcev 3syld syldan jcad eximdv n0 df-rex 3imtr4g reximdva ) A KUGZFUHZLUIUHUHZUJUKZKULUMZCUGZDUGZGUNZPUGZUOUPZDOUQZUYRURZPUSUMZCOUM @@ -443312,7 +443312,7 @@ negative of a vector from this axiom (see ~ hvsubid and ~ hvsubval ). ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) ) $= ( wcel chba wss wa cva cxp cima csm cc cv co wral wb wfun cdm ax-hfvadd - wf csh c0v issh ffun ax-mp xpss12 anidms fdmi syl6sseqr sylancr ax-hfvmul + wf csh c0v issh ffun ax-mp xpss12 anidms fdmi sseqtrrdi sylancr ax-hfvmul funimassov xpss2 anbi12d adantr pm5.32i bitri ) CUADCEFZUBCDZGZHCCIZJCFZK LCIZJCFZGZGUTAMZBMZHNCDBCOACOZVFVGKNCDBCOALOZGZGCUCUTVEVJURVEVJPUSURVBVHV DVIURHQZVAHRZFVBVHPEEIZEHTVKSVMEHUDUEURVAVMVLURVAVMFCECEUFUGVMEHSUHUIABCC @@ -457882,7 +457882,7 @@ r C_ ( p vH q ) ) ) -> ( r = p \/ r = q ) ) $= (New usage is discouraged.) $) mdsymlem1 $p |- ( ( ( p e. CH /\ ( B i^i C ) C_ A ) /\ ( B MH* A /\ p C_ ( A vH B ) ) ) -> p C_ A ) $= - ( cv cch wcel cin wss wa chj co mpan2 syl6sseqr wceq mpan adantr cdmd wbr + ( cv cch wcel cin wss wa chj co mpan2 sseqtrrdi wceq mpan adantr cdmd wbr chub2 chjcomi sseq2i biimpi anim12i sylib ad2ant2rl chjcl eqeltrid anim2i ssin chub1 ancoms dmdi mp3anl1 mpanl1 syl2anc adantlr incom oveq1i chincl wb chlejb1 3syl biimpa syl5eq eqtr3d adantrr sseqtrd ) DHZIJZBCKZALZMZBAU @@ -462373,7 +462373,7 @@ its graph has a given second element (that is, function value). cfn isfinite2 isfinite4 adantr bren 3adant3 cdif cmpt cin f1of adantl cxp sylib fconstmpt eqcomi wb simplr fconst2g mpbiri disjdif a1i fun syl21anc fz1ssnn undif mpbi feq2i 3adantl3 ssid wfo simpr forn sseqtrrid orcd ssun - f1ofo rnun syl6sseqr dff1o3 simprbi cnvun reseq1i resundir dff1o4 fnresdm + f1ofo rnun sseqtrrdi dff1o3 simprbi cnvun reseq1i resundir dff1o4 fnresdm eqtri wfn simpl3 cnveqi cnvxp incom disjsn biimpri syl5eqr syl5eq uneq12d xpdisjres un0 syl6eq funeqd mpbird nnex difexg ax-mp mptex unex feq1 rneq vex cvv sseq2d cnveq eqidd reseq12d 3anbi123d spcev syl3anc ex exlimimdd @@ -463220,7 +463220,7 @@ its graph has a given second element (that is, function value). ( vx vy va vb cxr clt cxad wcel wbr wrex wa vz vk vu vv vw wss csup co cv cle wral wi wceq cxp cima cfv sseld anim12d imp xaddcl syl ralrimivva cop cr fveq2 df-ov syl6eqr eleq1d ralxp sylibr wfun cdm wb xaddf ax-mp xpss12 - wf ffun syl2anc syl6sseqr funimass4 sylancr mpbird eqsstrd supxrcl eleq2d + wf ffun syl2anc sseqtrrdi funimass4 sylancr mpbird eqsstrd supxrcl eleq2d fdmi xaddcld pm5.32i nfvd ad2antrr simprl supxrub simprr xle2add syl22anc sseldd mp2and fvelima mpan adantl eqeq1d rexxp sylib ancom 2rexbii biimpa r19.29d2r breq1 reximi 19.9d2r sylbi ralrimiva w3a simplr simpr xlt2addrd @@ -463480,7 +463480,7 @@ its graph has a given second element (that is, function value). $( A finite set of sequential integers that is a subset of ` NN0 ` . (Contributed by Thierry Arnoux, 8-Dec-2021.) $) fz2ssnn0 $p |- ( M e. NN0 -> ( M ... N ) C_ NN0 ) $= - ( cn0 wcel cfz co cuz cfv fzssuz cc0 wss nn0uz eleq2i biimpi uzss syl6sseqr + ( cn0 wcel cfz co cuz cfv fzssuz cc0 wss nn0uz eleq2i biimpi uzss sseqtrrdi syl sstrid ) ACDZABEFAGHZCABISTJGHZCSAUADZTUAKSUBCUAALMNJAOQLPR $. ${ @@ -476586,7 +476586,7 @@ commutative monoid (=vectors) together with a semiring (=scalars) and a E. r e. B ( X e. r /\ r C_ A ) ) $= ( vd co wcel wa crp cr cc vz vm ctx c1st cfv cv cdiv cmin caddc cioo c2nd cxp wss wrex wral crn cmpo wceq cxr wfn cpw clt df-ioo ixxf ffn mp1i cuni - c2 elssuni ctg ctop retop eqeltri uniretop unieqi eqtr4i txunii syl6sseqr + c2 elssuni ctg ctop retop eqeltri uniretop unieqi eqtr4i txunii sseqtrrdi wf ad2antrr simplr sseldd xp1st syl simpr rpred rehalfcld resubcld fnovrn rexrd readdcld syl3anc xp2nd eqidd eqeq2d vex syl6eleqr ralrimiva cvv wbr eqid rphalfcld ltsubrpd ltaddrpd w3a wb elioo1 syl2anc mpbir3and jca cabs @@ -485596,7 +485596,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry ( crn wcel w3a wne wo ccnv csn cima cin cfv cc0 cle wbr cpnf clt cico wa cr cxr cicc cdm cmeas cuni measbasedom sylib 3ad2ant1 csiga dmmeas co syl csigagen ct1 sgsiga eqeltrid sibfmbl ccld wss ctps ctop tpstop - cmbfm cldssbrsiga 3syl syl6sseqr sibff frnd simp2 sseldd eqid t1sncld + cmbfm cldssbrsiga 3syl sseqtrrdi sibff frnd simp2 sseldd eqid t1sncld syl2anc mbfmcnvima inelsiga syl3anc measvxrge0 elxrge0 simplbi adantr simp3 0re a1i simprbi pnfxr measssd cdif simpl1 anim1i eldifsn sylibr inss1 sibfima wb elico2 mp2an simp3bi xrlelttrd inss2 jaodan syl22anc @@ -492199,7 +492199,7 @@ strict in the case where the sets B(x) overlap. (Contributed by Thierry $( Lemma for ~ ftc2re . (Contributed by Thierry Arnoux, 20-Dec-2021.) $) fct2relem $p |- ( ph -> ( A [,] B ) C_ E ) $= ( co cxr wcel clt wbr wa syl6eleq syl simpld simprd eliooord cicc eliooxr - cioo wss iccssioo syl22anc syl6sseqr ) ABCUAJZDEUCJZFADKLZEKLZDBMNZCEMNZU + cioo wss iccssioo syl22anc sseqtrrdi ) ABCUAJZDEUCJZFADKLZEKLZDBMNZCEMNZU HUIUDAUJUKABUILZUJUKOABFUIHGPZBDEUBQZRAUJUKUPSAULBEMNZAUNULUQOUOBDETQRADC MNZUMACUILURUMOACFUIIGPCDETQSDEBCUEUFGUG $. @@ -499042,7 +499042,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a w-bnj15 wfn csuc wral w3a csn cdif cab c-bnj18 wss weu wne 1onn 1n0 ne0ii eldifsn mpbir2an biid eqid bnj852 r19.2z sylancr euex bnj31 rexcom4 sylib bnj1198 simp2 reximi sylbi df-rex 19.41v simprbi cdm bnj900 fveq2 ssiun2s - abid ssiun2 bnj882 syl6sseqr sstrd eqsstrrd exlimiv ) ABUBCAHIZDJZWGEJZUC + abid ssiun2 bnj882 sseqtrrdi sstrd eqsstrrd exlimiv ) ABUBCAHIZDJZWGEJZUC ZKWGLZABCMZNZFJZUDZWHHWNWGLGWMWGLZABGJMONUAFPUEZUFZEPKUGUHZQZDUIZHZDRWKAB CUJZUKZWFWSDXAWFWQDRZEWRQWSDRWFWQDULZXDEWRWFWRKUMXEEWRUEXEEWRQSWRSWRHSPHS KUMUNUOSPKUQURUPWLWPGAWRBDFECWLUSZWPUSZWRUTZVAXEEWRVBVCWQDVDVEWQEDWRVFVGW @@ -499820,7 +499820,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a ) ) $= ( cv wcel nfv cdm wa cfv c-bnj18 wss wi wfn w3a wrex cab nfcv bnj911 nf5i nfrex nfab nfcxfr nfcri nfan nfim nf5ri wb weq eleq1w anbi2d fveq2 sseq1d - imbi12d equcoms bnj1317 dmeq eleq2d anbi12d fveq1 ssiun2 bnj882 syl6sseqr + imbi12d equcoms bnj1317 dmeq eleq2d anbi12d fveq1 ssiun2 bnj882 sseqtrrdi ciun sylan9ssr chvar spei bnj1131 ) IRZESZKRZWBUAZSZUBZWDWBUCZDGMUDZUEZUF ZJWKJWGWJJWCWFJJIEJEHRZLRUGABUHZLFUIZHUJQWNJHWMJLFJFUKWMJABCDGHJLMNOULUMU NUOUPUQWFJTURWJJTUSUTWKWCJRZWESZUBZWOWBUCZWIUEZUFZJKWKWTVAKJKJVBZWGWQWJWS @@ -501137,7 +501137,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a bnj1286 $p |- ( ps -> _pred ( x , A , R ) C_ D ) $= ( cv c-bnj14 cdm cin wss wcel wbr wral wfn bnj1256 bnj1196 bnj1517 adantr wn wa wb wceq sseq2 raleqbi1dv syl adantl mpbird bnj593 bnj937 bnj835 cfv - ssrab3 bnj1292 sstri sseli bnj836 bnj1294 bnj1259 bnj1293 ssind syl6sseqr + ssrab3 bnj1292 sstri sseli bnj836 bnj1294 bnj1259 bnj1293 ssind sseqtrrdi fndm wne ) BEICUDZUEZKUDZUFZLUDZUFZUGHBWCWEWGBWCWEUHZCWEAWBMUIZDUDWBIUJUQ DMUKZWHCWEUKZBUCAWKPAPUDZFUIZWDWLULZURZWKPAWNPFABCDEFGHIJKLMNOPQRSTUAUBUC UMUNWOWKWCWLUHZCWLUKZWMWQWNWLEUHWQPFQUOZUPWNWKWQUSZWMWNWEWLUTWSWLWDVTWHWP @@ -501593,7 +501593,7 @@ have become an indirect lemma of the theorem in question (i.e. a lemma bnj1408 $p |- ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) = B ) $= ( vz wcel wa c-bnj18 wss syl2anc sstrd biid w-bnj15 biimpri cvv wral ciun w-bnj19 c-bnj14 bnj1413 cv simplll bnj213 sseli adantl bnj906 bnj1318 cun - ssiun2s ssun4 syl6sseqr syl w3a simpr bnj1405 nfv nfcv nfiu1 nfcxfr nfcri + ssiun2s ssun4 sseqtrrdi syl w3a simpr bnj1405 nfv nfcv nfiu1 nfcxfr nfcri nf5ri bnj1521 3ad2ant1 bnj1147 simp3 bnj1213 simp2 bnj1125 syl3anc ssiun2 nfun nfan 3ad2ant2 bnj593 nfss bnj1397 wo bnj1138 sylib mpjaodan df-bnj19 ralrimiva sylibr bnj931 a1i syl3anbrc bnj1124 iunss1 3syl 3sstr4g bnj1136 @@ -502060,7 +502060,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a dmeqi bnj1436 bnj836 bnj1373 rexbii bnj1196 3anass bnj1198 w-bnj17 bnj252 sylib bitri bnj1444 bnj1340 wfn wral bnj771 bnj1445 fveq2 cres cop bnj602 wa id reseq2d opeq12d 3eqtr4g fveq2d eqeq12d bnj1254 simp3bi fndm eleqtrd - bnj769 rspcdva bnj930 bnj835 wss simp2bi elssuni syl6sseqr bnj593 bnj1397 + bnj769 rspcdva bnj930 bnj835 wss simp2bi elssuni sseqtrrdi bnj593 bnj1397 wfun ssun3 bnj1502 sseq1d bnj1517 bnj770 sseqtrrd bnj1503 3eqtr4d bnj1446 3syl opeq2d bnj1447 bnj1448 ) GLVNZRVOZUDUBVOZVPZTGIUUQTUUNTVNZVQZVRZGITU CGTUCUUSUUNGUUNUCVSZVQZTUCUUSVTGUUNQVQZUVBGUUNMSJVNZWAZUVCGDUUNUVEVRZVHWB @@ -502151,7 +502151,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a bnj1452 $p |- ( ch -> E e. B ) $= ( wcel wss cv c-bnj14 wral csn c-bnj18 cun wex wn wbr bnj1212 bnj1147 a1i snssd unssd eqsstrid wa elsni adantl bnj602 syl w-bnj15 c0 simplbi bnj835 - wne bnj906 syl2anc ad2antrr eqsstrd ssun4 syl6sseqr simpr bnj1213 bnj1125 + wne bnj906 syl2anc ad2antrr eqsstrd ssun4 sseqtrrdi simpr bnj1213 bnj1125 wceq syl3anc sstrd wo bnj1424 mpjaodan ralrimiva wsbc cvv wb snex bnj1149 bnj893 eqeltrid bnj1454 weq sseq1d cbvralv anbi2i sbcbii sseq1 raleqbi1dv syl6bb sseq2 anbi12d sbcieg bitrd mpbir2and ) BOHUQZOGURZGMFUSZUTZOURZFOV @@ -502459,7 +502459,7 @@ become an indirect lemma of the theorem in question (i.e. a lemma of a vt bnj1436 bnj1299 fndm bnj31 bnj1196 simpld anim1i bnj593 sseq1 biimparc c-bnj14 bnj937 sselda rexlimiva sylbi bnj1317 bnj1400 dmeqi ssriv a1i csn eleq2s c-bnj18 cun bnj1493 vsnid elun1 mpbiri reximi ralimi ralbii sylibr - ax-mp eleq2 syl nfcv bnj1309 bnj1307 nfcii nfiun dfss3f syl6sseqr eqssd ) + ax-mp eleq2 syl nfcv bnj1309 bnj1307 nfcii nfiun dfss3f sseqtrrdi eqssd ) BEUCZGUDZBWPBOWOUAWPBUAPZBQZWQDUEZUDZWPWRWQFDFPZUDZUFZWTWQXCQWQXBQZFDRWRF WQDXBUGXDWRFDXADQZXBBWQXEXBBOZJXEJPZBOZXBXGUHZSZXFJXEXGCQZXISXJJXEXIJCXEX AXGUIZXIJCXEXLAPZXAUJIHUJUHAXGTZJCXLXNSJCRZFDMULUMXGXAUNUOUPXKXHXIXKXHBEX @@ -502597,7 +502597,7 @@ have become an indirect lemma of the theorem in question (i.e. a lemma ( vw w-bnj15 cv cfv c-bnj14 cres cop wceq cdm wcel ciun simprbi wfn bnj60 fndm syl bnj832 eleqtrrd cuni dmeqi wral wa wrex bnj1317 bnj1400 syl6eleq eqtri bnj1405 bnj1209 bnj1436 bnj1299 bnj31 bnj836 bnj1518 bnj1521 bnj930 - wfun bnj835 wss elssuni syl6sseqr simp3bi bnj1502 bnj1514 bnj1294 bnj1517 + wfun bnj835 wss elssuni sseqtrrdi simp3bi bnj1502 bnj1514 bnj1294 bnj1517 eqtrd eleqtrd bnj1503 opeq2d syl6eqr fveq2d eqtr4d bnj593 bnj1519 bnj1397 sseqtrrd bnj1520 bnj1459 ) EHUBZADUCZJUDZXAJEHXAUEZUFZUGZKUDZUHZDERAXGIAB XGIXAIUCZUIZUJZABIGAIGXIXAAXAJUIZIGXIUKZAXAEXKAWTXAEUJZRULWTXMXKEUHZARWTJ @@ -503044,7 +503044,7 @@ have become an indirect lemma of the theorem in question (i.e. a lemma A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) ) $= ( cuhgr wcel cedg cfv c2 cv chash cle wbr cpw wss wf crn syl ciedg edgval crab cdm wral rneqi eqtr4i sseq1i wfun wi uhgrfun fdmrn fss sylbi impbid1 - ex frn syl5bb wb cvtx c0 csn uhgredgss difss2d pweqi syl6sseqr ssrab baib + ex frn syl5bb wb cvtx c0 csn uhgredgss difss2d pweqi sseqtrrdi ssrab baib bitr3d ) BGHZBIJZKALMJNOZADPZUCZQZCUDZVNCRZVLAVKUEZVOCSZVNQZVJVQVKVSVNVKB UAJZSVSBUBCWAFUFUGUHVJVTVQVJCUIZVTVQUJZCBFUKWBVPVSCRZWCCULWDVTVQVPVSVNCUM UPUNTVPVNCUQUOURVJVKVMQZVOVRUSVJVKBUTJZPZVMVJVKWGVAVBBVCVDDWFEVEVFVOWEVRV @@ -506891,7 +506891,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by $( Lemma for ~ cvmopn . (Contributed by Mario Carneiro, 7-May-2015.) $) cvmopnlem $p |- ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( F " A ) e. J ) $= ( vx vy co wcel wa cv wss adantr vz vt vw ccvm cima wrex wral cfv c0 cuni - wne simpll wf ccn cvmcn eqid cnf elssuni syl6sseqr adantl sselda ffvelrnd + wne simpll wf ccn cvmcn eqid cnf elssuni sseqtrrdi adantl sselda ffvelrnd syl cvmcov syl2anc wex crio cin crest cres wceq inss2 resima2 ax-mp chmeo n0 simprr simprl cvmsiota syl13anc simpld cvmtop1 simpllr elrestr syl3anc cvmshmeo ctop hmeoima wb cvmtop2 ad2antrr cvmsrcl ad2antll restopn2 mpbid @@ -506921,7 +506921,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by cvmfolem $p |- ( F e. ( C CovMap J ) -> F : B -onto-> X ) $= ( vx vy vz wcel cv cfv wa vw vt ccvm co wf wceq wrex wral wfo ccn cnf syl cvmcn c0 wne cvmcov ex wex n0 cvmsn0 ad2antll sylib cres ccnv wss simprlr - cuni cvmsss simprr sseldd elssuni syl6sseqr simpll cvmsf1o syl3anc f1ocnv + cuni cvmsss simprr sseldd elssuni sseqtrrdi simpll cvmsf1o syl3anc f1ocnv wf1o f1of 3syl simprll ffvelrnd f1ocnvfv2 syl2anc fvres eqtr3d fveq2 expr rspceeqv exlimdv syl5bi expimpd rexlimdva syld ralrimiv dffo3 sylanbrc mpd ) GDHUCUDQZCIGUEZNRZORZGSZUFOCUGZNIUHCIGUIWRGDHUJUDQWSDGHUMGDHCILMUKU @@ -507250,7 +507250,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by co cima wfn wb ccn cvmcn cnf 3syl fniniseg mpbid simpld simprd cicc ffn cxr cle wbr cr cn elfznn nnred peano2rem nndivred rexrd clt cc0 ltm1d nngt0d ltdiv1 syl112anc syl3anc syl6eleqr cvmliftlem3 eqeltrd - lbicc2 eqid cvmsiota syl13anc sseldd elssuni syl6sseqr wf1o cvmsf1o + lbicc2 eqid cvmsiota syl13anc sseldd elssuni sseqtrrdi wf1o cvmsf1o ltled f1ocnv f1of simprr ffvelrnd anassrs fmpttd fvres feqmptd cii cvmliftlem5 syldan feq1d f1ocnvfv2 syl2anc 3eqtr2rd mpteq2dva fveq2 mpbird fmptco iiuni cvmliftlem2 fssresd 3eqtr4d jca ) ABVBZUBGTJVCZ @@ -507354,7 +507354,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by eqtr4i ovexd syl3anc syl5eq oveq1d eleqtrd wb cvmtop2 toptopon simprl sylib simprr cvmliftlem3 anassrs mpbid simpld cxr wbr nnred rexrd clt nndivred eqeltrd fmpttd frnd cuni cvmliftlem1 cvmsrcl elssuni cnrest2 - syl6sseqr chmeo csn cima cvmliftlem7 wfn cvmcn fniniseg simprd adantl + sseqtrrdi chmeo csn cima cvmliftlem7 wfn cvmcn fniniseg simprd adantl ffn cle peano2rem ltm1d nngt0d ltdiv1 syl112anc ltled lbicc2 cvmsiota syl6eleqr syl13anc cvmshmeo syl2anc hmeocnvcn cnmpt11f sseldd ) ASURT USUTVAZVBZSIVCZCUACVDZPVCZOSURVEUTZTVFUTZUVTIVCVCZUDVDVAUDSKVCZVGVCZV @@ -507563,7 +507563,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by cvmliftlem13 $p |- ( ph -> ( K ` 0 ) = P ) $= ( cc0 cfv c1 cop csn wfun wss cdm wcel wceq cicc co cii wf cvmliftlem11 ccn ccom simpld iiuni cnf syl ffund cfz cv ciun cuz cn syl6eleq eluzfz1 - nnuz fveq2 ssiun2s syl6sseqr cmin cxr cle wbr 0xr a1i nnrecred rexrd cr + nnuz fveq2 ssiun2s sseqtrrdi cmin cxr cle wbr 0xr a1i nnrecred rexrd cr cdiv 1red 0le1 nnred nngt0d divge0 syl22anc lbicc2 syl3anc 1m1e0 oveq1i clt nncnd nnne0d div0d syl5eq oveq1d eleqtrrd cres wa simpr cvmliftlem7 eqid cvmliftlem6 mpdan fdmd cvmliftlem9 fveq2d fveq2i cvmliftlem4 eqtri @@ -507622,7 +507622,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by ex sylancr csn cxp ciun c1st weq cop vex sseq2d fveq2 c2nd crio cres cmpt cvv cmpo cseq ax-mp eqid 2fveq3 eleq1d syl5eq reseq2d cnveqd fveq1d oveq1 syl12anc adantr ffvelrnda cvmcov reximddv r19.42v rexbii elunirab 3bitr4i - ccvm rexcom ssrdv uniss mp1i syl6sseqr eqssd lebnumii wex cfn fzfi rexrab + ccvm rexcom ssrdv uniss mp1i sseqtrrdi eqssd lebnumii wex cfn fzfi rexrab 2rexbidv op1std rexiunxp wi imass2 sstr2 reximdv syl5bir impcom rexlimivw sylbi ralimi ac6sfi cid cun cioo sneq xpeq12d cbviunv feq3 simprr cbvmptv ctg cbvriotav fveq1 riotabidv oveq1d oveq12d fveq2d riotaeqbidv mpteq12dv @@ -507965,7 +507965,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by cpr pwsn syl6eqel txconn xpss2 snssd restuni sseqtrd syl3anc crn wb xpss1 df-ima imass2 3syl syl5eqr mpbird sstrd cnrest2 mpbid eleqtrd eqsstrrid conncn feq2d cc0 c1 cicc txunii cvmlift2lem5 cvmlift2lem7 - ccom txtopi syl6sseqr fvco3 fveq1d eqtr3d 3eqtr4g cvmsiota syl13anc + ccom txtopi sseqtrrdi fvco3 fveq1d eqtr3d 3eqtr4g cvmsiota syl13anc ccvm fveq2i eleq1i anbi2i xpss12 wral ad2antrl simprr ctopon sselda cv adantrr cvmlift2lem6 syldan cnrest resabs1d ovex restabs 3eltr3d xpex oveq1d cvmtop1 toptopon simprl imaco cnvco cnveqd imaeq1d wfun @@ -508113,7 +508113,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by cvmlift2lem11 $p |- ( ph -> ( ( U X. { Y } ) C_ M -> ( U X. { Z } ) C_ M ) ) $= ( csn cxp wss wa cv cii ctx ccnp cfv wcel cc0 cicc crab adantr cuni - co c1 elssuni iiuni syl6sseqr elunii syl6eleqr syl2anc snssd xpss12 + co c1 elssuni iiuni sseqtrrdi elunii syl6eleqr syl2anc snssd xpss12 syl cres crest ccn wrex wf wral cvmlift2lem5 fssresd simpr syl6sseq sseldd ssrab simprbi r19.21bi ctopon iitopon txtopon mp2an cnpresti toponunii syl3anc ralrimiva wb resttopon sylancr ctop ccvm toptopon @@ -508168,7 +508168,7 @@ property of an acyclic graph (see also ~ acycgr0v ). (Contributed by a1d chmeo cpw ccvm txopn opnneip syl3anc simplr2 cbvrexv simplr3 rspe elunii alrimivv ssntr simpr1 simpr2 sseldd opeq2 ralsn anassrs txtube dfss3 eleq1 ralxp ntrss2 sstr mpan2 r2al ralcom 3bitr2i ralimi rexbii - bicom ralbii rabeq2i ad3antlr elssuni syl6sseqr sselda sseq1d bibi12d + bicom ralbii rabeq2i ad3antlr elssuni sseqtrrdi sselda sseq1d bibi12d sylbi baib syl5ibr ralimdva syl5 anim2d reximdva ssrab2 eqsstri isclo sseldi 0elunit wrel relxp opelxp id df-3an wfn ffnd fnov snssd resmpo reseq1d simplll cvmlift2lem8 sylan syldan eqeq1d syl5ibrcom mpoeq3dva @@ -513361,7 +513361,7 @@ proper pair (of ordinal numbers) as model for a Godel-set of membership wfun cdm wb ffund simpld 3syl elpreima simplbda wbr wrex ciun cxp ssbrd cid imp brxp fveq2d msubvrs syl3anc eqtrd eleq2d eliun syl6bb wi breq12 wal cvv simpl simpr syl5bir vex simp2bi mvhf unssd fdmd funimass3 mpbid - frn sseqtrrd cnvco imaeq1i imaco eqtri syl6sseqr unssad sselda fnfvelrn + frn sseqtrrd cnvco imaeq1i imaco eqtri sseqtrrdi unssad sselda fnfvelrn unssbd ffn sylan simp1d cdif mdvval difss eqsstri simprd anbi12d reeanv simpll xpeq12d sseq1d imbi12d spc2gv el2v 3anbi123d anbi2d imbi1d 3exp2 vtocl2 imp4b rexlimdvva sylbid exp4b 3imp2 mclsax eqeltrrd mpbir2and ) @@ -515168,7 +515168,7 @@ Real and complex numbers (cont.) ( abs ` ( prod_ k e. ( K ... p ) A - prod_ k e. ( K ... j ) A ) ) < x ) @= ( wcel wa co cv crp c1 caddc cfz cprod cmin cabs cfv c2 cdiv clt wbr wral - cuz wrex ntrivcvgcaulem4 wss syl6eleq uzss syl6sseqr adantr sseld adantrd + cuz wrex ntrivcvgcaulem4 wss syl6eleq uzss sseqtrrdi adantr sseld adantrd syl wi w3a cmul fzfid simplll simpll elfzuz uztrn2 syl2an syl2anc fprodcl cr cc abscld 3adant3 simpl peano2uzs ax-1cn subcld simplr rphalfcld rpred 2re a1i cc0 cle absge0d simprl eleq1 anbi2d prodeq1d oveq1d fveq2d breq1d @@ -516953,7 +516953,7 @@ Set induction (or epsilon induction) -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) ) $= ( va vy vz cpred wcel cvv cv ciun cmpt crdg com cres crn wbr c0 syl mp2an cuni ctrpred wss wex cfv wceq fr0g wfn wb frfnom peano1 fnbrfvb sylib 0ex - breq1 spcev elrng mpbird elssuni df-trpred syl6sseqr ) ACDHZBIZVCEJFEKACF + breq1 spcev elrng mpbird elssuni df-trpred sseqtrrdi ) ACDHZBIZVCEJFEKACF KHLMZVCNOPZQZUBZACDUCVDVCVGIZVCVHUDVDVIGKZVCVFRZGUEZVDSVCVFRZVLVDSVFUFVCU GZVMVCBVEUHVFOUISOIVNVMUJVCVEUKULOSVCVFUMUAUNVKVMGSUOVJSVCVFUPUQTGVCVFBUR USVCVGUTTFACDEVAVB $. @@ -516982,7 +516982,7 @@ Set induction (or epsilon induction) ssid rspcev ssiun sylancl wral setlikespec trpredlem1 sseld expcom adantl fvex wi syld ralrimiv ad2antrr iunexg sylancr nfcv cbviunv iuneq1 cbvmptv syl5eq rdgeq1 reseq1 frsucmpt syl2anc sseqtrrd fveq2 dftrpred2 rexlimdva2 - mp2b syl6sseqr syl5bi ) DABCUCZKDELZFMGFLZABGLZNZOZUDZABCNZUEZPUFZUAZKZEP + mp2b sseqtrrdi syl5bi ) DABCUCZKDELZFMGFLZABGLZNZOZUDZABCNZUEZPUFZUAZKZEP UGCAKZABUHZQZABDNZWHRZGABECDFUIXBWSXDEPXBWIPKZQZWSQZWIUJZPKZXCXHWQUAZRZXD XGXEXIXBXEWSUBZWIUKSXGXCHWRABHLZNZOZXJXGWSXCXCRZXCXORZXFWSULXCUOWSXPQXCXN RZHWRUGXQXRXPHDWRXMDTXNXCXCABXMDUMUNUPHWRXNXCUQSURXGXEXOMKZXJXOTXLXGWRMKX @@ -517138,7 +517138,7 @@ Set induction (or epsilon induction) cpred cmpt crdg cres wbr wo eltrpred csuc nn0suc fveq2 anbi2d setlikespec c0 biimpd fr0g syl biimpa syl6com wral wss trpredlem1 sseld expcom adantl fvex syld ralrimiv iunexg sylancr nfcv nfmpt1 nfrdg nfres nffv nfiun eqid - predeq3 cbviunv iuneq1 syl5eq frsucmpt sylan2 expimpd dftrpred2 syl6sseqr + predeq3 cbviunv iuneq1 syl5eq frsucmpt sylan2 expimpd dftrpred2 sseqtrrdi eliun ssiun2 vex elpredim a1i anim12d reximdv2 com12 sylbi com23 rexlimdv pm2.43d orim12d ex syl5 syl5bi ) EBCDUAZJEFKZGLHGKZBCHKZUCZMZUDZBCDUCZUEZ NUFZOZJZFNPDBJZBCUBZQZEXKJZEAKZCUGZAXDPZUHZHBCFDEGUIXRXOYCFNXENJXEUORZXEI @@ -518096,7 +518096,7 @@ Set induction (or epsilon induction) ( vw vg va cv wcel wex wss wa syl cdm cop cpred vex eldm2 wfn wral cfv co cres wceq w3a cab cuni frrlem5 frrlem1 unieqi eqtri eleq2i eluniab wi wel bitri simpr2r opeldm adantr simpr1 fndm eleqtrd rsp sseqtrrd 19.8a abeq2i - sylc sylibr adantl elssuni syl6sseqr sstrd expcom exlimiv impcom sylbi + sylc sylibr adantl elssuni sseqtrrdi sstrd expcom exlimiv impcom sylbi dmss ) COZHUAZPWELOZUBZHPZLQDFWEUCZWFRZLWEHCUDZUEWIWKLWIWHMOZPZWMNOZUFZWO DRZWJWORZCWOUGZSZWEWMUHWEWMWJUJIUIUKCWOUGZULZNQZSZMQZWKWIWHXCMUMZUNZPXEHX GWHHEUNZXGABDEFGHIJKUOZEXFABNCDEFGMIJUPZUQURUSXCMWHUTVCXDWKMXCWNWKXBWNWKV @@ -518141,7 +518141,7 @@ Set induction (or epsilon induction) ( vz wcel wceq wss cv cdm cfv cpred cres co cop wex vex eldm2 wfn wral wa w3a cuni frrlem5 unieqi eqtri eleq2i eluniab bitri wi 19.8a 3ad2ant2 abid cab sylibr elssuni syl wel simpl23 simpl3 opeldm simpl21 fndm eleqtrd rsp - syl6sseqr sylc wfun simpl1 frrlem9 simpr funssfv syl3anc simp22r sseqtrrd + sseqtrrdi sylc wfun simpl1 frrlem9 simpr funssfv syl3anc simp22r sseqtrrd adantr fun2ssres oveq2d 3eqtr4d mpdan 3exp exlimdv impcomd syl5bi imp ) A CUAZLUBRZWRLUCZWRLFHWRUDZUEZMUFZSZWSWRQUAZUGZLRZQUHAXDQWRLCUIZUJAXGXDQXGX FIUAZRZXIBUAZUKZXKFTZXAXKTZCXKULZUMZWRXIUCZWRXIXAUEZMUFZSZCXKULZUNZBUHZUM @@ -518202,7 +518202,7 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $= wbr frrlem10 sylan2 adantlr cop fveq1i c0 wfun frrlem9 funres dmres df-fn wfn syl sylanblrc adantr vex ovex fnsn a1i wn eldifn disjsn sylibr adantl nsyl simpr fvun1 syl112anc syl5eq elinel1 fvresd eqtrd wss frrlem11 fnfun - ssun1 sseqtrri wral eldifi rspa frrlem8 ssind syl6sseqr fun2ssres syl3anc + ssun1 sseqtrri wral eldifi rspa frrlem8 ssind sseqtrrdi fun2ssres syl3anc syl2an resabs1d oveq2d 3eqtr4d ex fvsn vsnid fvun2 reseq1i resundir eqtri wfr predfrirr ressnop0 uneq12d un0 syl6eq 3eqtr4a fveq2 id predeq3 syl5bi reseq2d oveq12d eqeq12d syl5ibrcom jaod 3impia ) ADUGZHPUHZUIUJZEUGZLUUIU @@ -518281,7 +518281,7 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $= ` ( A \ dom F ) ` . (Contributed by Scott Fenton, 7-Dec-2022.) $) frrlem14 $p |- ( ph -> dom F = A ) $= ( cdm wss frrlem7 a1i cdif c0 wceq cv cpred wrex wcel wa wn eldifn adantl - cuni frrlem13 elssuni syl frrlem5 syl6sseqr dmss cres csn cun ssun2 vsnid + cuni frrlem13 elssuni syl frrlem5 sseqtrrdi dmss cres csn cun ssun2 vsnid sselii cop dmeqi dmun ovex dmsnop uneq2i 3eqtri eleqtrri sseldd expr mtod co nrexdv wne df-ne sylan2br ex mt3d ssdif0 sylibr eqssd ) APUHZHWQHUIABC HIKMPQRSUJUKAHWQULZUMUNZHWQUIAWSWRKDUOZUPUMUNZDWRUQZAXADWRAWTWRURZUSXAWTW @@ -528146,7 +528146,7 @@ A Fne if ( S = (/) , { X } , U. S ) ) $= wf co fssres2 sylancr filtop xpexg mpdan ssexd fex syl2anc dirdm simpli syl syl6reqr feq2d mpbid cfg cima c1st wral cpw wfn tailf mpbird adantr eqid ffn imaeq2 sseq1d rexrn 3syl wfun wfo fo2nd fofn ax-mp ssv fnssres - mp2an fnfun ffvelrnda elpwid ad2antrr sseqtrrd fndm syl6sseqr funimass4 + mp2an fnfun ffvelrnda elpwid ad2antrr sseqtrrd fndm sseqtrrdi funimass4 wb wbr simpr eleqtrd vex a1i eltail syl3anc biantrurd anbi1d filnetlem1 syl6bbr bitr4d imbi1d eleq1d bitri rexbidva csn ciun cop op1std imbi12d weq wne sseq1 cfbas wn sylib ss0b dmss eqeq2d anbi12d ralbidv2 raliunxp @@ -539240,7 +539240,7 @@ coordinates of a barycenter of two points in one dimension (complex ( 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 - rneqd abbii eqtri syl6sseqr wi sstr expcom adantr mpd ssexd isset sylib + 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 eltg3 sylibrd ssrdv eqssd ) EDIZDCUAJZKZLZDCUBZXGUPCUCDIZDXHIZXFXIXJLXD @@ -540710,7 +540710,7 @@ coordinates of a barycenter of two points in one dimension (complex vex simpll sseq1 mpbiri adantl cldlp adantr mpbird sylanl1 adantllr simpr 0ss w3a wf1 cldss wf nlpineqsn reximi ralimi ineq1 eqeq1d ac6s fvineqsnf1 csn 3syl jca eximi syl syl3an2 syl3an1 3adant1r crn cun ciun vsnid elin1d - eleq2 ralssiun anim1i unisng syl6sseqr unss12 unidm syl6sseq sylan syl2an + eleq2 ralssiun anim1i unisng sseqtrrdi unss12 unidm syl6sseq sylan syl2an syldan sylan2 adantlrr isfinite adantrr ad2antrr mpd eqeq2d sylibr df-rex ex unieq a1i eximdv exlimdv sylan2b adantlr sseld wfn f1fn fniunfv cldopn sseqtrd ancomd eqcomd eqimss ssun4 uniun ssun3 uncom undif1 eqtri ssequn2 @@ -543328,7 +543328,7 @@ can be simplified (see ~ wl-dfrexf , ~ wl-dfrexv ). cfrlm clinds w3a cuvc crn cdom cen clss cmri cpw wrex cmrc cbs cmre clmod crg drngring frlmlmod lssmre csn cdif wral cacs clvec csca simpl eqeltrrd frlmsca islvec sylanbrc lssacsex simprd wss dif0 linds1 3ad2ant3 wf uvcff - frnd syl6sseqr wceq fveq2i clspn mrclsp fveq1d clbs frlmlbs eqtr3d syl5eq + frnd sseqtrrdi wceq fveq2i clspn mrclsp fveq1d clbs frlmlbs eqtr3d syl5eq un0 lbssp sseqtrrd cnzr drngnzr adantr jca lindsind2 3expa sylanl1 eleq2d wn wb ad2antrr mtbid ralrimiva 3impa ismri2 syl2an eqeltrid wo simpr enfi mpbird uvcendim mpbid olcd mreexexd cvv ovex elpwi ssdomg endomtr syl2anr @@ -548079,7 +548079,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= wf ax-mp ssrab2 cle oveq1 oveq1d opeq12d oveq2 oveq2d cbvmpov dyadf inss2 cin frn rexpssxrxp sstri fdmi sseqtrri funimass4 mp2an sspwuni sylib cabs cmin ccom cres cbl crp wrex cxmet eqid rexmet cmopn mopni2 mp3an1 elssuni - tgioo wceq uniretop syl6sseqr sselda rpre bl2ioo syl2an 2re 1lt2 expnlbnd + tgioo wceq uniretop sseqtrrdi sselda rpre bl2ioo syl2an 2re 1lt2 expnlbnd cn mp3an23 ad2antrl cmul cfl ad2antrr 2nn nnnn0 nnexpcl sylancr nnred syl syl112anc mpbird nndivred syl2anc rexrd readdcld recnd ltadd2dd eqbrtrd remulcld fllelt simpld cc0 reflcl ledivmul2 peano2re ltmuldiv mpbid ltled @@ -549182,7 +549182,7 @@ curry M LIndF ( R freeLMod I ) ) ) $= eqeltrid ssdif ovex rabex fnmpti resttopon sylancr cnpfval sylancl fneq1d mpbiri elpreima wbr wrel rele elrelimasn fvex epeli bitr2i syl6rbbr imaco anbi2i abid2 eqtr4i sseqtrid difmbl eqeltrrid eleq2i ibar sylan9bb notbid - difeq2d biimpd adantrd ss2rabdv dfdif2 syl6sseqr 3adant1 eqeltrd 3ad2ant1 + difeq2d biimpd adantrd ss2rabdv dfdif2 sseqtrrdi 3adant1 eqeltrd 3ad2ant1 unmbl ismbf mpbird ) AGBUAZAUBUCZHZAUDUEZUFIZAUGUHZUXPUIUHZUJZJUKBULZKZLZ UMIUNMZUOZBUPHZBUJZCNZKZUXMHZCUXOOZUYDUYICUXOUYDUYGUXOHZPUYHBDNZUXRIZHZDE URZBENZKZUYGQZPZPZEUXQUQZDARZUYNSZUYLBIZUYGHZPZDARZVJZUXMUXLUXNUYKUYHVUHM @@ -555022,7 +555022,7 @@ counterexample is the discrete extended metric (assigning distinct metcl rpred mpan2d anassrs ccl cab ccmp ctop cuni cxmet metxmet mopntop clm cmet frnd mopnuni clscld rexlimdvw abssdv elpw2 sylibr elin ssabral velpw anbi1i csn cun ffn 0z ssv int0 sseqtrri ssun1 anim2i imim1i ssun2 - ralsn sscls sseq2 syl5ibrcom anim12i intunsn syl6sseqr rexlimdvv reeanv + ralsn sscls sseq2 syl5ibrcom anim12i intunsn sseqtrrdi rexlimdvv reeanv ssin ss2in cbvrexv 3imtr3g expd findcard2 com12 impr ffnd eqeltri mpan2 sylcom 1z uzn0 wfun fnfun fndm sseqtrrid funfvima2 necomd neneqd nrexdv ne0i 0ex zex pwex frn ssexi abrexex elfi sylnibr cmptop cmpfi ibi fveq2 @@ -585075,7 +585075,7 @@ one element is a lattice line (expressed as the join ` P .\/ Q ` ). osumcllem1N $p |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. U ) -> ( U i^i M ) = M ) $= ( chlt wcel wss w3a cv wa cin wceq csn sspadd1 adantr cfv simpl1 paddssat - co 2polssN syl2anc syl6sseqr sstrd simpr snssd cpsubsp wb simpl2 polssatN + co 2polssN syl2anc sseqtrrdi sstrd simpr snssd cpsubsp wb simpl2 polssatN eqsstrid eqid polsubN eqeltrid paddss syl13anc mpbi2and sseqin2 sylib ) F UAUBZJAUCZKAUCZUDZLUEZDUBZUFZHDUCDHUGHUHWAHJVSUIZCUOZDSWAJDUCZWBDUCZWCDUC ZWAJJKCUOZDVRJWGUCVTAUACFJKOPUJUKWAWGWGIULZIULZDWAVOWGAUCZWGWIUCVOVPVQVTU @@ -585089,7 +585089,7 @@ one element is a lattice line (expressed as the join ` P .\/ Q ` ). osumcllem2N $p |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. U ) -> X C_ ( U i^i M ) ) $= ( chlt wcel wss w3a cv wa cin csn co simpl1 simpl2 simpr snssd cfv adantr - paddssat polssatN syl2anc eqsstrid sspadd1 syl6sseqr osumcllem1N sseqtrrd + paddssat polssatN syl2anc eqsstrid sspadd1 sseqtrrdi osumcllem1N sseqtrrd sstrd syl3anc ) FUAUBZJAUCZKAUCZUDZLUEZDUBZUFZJHDHUGVLJJVJUHZCUIZHVLVFVGV MAUCJVNUCVFVGVHVKUJZVFVGVHVKUKVLVMDAVLVJDVIVKULUMVLDJKCUIZIUNZIUNZATVLVFV QAUCZVRAUCVOVLVFVPAUCZVSVOVIVTVKAUACFJKOPUPUOAFIVPOQUQURAFIVQOQUQURUSVDAU @@ -585366,7 +585366,7 @@ to be equivalent to (and derivable from) the orthomodular law ~ poml4N . -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M = X ) $= ( chlt wcel wss cfv wceq cv w3a c0 wne co cin pexmidlem5N 3adantr1 fveq2d wn simpl1 pol0N syl eqtrd ineq1d simpl2 csn simpl3 snssd paddssat syl3anc - wa eqsstrid 3jca sspadd1 syl6sseqr cpscN wb ispsubclN mpbir2and paddatclN + wa eqsstrid 3jca sspadd1 sseqtrrdi cpscN wb ispsubclN mpbir2and paddatclN simpr1 eqid eqeltrid psubcli2N syl2anc poml4N sylc sseqin2 sylib 3eqtr3rd jca ) DPQZHARZIUAZAQZUBZHGSZGSZHTZHUCUDZWEHWHBUEQUJZUBZVBZFWIHWNWHFUFZGSZ FUFZAFUFZWIFWNWPAFWNWPUCGSZAWNWOUCGWGWKWLWOUCTWJABCDEFGHIJKLMNOUGUHUIWNWC @@ -616596,7 +616596,7 @@ x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ) $= ( cfv cin csn dochexmidlem5 fveq2d chlt wcel wa wceq doch0 eqtrd ineq1d syl cdih crn cv co eqid lssss dochssv syl2anc dochcl eqeltrrd dihsmatrn wss eqeltrid dihrnlss clmod dvhlmod lsatlssel syl3anc eqsstrid dochoccl - lsmcl mpbid lsssssubg sseldd lsmub1 syl6sseqr dihoml4 sseqin2 3eqtr3rd + lsmcl mpbid lsssssubg sseldd lsmub1 sseqtrrdi dihoml4 sseqin2 3eqtr3rd csubg sylib ) AHMJULZJULZMAWPHUMZJULZHUMKHUMZWQHAWSKHAWSNUNZJULZKAWRXAJ ABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUKUOUPAGUQURLFURUSZXBKUTUDEFGJKLN PRQSUGVAVDVBVCADEFGJLMHPRTQUDUEAXCHLGVEULULZVFZURZHDURUDAHMOVGZCVHZXEUH @@ -616611,7 +616611,7 @@ x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ) $= NM, 15-Jan-2015.) $) dochexmidlem7 $p |- ( ph -> M =/= X ) $= ( cv wss wn wne co csubg cfv wcel clmod dvhlmod lsssssubg syl lsatlssel - sseldd lsmub2 syl2anc syl6sseqr chlt lssss dochlss lsmub1 sstr2 syl5com + sseldd lsmub2 syl2anc sseqtrrdi chlt lssss dochlss lsmub1 sstr2 syl5com wa mtod wceq sseq2 biimpcd necon3bd sylc ) AOULZHUMZWBMUMZUNHMUOAWBMWBC UPZHAMEUQURZUSZWBWFUSWBWEUMADWFMAEUTUSDWFUMAEFGLPRUDVAZDETVBVCZUEVEZADW FWBWIABDWBETUCWHUFVDVECMWBEUBVFVGUHVHAWDWBMMJURZCUPZUMZUKAMWLUMZWDWMAWG @@ -620547,7 +620547,7 @@ orthocomplement of its kernel (when its kernel is a closed hyperplane). $( Lemma for ~ mapdrval . (Contributed by NM, 2-Feb-2015.) $) mapdrvallem3 $p |- ( ph -> { f e. C | ( O ` ( L ` f ) ) C_ Q } = R ) $= - ( cfv wss crab mapdrvallem2 wcel ciun 2fveq3 ssiun2s adantl syl6sseqr + ( cfv wss crab mapdrvallem2 wcel ciun 2fveq3 ssiun2s adantl sseqtrrdi cv wa ssrabdv eqssd ) AJVMZPVCSVCZEVDZJCVEFABCDEFGHIJKLMNOPQRSTUAUBUC UDUEUFUGUHUIUJUKULUMUNUOUPUQURUSUTVAVBVFAVSJCFUPAVQFVGZVNVRLFLVMZPVCS VCZVHZEVTVRWCVDALFWBVQVRWAVQSPVIVJVKUQVLVOVP $. @@ -653098,7 +653098,7 @@ base set if and only if the neighborhoods (convergents) of every point ) $= ( vv cn0 wcel cfv cr c1 caddc co cfz cmap crrx cc0 cvv eqid cbs cv cfsupp k0004ss1 wbr crab ssidd wa wf elmapi adantl fzfid 0red fdmfifsupp ssrabdv - wceq ovex rrxbase ax-mp syl6sseqr sstrd ) EHIZEBJKLELMNZONZPNZVDQJZUAJZAB + wceq ovex rrxbase ax-mp sseqtrrdi sstrd ) EHIZEBJKLELMNZONZPNZVDQJZUAJZAB CDEFUDVBVEGUBZRUCUEZGVEUFZVGVBVIGVEVEVBVEUGVBVHVEIZUHZVDKVHKRVKVDKVHUIVBV HKVDUJUKVLLVCULVLUMUNUOVDSIVGVJUPLVCOUQVGGVFVDSVFTVGTURUSUTVA $. @@ -654337,7 +654337,7 @@ base set if and only if the neighborhoods (convergents) of every point 11-Aug-2023.) $) cpcolld $p |- ( ph -> E. y e. ( F Coll A ) x F y ) $= ( vz cv ccoll wcel wbr wa wex wrex cab cscott vex breq2 sylibr 19.8ad jca - elab ciun ssiun2 dfcoll2 syl6sseqr sselda elscottab adantl ex eximdv sylc + elab ciun ssiun2 dfcoll2 sseqtrrdi sselda elscottab adantl ex eximdv sylc scotteld df-rex ) ACIZDEJZKZBIZUPELZMZCNZUTCUQOAUSDKZUPUSHIZELZHPZQZKZCNV BFACVFAUPVFKZCAUTVIGVEUTHUPCRVDUPUSESZUCTUAUNVCVHVACVCVHVAVCVHMURUTVCVGUQ UPVCVGBDVGUDUQBDVGUEBHDEUFUGUHVHUTVCVEUTHCVJUIUJUBUKULUMUTCUQUOT $. @@ -655904,7 +655904,7 @@ collection and union ( ~ mnuop3d ), from which closure under pairing dvsconst $p |- ( ( S e. { RR , CC } /\ A e. CC ) -> ( S _D ( S X. { A } ) ) = ( S X. { 0 } ) ) $= ( cr cc cpr wcel wa csn cxp cres cdv co cc0 wss cdm wceq adantr xpssres syl - wf fconst6g anim2i recnprss c0ex fconst fdmi syl6sseqr dvconst adantl dmeqd + wf fconst6g anim2i recnprss c0ex fconst fdmi sseqtrrdi dvconst adantl dmeqd sseqtrrd ssid jctil dvres3 syl2anc oveq2d reseq1d eqtrd 3eqtr3d ) BCDEFZADF ZGZBDAHZIZBJZKLZDVDKLZBJZBBVCIZKLZBMHZIZVBUTDDVDTZGDDNZBVGOZNZGVFVHPVAVMUTD ADUAUBVBVPVNVBBDVKIZOZVOUTBVRNVAUTBDVRBUCZDVKVQDMUDUEUFUGQVBVGVQVAVGVQPUTAU @@ -655915,7 +655915,7 @@ collection and union ( ~ mnuop3d ), from which closure under pairing (Contributed by Steve Rodriguez, 11-Nov-2015.) $) dvsid $p |- ( S e. { RR , CC } -> ( S _D ( _I |` S ) ) = ( S X. { 1 } ) ) $= ( cr cc cpr wcel cid cres cdv co c1 csn cxp wf wa wss cdm wceq wfn crn dvid - fnresi rnresi eqimssi df-f mpbir2an jctr recnprss 1ex fconst fdmi syl6sseqr + fnresi rnresi eqimssi df-f mpbir2an jctr recnprss 1ex fconst fdmi sseqtrrdi dmeqi eqtri jctil dvres3 syl2anc resabs1d oveq2d reseq1i xpssres syl5eq syl ssid 3eqtr3d ) ABCDEZAFCGZAGZHIZCVFHIZAGZAFAGZHIAJKZLZVEVECCVFMZNCCOZAVIPZO ZNVHVJQVEVNVNVFCRVFSZCOCUAVRCCUBUCCCVFUDUEUFVEVQVOVEACVPAUGZVPCVLLZPCVIVTTU @@ -655926,7 +655926,7 @@ collection and union ( ~ mnuop3d ), from which closure under pairing (Contributed by Steve Rodriguez, 12-Nov-2015.) $) dvsef $p |- ( S e. { RR , CC } -> ( S _D ( exp |` S ) ) = ( exp |` S ) ) $= ( cr cc cpr wcel ce cres cdv co wf wa wss cdm wceq jctr recnprss dvef dmeqi - eff fdmi eqtri syl6sseqr ssid jctil dvres3 syl2anc reseq1i syl6eq ) ABCDEZA + eff fdmi eqtri sseqtrrdi ssid jctil dvres3 syl2anc reseq1i syl6eq ) ABCDEZA FAGZHIZCFHIZAGZUJUIUICCFJZKCCLZAULMZLZKUKUMNUIUNSOUIUQUOUIACUPAPUPFMCULFQRC CFSTUAUBCUCUDCAFUEUFULFAQUGUH $. @@ -666956,7 +666956,7 @@ unification theorem (e.g., the sub-theorem whose assertion is step 5 wn wi crest co cconn ex ralrimiv iunss biimpri biimpi simprd wrex simp-4r wo wex n0 inss2 sseldi eliun rexn0 exlimiv wnf nfan nfiu1 nfin nfne nfdif id nfv nfss nfbii mpbir simp-6l ralrimi r19.2z ancoms syl2anc sseldd elun - sylan sylbir simp-6r simp-5r simpllr simplr iunconnlem eqsstrid syl6sseqr + sylan sylbir simp-6r simp-5r simpllr simplr iunconnlem eqsstrid sseqtrrdi incom uncom pm4.56 idiALT pm2.65da ex3 3impd 3expia impd connsub biimp3ar ralrimivv syl3anc ) AIJUBUCPZHEFUDZJUEZDUFZXOUGZQUHZCUFZXOUGZQUHZXQXTUGZJ XOUIZUEZUJXOXQXTUKZUEZUMZUNZCIULDIULZIXOUOUPUQPZLAFJUEZHEULZXPAYLHEAHUFEP @@ -672932,7 +672932,7 @@ not even needed (it can be any class). (Contributed by Glauco $( Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) $) uzssd2 $p |- ( ph -> ( ZZ>= ` N ) C_ Z ) $= - ( cuz cfv syl6eleq uzssd syl6sseqr ) ACGHBGHZDABCACDLFEIJEK $. + ( cuz cfv syl6eleq uzssd sseqtrrdi ) ACGHBGHZDABCACDLFEIJEK $. $} ${ @@ -676214,7 +676214,7 @@ closed under the multiplication ( ' X ' ) of a finite number of adantr rpre adantl readdcld infrglb mpbid sselda adantlr ad2antlr ltsub1d syl3anc recnd ad2antrr pncand breq2d bitrd biimpd reximdva mpd wceq oveq1 cc breq1d rexrn biimpa syldan wi wf uztrn2 syl2an simpl simprr cfz fzssuz - ffvelrn uzss syl6sseqr eleq2s ad2antrl sstrid ralrimiva ssralv c1 fvoveq1 + ffvelrn uzss sseqtrrdi eleq2s ad2antrl sstrid ralrimiva ssralv c1 fvoveq1 sylc r19.21bi fveq2 breq12d sylan monoord2 lesub1dd resubcld lelttr mpand rspccva ltsub23 sseldd infrelb abssubge0d 3imtr4d anassrs ralrimdva fvexi cvv fex sylancl eqidd ffvelrnda clim2c ) ADDUBZNOUCZUDPCUEZDQZUUGUFRZUGQZ @@ -676299,7 +676299,7 @@ closed under the multiplication ( ' X ' ) of a finite number of climsuse $p |- ( ph -> G ~~> A ) $= ( vi vx vl vj vh cli wbr cc wcel cv cfv cmin co cabs clt wa cuz wral wrex cz crp climcl syl nfv cle cif simpllr wn ad4antr ifclda nfra1 simp-4l jca - nfan simpr wss anim1i adantr eluz mpbird simpll uzid 3syl syl6sseqr sseld + nfan simpr wss anim1i adantr eluz mpbird simpll uzid 3syl sseqtrrdi sseld wb uzss sylc wceq wi nfcv nffv nfeq weq eleq1 anbi2d fveq2 2fveq3 eqeq12d nfim imbi12d chvar eleq2i biimpi adantl c1 caddc fvoveq1 fvoveq1d eleq12d nfov nfel climsuselem1 sseldd syl6eleqr ex imdistani nfel1 eleq1d vtoclgf @@ -678147,7 +678147,7 @@ closed under the multiplication ( ' X ' ) of a finite number of $( A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021.) $) climresmpt $p |- ( ph -> ( G ~~> B <-> F ~~> B ) ) $= - ( cli wbr cuz wceq a1i wcel cvv cres cmpt reseq1i syl6eleq uzss syl6sseqr + ( cli wbr cuz wceq a1i wcel cvv cres cmpt reseq1i syl6eleq uzss sseqtrrdi cfv wss resmpt eqcomi 3eqtrrd breq1d cz wb eluzelz fvexi eqeltrid climres syl mptex syl2anc bitrd ) AFDNOEHPUGZUAZDNOZEDNOZAFVDDNAVDBICUBZVCUAZBVCC UBZFVDVHQAEVGVCKUCRAVCIUHVHVIQAVCGPUGZIAHVJSZVCVJUHAHIVJLJUDZGHUEUSJUFBIV @@ -678543,7 +678543,7 @@ closed under the multiplication ( ' X ' ) of a finite number of (Contributed by Glauco Siliprandi, 26-Jun-2021.) $) climleltrp $p |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( F ` k ) < ( C + X ) ) ) $= - ( wcel cuz cfv wss cv cr caddc co clt wbr wa wral wrex syl6eleq syl6sseqr + ( wcel cuz cfv wss cv cr caddc co clt wbr wa wral wrex syl6eleq sseqtrrdi uzss syl cc cmin cabs cz uzssz sseldi eqid eqidd clim2d nfv nfan ad2antlr simplll simpr sseldd adantr eqeltrd wceq cli climcl recnd eqcomd eqeltrrd pncan3d ad2antrr climreclf resubcld readdcld rpred leadd1dd subcld abscld @@ -689163,7 +689163,7 @@ represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, eqid biimpi r19.21bi sylan elrpd 3adant3 nfcri nfra1 nf3an rspa 3ad2antl3 simpl2 fvres syl 3brtr3d ex ralrimi wi spcegv mp2and simpl1 simprl simprr cif 3ad2ant1 difssd simp2 simp3 stoweidlem5 exlimddv wrex crest cuni ccmp - anbi12d ccld ctop wb cmptop elssuni syl6sseqr isopn2 syl2anc mpbid cmpcld + anbi12d ccld ctop wb cmptop elssuni sseqtrrdi isopn2 syl2anc mpbid cmpcld wss wne nffv cnrest df-ne restuni syl5rbbr biimpar evth2 nfov nfuni nfres neeq1d nfbr rexbii sylib raleqf rexeqbi1dv mpbird r19.29a pm2.61dan ) ADE UCZUDUEZHUFZUGRZUVAUHUISZUVABUFZCUJZTSZBUUSUKZULZHUMZAUUTUNZUHUOUPVHZUGRZ @@ -690543,7 +690543,7 @@ used to represent the final q_n in the paper (the one with n large ( T \ U ) C_ U. u ) ) $= ( vc cdif cuni wss cv cfn wcel w3a wex cfv cc0 wceq cle c1 wa wral nfrab1 wbr crab nfcxfr nfv ccn co syl6sseq cvv ccmp uniexg eqeltrid stoweidlem46 - syl cpw cin wrex crest ccld dfin4 elssuni syl6sseqr sseqin2 sylib syl5eqr + syl cpw cin wrex crest ccld dfin4 elssuni sseqtrrdi sseqin2 sylib syl5eqr wi eqeltrd wb cmptop difssd iscld2 syl2anc mpbird cmpcld cmpsub mpbid clt ctop ssrab2 eqsstri rabexd elpwg mpbiri unieq sseq2d pweq rexeqdv imbi12d ineq1d rspccva imp df-rex elinel2 ad2antrl elinel1 elpwid simprr 3jca mpd @@ -690682,7 +690682,7 @@ used to represent the final q_n in the paper (the one with n large A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) ) $= ( vy wcel wss wa cc0 cv cfv cle wbr c1 wral clt cmin co cdif w3a wrex crp c2 cdiv nfcv rpred rehalfcld rexrd ccn syl6sseq sseldd rfcnpre2 crab cuni - elssuni syl syl6sseqr 2re a1i rpgt0d 2pos divgt0d eqbrtrd nffv nfbr fveq2 + elssuni syl sseqtrrdi 2re a1i rpgt0d 2pos divgt0d eqbrtrd nffv nfbr fveq2 cr wceq breq1d elrabf sylanbrc syl6eleqr nfrab1 nfcxfr wn wf fcnre adantr rabeq2i biimpi adantl simpld ffvelrnd simprd halfpos mpbid lttrd ad2antrr wb anim1i eldif sylibr rsp sylc lensymd cmpt nfv nfan eqid sselda syl2anc @@ -690758,7 +690758,7 @@ used to represent the final q_n in the paper (the one with n large nfcxfr nfrab1 nfeq2 nfrex nfss nfdif nf3an nfre1 eqid cvv ccn ctop cmptop wa ccmp syl cioo crn ctg retop eqeltri cnfex syl6sseq ssexd adantr simpr1 sylancl simpr2 simpr3 c0 wne stoweidlem35 exlimddv cdiv cmul nfral simprl - csu simprrl simprrr caddc 3adant1r adantlr elssuni syl6sseqr stoweidlem44 + csu simprrl simprrr caddc 3adant1r adantlr elssuni sseqtrrdi stoweidlem44 nff cr sseldd ex exlimdvv mpd ) AUPUTZVAVBZVCUUAVDVEZGRUTZVOZVFDUTZUQUTUU DVGVGVHVIZUQUUCVJZDHIVKZVLZXBZXBZRVMUPVMZVFUUFSUTZVGZVNVIUUOVCVNVIXBDHVLP UUNVGVFVPVFUUOVHVIDUUIVLVQSEVJZAURUTZVRVBZUUQOVSZUUIUUQVTZVSZVQZUUMURABCU @@ -690824,7 +690824,7 @@ used to represent the final q_n in the paper (the one with n large A. t e. B ( 1 - E ) < ( x ` t ) ) ) $= ( cv wcel cc0 cfv cle wbr c1 wa wral clt cmin co w3a wex wrex cfz wf cdiv nfv cseq nfra1 nfan nfcv crab nfrab nfcxfr nff nfral cdif crp nfrab1 eqid - cn adantr simprl simpr rabeq2i simplbi cuni elssuni syl6sseqr 3syl r19.26 + cn adantr simprl simpr rabeq2i simplbi cuni elssuni sseqtrrdi 3syl r19.26 wss crn ad2antll r19.21bi simprbi cmul cmpt 3adant1r adantlr stoweidlem51 cr cvv c3 exlimdd df-rex sylibr ) ABVFZFVGVHEVFZYEVIZVJVKYGVLVJVKVMEJVNYG QVOVKEHVNVLQVPVQYGVOVKEGVNVRZVMBVSZYHBFVTAVLTWAVQZUCCVFZWBZYFPVFZYKVIVIZQ @@ -697408,7 +697408,7 @@ approximated is nonnegative (this assumption is removed in a later c0 cpr cun prid1g ne0d prfi cabs ccom cxp cid cdif cres ctg fourierdlem11 cinf cioo crest simp1d fourierdlem15 frn wfn elmapi ffn fzfid fnfi nnnn0d rnfi anbi1d anbi2d cbvrex2v anbi2i fourierdlem42 unfi hashnncl nnzd ltned - cbvrabv hashprg ssun1 syl6sseqr hashssle eluz2 syl3anbrc uz2m1nn iccssred + cbvrabv hashprg ssun1 sseqtrrdi hashssle eluz2 syl3anbrc uz2m1nn iccssred wf1o ssrab2 sstrid fourierdlem36 df-isom f1of fssd reex elmapg wfo df-f1o wf1 dffo3 simplr eqtrd ad2antrr eqeltrd eqled 3adantl2 rexrd ltled lbicc2 ovex wn syl3anc ubicc2 nnm1nn0 ffvelrnd 3ad2antl1 elfzelz elfzle1 ne0gt0d @@ -700148,7 +700148,7 @@ approximated is nonnegative (this assumption is removed in a later simp3r clt simplrd syl2an simpllr fveq1i fveq2i simprd r19.21bi eqbrtrrid rspa fourierdlem68 raleqdv eqcomi fvres fveq1d 3eqtr3a ralbidva rexlimdvv breq1d raleq 3ad2ant3 pm2.61dan pm3.22 elin eqcomd orcd dvbss fveq2 fvmpt - rexbiia dmmpti rexeqi syl21anc wfun funmpt olcd ralrimiva dfss3 syl6sseqr + rexbiia dmmpti rexeqi syl21anc wfun funmpt olcd ralrimiva dfss3 sseqtrrdi elunirn ssfiunibd ) ASUSRTIUTZVAEFGVBVCZPEVDZVEVCZLVFZHVGVCZVPVXGVPVHVCZV IVFZVJVCZVHVCZVKZVLVCZVMZVNZVOZJVQNUUDVCZJVDZIVFZVYAVRVEVCZIVFZVSVCZVKZUT ZVTZRVDZVAOVLVCZVFZWAVFZVYJVMZAVYHVXEVYMVNZVOZVYGVTZWJVXSVYOVYGVXRVYNVXQV @@ -713185,7 +713185,7 @@ nondecreasing measurable sets (with bounded measure) then the measure of Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.) $) meaiininclem $p |- ( ph -> S ~~> ( M ` |^|_ n e. Z ( E ` n ) ) ) $= - ( vm vx cv cfv ciin cli wbr cmpt cmin co cuz wcel cdif wceq wss syl6sseqr + ( vm vx cv cfv ciin cli wbr cmpt cmin co cuz wcel cdif wceq wss sseqtrrdi wa uzss syl adantr simpr sseldd cvv a1i cdm csalg eqid dmmeasal syl6eleqr ffvelrnda mpdan saldifcl2 syl3anc elexd fvmpt2d syldan cmea cr cfzo caddc fveq2d c1 simpl elfzouz adantl eleq1w anbi2d fvoveq1 fveq2 sseq12d chvarv @@ -714189,7 +714189,7 @@ This is the proof of the statement in the middle of Step (e) in the caratheodorylem2 $p |- ( ph -> ( O ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( O ` ( E ` n ) ) ) ) ) $= ( cn cfv wss wcel cvv c1 vx vm cv ciun cmpt csumge0 wral wa cdm cuni come - caragenss syl adantr ffvelrnda sseldd elssuni syl6sseqr ralrimiva omexrcl + caragenss syl adantr ffvelrnda sseldd elssuni sseqtrrdi ralrimiva omexrcl iunss sylibr nnex a1i cc0 cpnf cicc co omecl eqid fmptd sge0xrcl nfv nfcv nnuz cpw caragensspw fssd omeiunle cle wbr cres cfn wceq elpwinss resmptd cin fveq2d adantl cfz wrex 1zzd elinel2 uzfissfz w3a cxr ad2antrr fz1ssnn @@ -718334,7 +718334,7 @@ This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by rspa id ovex mptex fvmptd3 fveq1 ifbieq1d ifeq12d eqeltrd ifbieq12d fvexd mptexg ifexg eleq1 3adant2 iffalsed 3ad2ant3 3eqtrrd eqtr3d mnfxr iooltub ad5ant145 3adant1r ad4ant123 notbid adantlr adantllr neqne elicod ralrimi - nelsn syl21anc reximdva ralrimiva dfss3 2fveq3 ixpeq2dv iuneq2i syl6sseqr + nelsn syl21anc reximdva ralrimiva dfss3 2fveq3 ixpeq2dv iuneq2i sseqtrrdi mpd ovnlecvr2 fveq2i eldifi icossre sseldd hoidifhspval3 ad5ant134 simpl1 mpteq2ia breq2d 3ad2antl3 rexlimdva2 3syl ltnled r19.29a ad4antr ad4ant24 mnfltd eliood 3ad2antl1 eldifn condan ad5ant124 adantl4r oveq1d leadd12dd @@ -721297,7 +721297,7 @@ its dimensional volume (the product of its length in each dimension, 26-Jun-2021.) $) mbfresmf $p |- ( ph -> F e. ( SMblFn ` S ) ) $= ( vx va cdm csalg wceq a1i wcel dmvolsal eqeltrd cr cuni wss adantr cvv - nfv cvol cmbf mbfdmssre syl unieqi unidmvol eqtri syl6sseqr wfn crn wa wf + nfv cvol cmbf mbfdmssre syl unieqi unidmvol eqtri sseqtrrdi wfn crn wa wf cc mbff ffn 3syl jca df-f sylibr cv cfv clt wbr crab ccnv cmnf cioo crest co cima cxr adantl preimaioomnf eqcomd elexi eqeltri dmexd mbfima syl2anc rexr eleqtrrd cin cnvimass dfss biimpi ax-mp elrestd issmfd ) AGCIZBCHAHU @@ -721747,7 +721747,7 @@ but it is not a measurable functions ( w.r.t. to ~ df-mbf ). (Contributed by Glauco Siliprandi, 26-Jun-2021.) $) smfmbfcex $p |- ( ph -> ( F e. ( SMblFn ` S ) /\ -. F e. MblFn ) ) $= ( csmblfn cfv wcel wn cc0 csalg cdm a1i cr cuni 0red nfv dmvolsal eqeltri - cmbf cvol unieqi unidmvol eqtri syl6sseqr smfconst cv wa fdmd wceq eqcomi + cmbf cvol unieqi unidmvol eqtri sseqtrrdi smfconst cv wa fdmd wceq eqcomi fmptd eleq12d notbid mpbird mbfdm con3i syl jca ) ADCJKLDUDLZMZABENCDABUA COLACUEPZOFUBUCQAERCSZGVGVFSRCVFFUFUGUHUIATIUJADPZVFLZMZVEAVJECLZMHAVIVKA VHEVFCAERDABENRDABUKELULTIUPUMVFCUNACVFFUOQUQURUSVDVIDUTVAVBVC $. @@ -722123,7 +722123,7 @@ but it is not a measurable functions ( w.r.t. to ~ df-mbf ). cuz ssrab2f a1i wi wral wa cn co wrex c1 caddc clt simpllr ssrab2 eqsstri cdiv sseli wceq fveq2 iineq1d cbviunv eleq2i eliun bitri sylib syl cr nfv nfan nfcv nfii1 nfel nfmpt1 eqid uzssz biimpi sseldi uzid ad2antlr simpld - cz simplll uzss syl6sseqr sselda ad4ant24 adantll w3a fvexd 3adant3 csalg + cz simplll uzss sseqtrrdi sselda ad4ant24 adantll w3a fvexd 3adant3 csalg adantr simp3 syl3anc adantl3r sylibr eqcomd simplr uztrn2 simpll2 syl2anc cvv simpr id ex syl31anc reximdva mpd cin ralrimivw eleq12d ovmpt4g eliin wb ax-mp ralrimiva eliinid eqidd fvmpt2d wf csmblfn smff ffvelrnd eqeltrd @@ -723897,7 +723897,7 @@ that every function in the sequence can have a different (partial) (Contributed by Glauco Siliprandi, 23-Oct-2021.) $) smflimsuplem2 $p |- ( ph -> X e. dom ( H ` n ) ) $= ( vy cv cuz cfv cmpt crn cxr clt csup cr wcel cdm ciin crab cle wral wrex - wa wbr eqid wf wss syl6eleq uzss syl syl6sseqr adantr simpr csalg csmblfn + wa wbr eqid wf wss syl6eleq uzss syl sseqtrrdi adantr simpr csalg csmblfn sseldd ffvelrnda smff syldan iinss2 adantl ffvelrnd clsp nfmpt1 cz fmptdf cpnf eluzelz ffnd cvv nfcv fvexd mptfnd a1i fvmpt2d fvmpt2 syl2anc eqtr4d limsupequz eqcomi mpteq1i fveq2i eqtrd renepnfd eqnetrd limsupubuzmpt wne @@ -723947,7 +723947,7 @@ that every function in the sequence can have a different (partial) wa w3a csmblfn cr csalg adantr crn cxr csup cres wceq eqid eluzelz2 uzn0d clt rgenw iinexd adantl rabexd fvmpt2d fvres eqcomd dmeqd iineq2dv eleq2d wral fveq1d mpteq2ia rneqi supeq1i anbi12d rabbidva2 eqtrd mpteq12dv nfcv - eleq1d cz wss eleq2i biimpi uzss syl6sseqr fssresd smfsupxr eqeltrd fmptd + eleq1d cz wss eleq2i biimpi uzss sseqtrrdi fssresd smfsupxr eqeltrd fmptd wf syl ffvelrnda smff feqmptd smflimmpt ) ABFUAZIRZUBZBUAZXGRZFKXJSZUCUBT BDKFDUAUDRXHUEUFUGZCFDBXLXKUCRSZJUHUHKAFUIABUIADUILMXHUHTAXFKTZUNZXGXFIUJ UKULAXNXIXHTUOXIXGUMNXOBXHXJSZXGCUPRZXOXGXPXOBXHUQXGXOXHCXGACURTXNNUSZAKX @@ -724045,7 +724045,7 @@ that every function in the sequence can have a different (partial) smflimsuplem5 $p |- ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` X ) ) ~~> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` X ) ) ) ) $= ( vy cuz cfv cv cmpt crn cxr clt csup clsp cli wcel wa wceq eleq2i biimpi - cvv wss uzss syl syl6sseqr sselda cr cdm ciin crab nfcv nfrab1 nfmpt nffv + cvv wss uzss syl sseqtrrdi sselda cr cdm ciin crab nfcv nfrab1 nfmpt nffv nfcxfr fvex mptexf a1i fvmpt2 syl2anc fveq1d fveq2 mpteq2dv rneqd supeq1d cbvmptf simpl fveq2d mpteq2dva eleq1d iinss1 adantl adantr sseldd cle wbr wral wrex nfv nfan eqid simpll adantll csalg csmblfn ffvelrnda smff eliin @@ -724100,7 +724100,7 @@ that every function in the sequence can have a different (partial) smflimsuplem6 $p |- ( ph -> ( n e. Z |-> ( ( H ` n ) ` X ) ) e. dom ~~> ) $= ( cv cfv cmpt cvv wcel cuz clsp cli wbr cdm fvexi a1i fvexd smflimsuplem5 - mptexd cz eluzelz2 syl eqid wss eleq2i biimpi uzss syl6sseqr wa climeqmpt + mptexd cz eluzelz2 syl eqid wss eleq2i biimpi uzss sseqtrrdi wa climeqmpt ssid mpbird breldmg syl3anc ) AELKEUDZHUEZUEZUFZUGUHDJUIUEZKDUDGUEUEUFZUJ UEZUGUHVQVTUKULZVQUKUMUHAELVPUGLUGUHALIUIPUNUOZURAVSUJUPAWAEVRVPUFVTUKULA BCDEFGHIJKLMNOPQRSTUAUBUCUQAELVRVPVTUGJUGUGVRMWBAJUIUPAJLUHZJUSUHUBIJLPUT @@ -737922,7 +737922,7 @@ an isomorphism in the category of graphs (something like "GraphIsom ( vc vd ve wf cv cfv wceq wi wral isomuspgrlem2b wcel wa isomuspgrlem2a wf1 cima wb syl imaeq2 fveq2 eqeq12d rspcv ad2antrl imp eqcomd ad2antll mpidan wss wf1o f1of1 cuspgr cupgr uspgrupgr cuhgr upgruhgr cedg eleq2i - cvtx cpw edguhgr elpwi syl6sseqr ex syl5bi anim12d 3syl syl2an2r biimpd + cvtx cpw edguhgr elpwi sseqtrrdi ex syl5bi anim12d 3syl syl2an2r biimpd f1imaeq sylbid ralrimivva dff13 sylanbrc ) AEHGUFUCUGZGUHZUDUGZGUHZUIZW OWQUIZUJZUDEUKUCEUKEHGUPABCDEFGHIJLMNOPQRSTUAULAXAUCUDEEAWOEUMZWQEUMZUN ZUNZWSFWOUQZFWQUQZUIZWTAXDFUEUGZUQZXIGUHZUIZUEEUKZWSXHURAFKUMXMUBBCDUEE @@ -738386,7 +738386,7 @@ it allows only walks consisting of not proper hyperedges (i.e. edges upgredgssspr $p |- ( G e. UPGraph -> ( Edg ` G ) C_ ( Pairs ` ( Vtx ` G ) ) ) $= ( vp cupgr wcel cedg cfv cv chash c2 cle wbr cvtx cpw cdif crab upgredgss - c0 csn cspr cvv wceq fvex sprvalpwle2 ax-mp syl6sseqr ) ACDAEFBGHFIJKBALF + c0 csn cspr cvv wceq fvex sprvalpwle2 ax-mp sseqtrrdi ) ACDAEFBGHFIJKBALF ZMQRNOZUFSFZBAPUFTDUHUGUAALUBUFTBUCUDUE $. $} @@ -752986,7 +752986,7 @@ being careful about the above problem for some F (for example z = ( vw vy vz vx va cfv cv wss wi wal wcel wa nfv cab cuni eqid wex csetrecs sseld imp df-setrecs eqtri syl6eleq eluni sylib ralrimiva setrec1lem3 cun nfaba1 nfel2 nfan cvv adantr simprl simprr setrec1lem4 ssun2 syl exlimddv - jctil ssuni syl6sseqr ) ABDMZHNZINZOVKJNZOVKDMVMOPPHQVLVMOPZJQIUAZUBZCABK + jctil ssuni sseqtrrdi ) ABDMZHNZINZOVKJNZOVKDMVMOPPHQVLVMOPZJQIUAZUBZCABK NZOZVQVORZSZVJVPOZKAKIJHBDVOLVOUCZFALNZVQRVSSKUDZLBAWCBRZSZWCVPRWDWFWCCVP AWEWCCRABCWCGUFUGCDUEVPEIJHDUHUIZUJKWCVOUKULUMUNAVTSZVJVQVJUOZOZWIVORZSWA WHWKWJWHIJHBDVQVOAVTJAJTVRVSJVRJTJVQVOVNJIUPUQURURWBABUSRVTFUTAVRVSVAAVRV @@ -753181,7 +753181,7 @@ the relevant induction theorem (such as ~ tfi ) to the other class. 14-Mar-2022.) $) setrecsres $p |- ( ph -> B = setrecs ( ( F |` ~P B ) ) ) $= ( vx cpw cres csetrecs cv wss cfv wi wa wceq id resss a1i setrecsss wcel - syl6sseqr sylan9ssr velpw sylbir syl eqid cvv vex setrec1 adantl eqsstrrd + sseqtrrdi sylan9ssr velpw sylbir syl eqid cvv vex setrec1 adantl eqsstrrd fvres ex alrimiv setrec2v eqssd ) ABCBGZHZIZABUSCFDAFJZUSKZUTCLZUSKZMFAVA VCAVANZVBUTURLZUSVDUTBKZVEVBOZVAAUTUSBVAPZAUSCIBAURCEURCKACUQQRSDUAZUBVFU TUQTVGFBUCUTUQCULUDUEVAVEUSKAVAUTUSURUSUFUTUGTVAFUHRVHUIUJUKUMUNUOVIUP $. @@ -754831,7 +754831,7 @@ to Davis and Putnam (1960). (Contributed by David A. Wheeler, fvmpt2 sylan9eq fvconst2 eqeq12d ralbidva bitrd cdm cnzr drngnzr islindf3 imbi1d dmmpti f1eq2 anbi1i bitri wnel con34b df-nel xchbinx imbi1i bitr4i velsn ralbii raldifb ralnex 3bitri 3bitr3g clss cmri cuvc cpw cmre lssmre - clspn cmrc mrclsp clvec islvec mpbir2an cacs lssacsex frnd dif0 syl6sseqr + clspn cmrc mrclsp clvec islvec mpbir2an cacs lssacsex frnd dif0 sseqtrrdi simprd uvcff frn sseqtrri fveq2i clbs lbssp eqtri pm3.2i lindsind2 mp3an1 frlmlbs ralrimiva ismri2 sylancr biimpar eqeltrid wo mptfi rnfi mp2b orci mreexexd elpwi ssdomg mpsyl endomtr f1f1orn f1oen uvcendim ensymi domentr