From aabf1e5836e5f8f3b47f60ae1cfc14bf61d53a6e Mon Sep 17 00:00:00 2001 From: Scott Fenton Date: Sat, 11 Jan 2025 20:35:05 -0500 Subject: [PATCH] moved surreal ordering and dependencies to main set.mm --- set.mm | 492 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 243 insertions(+), 249 deletions(-) diff --git a/set.mm b/set.mm index 90c38330a..8c73c05bb 100644 --- a/set.mm +++ b/set.mm @@ -11559,6 +11559,21 @@ This definition (in the form of ~ dfifp2 ) appears in Section II.24 of 3orel3 $p |- ( -. ch -> ( ( ph \/ ps \/ ch ) -> ( ph \/ ps ) ) ) $= ( w3o wo wn df-3or orel2 biimtrid ) ABCDABEZCECFJABCGCJHI $. + $( Elimination of two disjuncts in a triple disjunction. (Contributed by + Scott Fenton, 9-Jun-2011.) $) + 3orel13 $p |- ( ( -. ph /\ -. ch ) -> ( ( ph \/ ps \/ ch ) -> ps ) ) $= + ( wn w3o wo 3orel3 orel1 sylan9r ) CDABCEABFADBABCGABHI $. + + ${ + 3pm3.2ni.1 $e |- -. ph $. + 3pm3.2ni.2 $e |- -. ps $. + 3pm3.2ni.3 $e |- -. ch $. + $( Triple negated disjunction introduction. (Contributed by Scott Fenton, + 20-Apr-2011.) $) + 3pm3.2ni $p |- -. ( ph \/ ps \/ ch ) $= + ( w3o wo pm3.2ni df-3or mtbir ) ABCGABHZCHLCABDEIFIABCJK $. + $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Logical "nand" (Sheffer stroke) @@ -75688,6 +75703,20 @@ be a set (so instead it is a proper class). Here we prove the denial of CUMVJCDVRVLUNCBUOACVJUPUQURVBUSBCUTVA $. $} + ${ + $d ph y z $. $d x y z $. + $( A closed form of ~ tfis . (Contributed by Scott Fenton, 8-Jun-2011.) $) + tfisg $p |- ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> + A. x e. On ph ) $= + ( vz cv wsbc wral wi con0 crab wceq wss wcel ssrab2 wa dfss3 nfcv elrabsf + simprbi nfsbc1v ralimi sylbi nfralw nfim sbceq1a imbi12d rspc impcom syl5 + raleq simpr jctild syl6ibr ralrimiva tfi sylancr eqcomd rabid2 sylib ) AB + CEZFZCBEZGZAHZBIGZIABIJZKABIGVEVFIVEVFILDEZVFLZVGVFMZHZDIGVFIKABINVEVJDIV + EVGIMZOZVHVKABVGFZOVIVLVHVMVKVHVACVGGZVLVMVHUTVFMZCVGGVNCVGVFPVOVACVGVOUT + IMVAABUTIBIQZRSUAUBVKVEVNVMHZVDVQBVGIVNVMBVABCVGBVGQABUTTUCABVGTUDVBVGKVC + VNAVMVACVBVGUJABVGUEUFUGUHUIVEVKUKULABVGIVPRUMUNDVFUOUPUQABIURUS $. + $} + ${ $d w y z ph $. $d w x y z $. tfis.1 $e |- ( x e. On -> ( A. y e. x [ y / x ] ph -> ph ) ) $. @@ -75957,7 +75986,6 @@ last three are the basis and the induction hypotheses (for successor and UCFCDOUDULHUMUEFCHUMUEZQUMUFZUKFCHUMUGUPFUOAPUDUHUI $. $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The natural numbers (i.e., finite ordinals) @@ -79594,6 +79622,175 @@ Power Set ( ~ ax-pow ). (Contributed by Mario Carneiro, 20-May-2013.) $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Ordering Ordinal Sequences +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + $d A f x $. $d G f x $. $d X x $. + orderseqlem.1 $e |- F = { f | E. x e. On f : x --> A } $. + $( Lemma for ~ poseq and ~ soseq . The function value of a sequene is + either in ` A ` or null. (Contributed by Scott Fenton, 8-Jun-2011.) $) + orderseqlem $p |- ( G e. F -> ( G ` X ) e. ( A u. { (/) } ) ) $= + ( wcel cv wf con0 wrex cfv c0 csn cun wceq feq1 wss syl rexbidv ibi unss1 + elab2g crn frn fvrn0 ssel mpisyl rexlimivw ) EDHZAIZBEJZAKLZFEMZBNOZPZHZU + KUNULBCIZJZAKLUNCEDDUSEQUTUMAKULBUSERUAGUDUBUMURAKUMEUEZUPPZUQSZUOVBHURUM + VABSVCULBEUFVABUPUCTEFUGVBUQUOUHUIUJT $. + $} + + ${ + $d A b f x $. $d a b c f g t w x y z $. $d F a b c f g t w x z $. + $d R f g t w x z $. $d S a b c $. + poseq.1 $e |- R Po ( A u. { (/) } ) $. + poseq.2 $e |- F = { f | E. x e. On f : x --> A } $. + poseq.3 $e |- S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ + E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ + ( f ` x ) R ( g ` x ) ) ) } $. + $( A partial ordering of sequences of ordinals. (Contributed by Scott + Fenton, 8-Jun-2011.) $) + poseq $p |- S Po F $= + ( vz vw wbr wa wral cfv con0 wrex anbi12d va vb vc vt wpo cv wn wcel wceq + wi w3a c0 csn cun cab feq2 cbvrexvw abbii eqtri orderseqlem poirr sylancr + wf intnand adantr nrexdv imnan vex weq eleq1w anbi1d fveq1 eqeq1d ralbidv + mpbi breq1d rexbidv anbi2d eqeq2d breq2d mtbir raleq fveq2 breq12d bitrid + brab simplll simplrr an4 2rexbii reeanv bitri word eloni ordtri3or syl2an + wel w3o simp1l wss onelss imp adantll ssralv anim2d r19.26 syl6ibr ralimi + eqtr syl adantrd 3impia eqeq12d rspcv breq2 biimpd com3l ad2ant2lr impcom + syl6 3adant1 rspcev syl12anc 3exp ad2antrr ad2antlr ad2antll 3jca anim12i + potr anassrs sylan2 exp32 imbi1d syl5ibcom simp1r adantlr anim1d sylbir + a1d breq1 biimprd ad2ant2rl 3jaod mpd rexlimivv jca31 an4s syl2anb sylibr + pm3.2i a1i rgen3 df-po mpbir ) HEUEUAUFZUUPENZUGZUUPUBUFZENZUUSUCUFZENZOZ + UUPUVAENZUJZOZUCHPUBHPUAHPUVFUAUBUCHHHUVFUUPHUHZUUSHUHZUVAHUHZUKUURUVEUUQ + UVGUVGOZBUFZUUPQZUVLUIZBAUFZPZUVNUUPQZUVPDNZOZARSZOZUVJUVSUGZUJUVTUGUVGUW + AUVGUVGUVRARUVGUVRUGUVNRUHUVGUVQUVOUVGCULUMUNZDUEZUVPUWBUHUVQUGIUBCFHUUPU + VNHUVNCFUFZVCZARSZFUOUUSCUWDVCZUBRSZFUOJUWFUWHFUWEUWGAUBRUVNUUSCUWDUPUQUR + USUTUWBUVPDVAVBVDVEVFVEUVJUVSVGVOUWDHUHZGUFZHUHZOZUVKUWDQZUVKUWJQZUIZBUVN + PZUVNUWDQZUVNUWJQZDNZOZARSZOZUVGUWKOZUVLUWNUIZBUVNPZUVPUWRDNZOZARSZOUVTFG + UUPUUPEUAVHZUXIFUAVIZUWLUXCUXAUXHUXJUWIUVGUWKFUAHVJVKZUXJUWTUXGARUXJUWPUX + EUWSUXFUXJUWOUXDBUVNUXJUWMUVLUWNUVKUWDUUPVLVMZVNUXJUWQUVPUWRDUVNUWDUUPVLV + PTVQTGUAVIZUXCUVJUXHUVSUXMUWKUVGUVGGUAHVJVRUXMUXGUVRARUXMUXEUVOUXFUVQUXMU + XDUVMBUVNUXMUWNUVLUVLUVKUWJUUPVLVSVNUXMUWRUVPUVPDUVNUWJUUPVLVTTVQTKWFWAUV + CUVGUVIOZUVLUVKUVAQZUIZBUDUFZPZUXQUUPQZUXQUVAQZDNZOZUDRSZOZUVDUUTUVGUVHOZ + UVLUVKUUSQZUIZBLUFZPZUYHUUPQZUYHUUSQZDNZOZLRSZOZUVHUVIOZUYFUXOUIZBMUFZPZU + YRUUSQZUYRUVAQZDNZOZMRSZOZUYDUVBUXBUXCUXDBUYHPZUYJUYHUWJQZDNZOZLRSZOUYOFG + UUPUUSEUXIUBVHZUXJUWLUXCUXAVUJUXKUXAUWOBUYHPZUYHUWDQZVUGDNZOZLRSUXJVUJUWT + VUOALRALVIZUWPVULUWSVUNUWOBUVNUYHWBVUPUWQVUMUWRVUGDUVNUYHUWDWCUVNUYHUWJWC + WDTUQUXJVUOVUILRUXJVULVUFVUNVUHUXJUWOUXDBUYHUXLVNUXJVUMUYJVUGDUYHUWDUUPVL + VPTVQWETGUBVIZUXCUYEVUJUYNVUQUWKUVHUVGGUBHVJVRVUQVUIUYMLRVUQVUFUYIVUHUYLV + UQUXDUYGBUYHVUQUWNUYFUVLUVKUWJUUSVLVSVNVUQVUGUYKUYJDUYHUWJUUSVLVTTVQTKWFU + XBUVHUWKOZUYFUWNUIZBUYRPZUYTUYRUWJQZDNZOZMRSZOVUEFGUUSUVAEVUKUCVHZFUBVIZU + WLVURUXAVVDVVFUWIUVHUWKFUBHVJVKUXAUWOBUYRPZUYRUWDQZVVADNZOZMRSVVFVVDUWTVV + JAMRAMVIZUWPVVGUWSVVIUWOBUVNUYRWBVVKUWQVVHUWRVVADUVNUYRUWDWCUVNUYRUWJWCWD + TUQVVFVVJVVCMRVVFVVGVUTVVIVVBVVFUWOVUSBUYRVVFUWMUYFUWNUVKUWDUUSVLVMVNVVFV + VHUYTVVADUYRUWDUUSVLVPTVQWETGUCVIZVURUYPVVDVUDVVLUWKUVIUVHGUCHVJZVRVVLVVC + VUCMRVVLVUTUYSVVBVUBVVLVUSUYQBUYRVVLUWNUXOUYFUVKUWJUVAVLZVSVNVVLVVAVUAUYT + DUYRUWJUVAVLVTTVQTKWFUYEUYPUYNVUDUYDUYEUYPOZUYNVUDOZOUVGUVIUYCUVGUVHUYPVV + PWGUYEUVHUVIVVPWHVVPVVOUYCVVPUYIUYSOZUYLVUBOZOZMRSLRSZVVOUYCUJZVVTUYMVUCO + ZMRSLRSVVPVVSVWBLMRRUYIUYSUYLVUBWIWJUYMVUCLMRRWKWLVVSVWALMRRUYHRUHZUYRRUH + ZOZLMWQZLMVIZMLWQZWRZVVSVWAUJZVWCUYHWMUYRWMVWIVWDUYHWNUYRWNUYHUYRWOWPVWEV + WFVWJVWGVWHVWEVWFVVSVWAVWEVWFVVSUKZUYCVVOVWKVWCUXPBUYHPZUYJUYHUVAQZDNZUYC + VWCVWDVWFVVSWSVWEVWFVVSVWLVWEVWFOZVVQVWLVVRVWOUYHUYRWTZVVQVWLUJVWDVWFVWPV + WCVWDVWFVWPUYRUYHXAXBXCVWPVVQUYGUYQOZBUYHPZVWLVWPVVQUYIUYQBUYHPZOZVWRVWPU + YSVWSUYIUYQBUYHUYRXDXEUYGUYQBUYHXFZXGVWQUXPBUYHUVLUYFUXOXIZXHZXTXJXKXLVWF + VVSVWNVWEVVSVWFVWNUYSUYLVWFVWNUJZUYIVUBUYSUYLVXDVWFUYSUYLVWNVWFUYSUYKVWMU + IZUYLVWNUJUYQVXEBUYHUYRBLVIUYFUYKUXOVWMUVKUYHUUSWCUVKUYHUVAWCXMXNVXEUYLVW + NUYKVWMUYJDXOXPXTXQXBXRXSYAUYBVWLVWNOZUDUYHRUDLVIZUXRVWLUYAVWNUXPBUXQUYHW + BVXGUXSUYJUXTVWMDUXQUYHUUPWCUXQUYHUVAWCWDTYBZYCYTYDVWCVWGVWJUJVWDVWCVWRUY + LUYKVWMDNZOZOZVWAUJVWGVWJVWCVXKVVOUYCVXKVVOOVWCVXFUYCVWRVXJVVOVXFVWRVWLVX + JVVOOVWNVXCVVOVXJVWNVVOUWCUYJUWBUHZUYKUWBUHZVWMUWBUHZUKVXJVWNUJIVVOVXLVXM + VXNUVGVXLUVHUYPACFHUUPUYHJUTYEUVHVXMUVGUYPACFHUUSUYHJUTYFUVIVXNUYEUVHACFH + UVAUYHJUTYGYHUWBUYJUYKVWMDYJVBXSYIYKVXHYLYMVWGVXKVVSVWAVWGVWRVVQVXJVVRVWR + VWTVWGVVQVXAVWGVWSUYSUYIUYQBUYHUYRWBVRWEVWGVXIVUBUYLVWGUYKUYTVWMVUADUYHUY + RUUSWCUYHUYRUVAWCWDVRTYNYOVEVWEVWHVVSVWAVWEVWHVVSUKZUYCVVOVXOVWDUXPBUYRPZ + UYRUUPQZVUADNZUYCVWCVWDVWHVVSYPVWEVWHVVSVXPVWEVWHOUYRUYHWTZVVSVXPUJVWCVWH + VXSVWDVWCVWHVXSUYHUYRXAXBYQVXSVVQVXPVVRVXSVVQUYGBUYRPZUYSOZVXPVXSUYIVXTUY + SUYGBUYRUYHXDYRVYAVWQBUYRPVXPUYGUYQBUYRXFVWQUXPBUYRVXBXHYSXTXKXJXLVWHVVSV + XRVWEVVSVWHVXRUYIVUBVWHVXRUJZUYSUYLUYIVUBVYBVWHUYIVUBVXRVWHUYIVXQUYTUIZVU + BVXRUJUYGVYCBUYRUYHBMVIUVLVXQUYFUYTUVKUYRUUPWCUVKUYRUUSWCXMXNVYCVXRVUBVXQ + UYTVUADUUAUUBXTXQXBUUCXSYAUYBVXPVXROUDUYRRUDMVIZUXRVXPUYAVXRUXPBUXQUYRWBV + YDUXSVXQUXTVUADUXQUYRUUPWCUXQUYRUVAWCWDTYBYCYTYDUUDUUEUUFYSXSUUGUUHUUIUXB + UXCUXDBUXQPZUXSUXQUWJQZDNZOZUDRSZOUYDFGUUPUVAEUXIVVEUXJUWLUXCUXAVYIUXKUXA + UWOBUXQPZUXQUWDQZVYFDNZOZUDRSUXJVYIUWTVYMAUDRAUDVIZUWPVYJUWSVYLUWOBUVNUXQ + WBVYNUWQVYKUWRVYFDUVNUXQUWDWCUVNUXQUWJWCWDTUQUXJVYMVYHUDRUXJVYJVYEVYLVYGU + XJUWOUXDBUXQUXLVNUXJVYKUXSVYFDUXQUWDUUPVLVPTVQWETVVLUXCUXNVYIUYCVVLUWKUVI + UVGVVMVRVVLVYHUYBUDRVVLVYEUXRVYGUYAVVLUXDUXPBUXQVVLUWNUXOUVLVVNVSVNVVLVYF + UXTUXSDUXQUWJUVAVLVTTVQTKWFUUJUUKUULUUMUAUBUCHEUUNUUO $. + $} + + ${ + $d a b p q y $. $d A f p q x $. $d A y $. $d F a b f g x $. + $d f g x y $. $d R f g x $. $d S a b $. + soseq.1 $e |- R Or ( A u. { (/) } ) $. + soseq.2 $e |- F = { f | E. x e. On f : x --> A } $. + soseq.3 $e |- S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ + E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ + ( f ` x ) R ( g ` x ) ) ) } $. + soseq.4 $e |- -. (/) e. A $. + $( A linear ordering of sequences of ordinals. (Contributed by Scott + Fenton, 8-Jun-2011.) $) + soseq $p |- S Or F $= + ( wral wcel wa cfv wceq con0 wrex wi va vb vp wor wpo wbr weq w3o csn cun + vq cv c0 sopo ax-mp poseq wo wn eleq1w anbi1d fveq1 eqeq1d ralbidv breq1d + anbi12d rexbidv anbi2d eqeq2d breq2d brabg bianabs ancoms notbid ralinexa + wb orbi12d andi eqcom ralbii anbi1i orbi2i bitri rexbii r19.43 xchbinx wf + cab feq2 cbvrexvw abbii eqtri orderseqlem sotrieq mpan syl2an imbi2d wsbc + vex fveq2 eqeq12d sbcie imbi1i tfisg sylbir feq1 elab2 anbi12i reeanv wss + bitr4i onss ssralv syl ad2antlr rspcv a1i ffvelcdm cdm eloni ordirr eleq2 + fdm word biimparc sylan ndmfv eleq1 ex com23 sylan2 exp4b imp32 syldd imp + syl5 mtoi syld jcad wfn ffn eqtr2 biimprd 3syl adantlr eqtr biimpd expcom + ad2antrr adantll ordtri3or adantr 3orel13 syl6ci eqfnfv2 adantl rexlimivv + sylibrd sylbi sylbird syl5bir sylbid orrd df-3or bitr2i sylib rgen2 df-so + 3orcomb mpbir2an ) HEUDHEUEUAULZUBULZEUFZUAUBUGZUVKUVJEUFZUHZUBHMUAHMABCD + EFGHCUMUIUJZDUDZUVPDUEIUVPDUNUOJKUPUVOUAUBHHUVJHNZUVKHNZOZUVLUVNUQZUVMUQZ + UVOUVTUWAUVMUVTUWAURBULZUVJPZUWCUVKPZQZBAULZMZUWGUVJPZUWGUVKPZDUFZOZARSZU + WEUWDQZBUWGMZUWJUWIDUFZOZARSZUQZURZUVMUVTUWAUWSUVTUVLUWMUVNUWRUVTUVLUWMFU + LZHNZGULZHNZOZUWCUXAPZUWCUXCPZQZBUWGMZUWGUXAPZUWGUXCPZDUFZOZARSZOZUVRUXDO + ZUWDUXGQZBUWGMZUWIUXKDUFZOZARSZOUVTUWMOFGUVJUVKHHEFUAUGZUXEUXPUXNUYAUYBUX + BUVRUXDFUAHUSUTUYBUXMUXTARUYBUXIUXRUXLUXSUYBUXHUXQBUWGUYBUXFUWDUXGUWCUXAU + VJVAVBVCUYBUXJUWIUXKDUWGUXAUVJVAVDVEVFVEGUBUGZUXPUVTUYAUWMUYCUXDUVSUVRGUB + HUSVGUYCUXTUWLARUYCUXRUWHUXSUWKUYCUXQUWFBUWGUYCUXGUWEUWDUWCUXCUVKVAVHVCUY + CUXKUWJUWIDUWGUXCUVKVAVIVEVFVEKVJVKUVSUVRUVNUWRVOUVSUVROZUVNUWRUXOUVSUXDO + ZUWEUXGQZBUWGMZUWJUXKDUFZOZARSZOUYDUWROFGUVKUVJHHEFUBUGZUXEUYEUXNUYJUYKUX + BUVSUXDFUBHUSUTUYKUXMUYIARUYKUXIUYGUXLUYHUYKUXHUYFBUWGUYKUXFUWEUXGUWCUXAU + VKVAVBVCUYKUXJUWJUXKDUWGUXAUVKVAVDVEVFVEGUAUGZUYEUYDUYJUWRUYLUXDUVRUVSGUA + HUSVGUYLUYIUWQARUYLUYGUWOUYHUWPUYLUYFUWNBUWGUYLUXGUWDUWEUWCUXCUVJVAVHVCUY + LUXKUWIUWJDUWGUXCUVJVAVIVEVFVEKVJVKVLVPVMUWTUWHUWKUWPUQZURZTZARMZUVTUVMUY + PUWHUYMOZARSZUWSUWHUYMARVNUYRUWLUWQUQZARSUWSUYQUYSARUYQUWLUWHUWPOZUQUYSUW + HUWKUWPVQUYTUWQUWLUWHUWOUWPUWFUWNBUWGUWDUWEVRVSVTWAWBWCUWLUWQARWDWBWEUVTU + YPUWHUWIUWJQZTZARMZUVMUVTVUBUYOARUVTVUAUYNUWHUVRUWIUVPNZUWJUVPNZVUAUYNVOZ + UVSBCFHUVJUWGHUWGCUXAWFZARSZFWGUWCCUXAWFZBRSZFWGJVUHVUJFVUGVUIABRUWGUWCCU + XAWHWIWJWKZWLBCFHUVKUWGVUKWLUVQVUDVUEOVUFIUVPUWIUWJDWMWNWOWPVCVUCVUAARMZU + VTUVMVUCVUAAUWCWQZBUWGMZVUATZARMVULVUOVUBARVUNUWHVUAVUMUWFBUWGVUAUWFAUWCB + WRABUGUWIUWDUWJUWEUWGUWCUVJWSUWGUWCUVKWSWTXAVSXBVSVUAABXCXDUVTUCULZCUVJWF + ZUKULZCUVKWFZOZUKRSUCRSZVULUVMTZUVTVUQUCRSZVUSUKRSZOVVAUVRVVCUVSVVDUVRUWG + CUVJWFZARSZVVCVUHVVFFUVJHUAWRUYBVUGVVEARUWGCUXAUVJXEVFJXFVVEVUQAUCRUWGVUP + CUVJWHWIWBUVSUWGCUVKWFZARSZVVDVUHVVHFUVKHUBWRUYKVUGVVGARUWGCUXAUVKXEVFJXF + VVGVUSAUKRUWGVURCUVKWHWIWBXGVUQVUSUCUKRRXHXJVUTVVBUCUKRRVUPRNZVURRNZOZVUT + VVBVVKVUTOZVULUCUKUGZVUAAVUPMZOZUVMVVLVULVVMVVNVVLVULVUPVURNZURZVURVUPNZU + RZOVVPVVMVVRUHZVVMVVLVULVVQVVSVVLVULVUAAVURMZVVQVVJVULVWATZVVIVUTVVJVURRX + IVWBVURXKVUAAVURRXLXMXNVVLVWAVVQVVLVWAOVVPUMCNZLVVLVWAVVPVWCTVVLVVPVWAVWC + VVLVVPVWAVUPUVJPZVUPUVKPZQZVWCVVPVWAVWFTTVVLVUAVWFAVUPVURAUCUGUWIVWDUWJVW + EUWGVUPUVJWSUWGVUPUVKWSWTXOXPVVKVUQVUSVVPVWFVWCTZTVVKVUQVUSVVPVWGVUSVVPOV + WECNZVVKVUQOVWGVURCVUPUVKXQVVIVUQVWHVWGTZVVJVUQVVIUVJXRZVUPQZVWIVUPCUVJYB + VVIVWKOZVWFVWHVWCVWLVUPVWJNZURZVWDUMQZVWFVWHVWCTZTVVIVUPVUPNZURZVWKVWNVVI + VUPYCZVWRVUPXSZVUPXTXMVWKVWNVWRVWKVWMVWQVWJVUPVUPYAVMYDYEVUPUVJYFVWOVWFVW + PVWOVWFOUMVWEQZVWPVWDUMVWEUUAVXAVWCVWHUMVWECYGUUBXMYHUUCYIYJUUDYOYKYLYMYI + YNYPYHYQVVLVULVVNVVSVVIVULVVNTZVVJVUTVVIVUPRXIVXBVUPXKVUAAVUPRXLXMUUHZVVL + VVNVVSVVLVVNOVVRVWCLVVLVVNVVRVWCTVVLVVRVVNVWCVVLVVRVVNVURUVJPZVURUVKPZQZV + WCVVRVVNVXFTTVVLVUAVXFAVURVUPAUKUGUWIVXDUWJVXEUWGVURUVJWSUWGVURUVKWSWTXOX + PVVKVUQVUSVVRVXFVWCTZTZVVKVUSVUQVXHVVKVUSVUQVVRVXGVUQVVROVXDCNZVVKVUSOVXG + VUPCVURUVJXQVUSVVKUVKXRZVURQZVXIVXGTZVURCUVKYBVVJVXKVXLVVIVVJVXKOVXEUMQZV + XLVVJVURVURNZURZVXKVXMVVJVURYCZVXOVURXSZVURXTXMVXOVXKOVURVXJNZURZVXMVXKVX + SVXOVXKVXRVXNVXJVURVURYAVMYDVURUVKYFXMYEVXMVXFVXIVWCVXFVXMVXIVWCTZVXFVXMO + VXDUMQZVXTVXDVXEUMUUEVYAVXIVWCVXDUMCYGUUFXMUUGYIXMUUIYJYOYKYIYLYMYIYNYPYH + YQYRVVKVVTVUTVVIVWSVXPVVTVVJVWTVXQVUPVURUUJWOUUKVVPVVMVVRUULUUMVXCYRVUTUV + MVVOVOZVVKVUQUVJVUPYSUVKVURYSVYBVUSVUPCUVJYTVURCUVKYTAVUPVURUVJUVKUUNWOUU + OUUQYHUUPUURYOUUSUUTUVAUVBUVOUVLUVNUVMUHUWBUVLUVMUVNUVHUVLUVNUVMUVCUVDUVE + UVFUAUBHEUVGUVI $. + $} + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The support of functions @@ -398705,6 +398902,51 @@ a multiplicative function (but not completely multiplicative). BWIPWJDXGXHWKWLWM $. $} +$( +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Ordering +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= +$) + + ${ + $d x y z $. + $( Lemma for ~ sltso . The sign expansion relationship totally orders the + surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.) $) + sltsolem1 $p |- { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } + Or ( { 1o , 2o } u. { (/) } ) $= + ( vx vy vz c1o c2o c0 cop cv wbr wcel wceq wa w3o eqtr2 brtp expcom 3jaod + mto ex ad2ant2lr ctp wor cpr csn cun wn 1n0 neii con0 wb 0elon csuc df-2o + 1on df-1o eqeq12i suc11 bitrid nemtbir ancoms nsuceq0 eqeq1i 3pm3.2ni vex + mp2an mtbir a1i w3a pm2.21i ad2ant2rl 3mix2 3jaoi imp syl2anb sylibr eltp + wi eqtr3 3mix2d 3mix1d 3mix1 3mix3 biid 3orbi123i issoi df-tp soeq2 ax-mp + 3mix3d mpbi ) DEFUAZDFGDEGFEGUAZUBZDEUCFUDUEZWLUBZABCWKWLAHZWPWLIZUFWPWKJ + ZWQWPDKZWPFKZLZWSWPEKZLZWTXBLZMXAXCXDXADFKZDFUGUHZWPDFNRXCEDKZXGDFUGDUIJZ + FUIJZXGXEUJUNUKXGDULZFULZKXHXILXEEXJDXKUMUOUPDFUQURVEUSZXBWSXGWPEDNUTRXDE + FKZXMXJFDVAEXJFUMVBUSZXBWTXMWPEFNUTRVCDFDEFEWPWPAVDZXOOVFVGWPBHZWLIZXPCHZ + WLIZLZWPXRWLIZVQWRXPWKJZXRWKJVHXTWSXRFKZLZWSXREKZLZWTYELZMZYAXQWSXPFKZLZW + SXPEKZLZWTYKLZMZXPDKZYCLZYOYELZYIYELZMZYHXSDFDEFEWPXPXOBVDZOZDFDEFEXPXRYT + CVDZOYNYSYHYJYSYHVQYLYMYJYPYHYQYRYPYJYHYOYIYHYCWSYOYILZYHUUCXEXFXPDFNRVIZ + VJPYQYJYHYOYIYHYEWSUUDVJPYJYRYHWSYEYHYIYIYFYDYGVKVJSQYLYPYHYQYRYLYPYHYKYO + YHWSYCYKYOLZYHUUEXGXLXPEDNRVIZTSYLYQYHYKYOYHWSYEUUFTSYLYRYHYKYIYHWSYEYKYI + LZYHUUGXMXNXPEFNRVIZTSQYMYPYHYQYRYMYPYHYKYOYHWTYCUUFTSYMYQYHYKYOYHWTYEUUF + TSYMYRYHYKYIYHWTYEUUHTSQVLVMVNDFDEFEWPXRXOUUBOVOVGWRYBLYNWPXPKZYOWTLZYOXB + LZYIXBLZMZMZXQUUIXPWPWLIZMWRWSXBWTMZYOYKYIMZUUNYBWPDEFXOVPXPDEFYTVPUUPUUQ + UUNWSUUQUUNVQXBWTWSYOUUNYKYIWSYOUUNWSYOLUUIYNUUMWPXPDVRVSSWSYKUUNYLYNUUIU + UMYLYJYMVKVTSWSYIUUNYJYNUUIUUMYJYLYMWAVTSQXBYOUUNYKYIYOXBUUNUUKUUMYNUUIUU + KUUJUULVKWIPXBYKUUNXBYKLUUIYNUUMWPXPEVRVSSYIXBUUNUULUUMYNUUIUULUUJUUKWBWI + PQWTYOUUNYKYIYOWTUUNUUJUUMYNUUIUUJUUKUULWAWIPWTYKUUNYMYNUUIUUMYMYJYLWBVTS + WTYIUUNWTYILUUIYNUUMWPXPFVRVSSQVLVMVNXQYNUUIUUIUUOUUMUUAUUIWCDFDEFEXPWPYT + XOOWDVOWEWKWNKWMWOUJDEFWFWKWNWLWGWHWJ $. + $} + + ${ + $d f g x y $. + $( Surreal less than totally orders the surreals. Axiom O of [Alling] + p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) $) + sltso $p |- ( ps -> ( ch -> et ) ) ) $. 3jaodd.2 $e |- ( ph -> ( ps -> ( th -> et ) ) ) $. @@ -532042,11 +532274,6 @@ Real and complex numbers (cont.) ( wb wi wa dfbi2 imbi1i impexp bitri ) ABDZCEABEZBAEZFZCELMCEEKNCABGHLMCIJ $. - $( Elimination of two disjuncts in a triple disjunction. (Contributed by - Scott Fenton, 9-Jun-2011.) $) - 3orel13 $p |- ( ( -. ph /\ -. ch ) -> ( ( ph \/ ps \/ ch ) -> ps ) ) $= - ( wn w3o wo 3orel3 orel1 sylan9r ) CDABCEABFADBABCGABHI $. - ${ $d A b $. $d C b $. $( Ordinal less than is equivalent to having an ordinal between them. @@ -534297,20 +534524,6 @@ Set induction (or epsilon induction) =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) - ${ - $d ph y z $. $d x y z $. - $( A closed form of ~ tfis . (Contributed by Scott Fenton, 8-Jun-2011.) $) - tfisg $p |- ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> - A. x e. On ph ) $= - ( vz cv wsbc wral wi con0 crab wceq wss wcel ssrab2 wa dfss3 nfcv elrabsf - simprbi nfsbc1v ralimi sylbi nfralw nfim sbceq1a imbi12d rspc impcom syl5 - raleq simpr jctild syl6ibr ralrimiva tfi sylancr eqcomd rabid2 sylib ) AB - CEZFZCBEZGZAHZBIGZIABIJZKABIGVEVFIVEVFILDEZVFLZVGVFMZHZDIGVFIKABINVEVJDIV - EVGIMZOZVHVKABVGFZOVIVLVHVMVKVHVACVGGZVLVMVHUTVFMZCVGGVNCVGVFPVOVACVGVOUT - IMVAABUTIBIQZRSUAUBVKVEVNVMHZVDVQBVGIVNVMBVABCVGBVGQABUTTUCABVGTUDVBVGKVC - VNAVMVACVBVGUJABVGUEUFUGUHUIVEVKUKULABVGIVPRUMUNDVFUOUPUQABIURUS $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Well-Founded Induction @@ -535159,177 +535372,6 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= $} $} - -$( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - Ordering Ordinal Sequences -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -$) - - ${ - $d A f x $. $d G f x $. $d X x $. - orderseqlem.1 $e |- F = { f | E. x e. On f : x --> A } $. - $( Lemma for ~ poseq and ~ soseq . The function value of a sequene is - either in ` A ` or null. (Contributed by Scott Fenton, 8-Jun-2011.) $) - orderseqlem $p |- ( G e. F -> ( G ` X ) e. ( A u. { (/) } ) ) $= - ( wcel cv wf con0 wrex cfv c0 csn cun wceq feq1 wss syl rexbidv ibi unss1 - elab2g crn frn fvrn0 ssel mpisyl rexlimivw ) EDHZAIZBEJZAKLZFEMZBNOZPZHZU - KUNULBCIZJZAKLUNCEDDUSEQUTUMAKULBUSERUAGUDUBUMURAKUMEUEZUPPZUQSZUOVBHURUM - VABSVCULBEUFVABUPUCTEFUGVBUQUOUHUIUJT $. - $} - - ${ - $d A b f x $. $d a b c f g t w x y z $. $d F a b c f g t w x z $. - $d R f g t w x z $. $d S a b c $. - poseq.1 $e |- R Po ( A u. { (/) } ) $. - poseq.2 $e |- F = { f | E. x e. On f : x --> A } $. - poseq.3 $e |- S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ - E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ - ( f ` x ) R ( g ` x ) ) ) } $. - $( A partial ordering of sequences of ordinals. (Contributed by Scott - Fenton, 8-Jun-2011.) $) - poseq $p |- S Po F $= - ( vz vw wbr wa wral cfv con0 wrex anbi12d va vb vc vt wpo cv wn wcel wceq - wi w3a c0 csn cun cab feq2 cbvrexvw abbii eqtri orderseqlem poirr sylancr - wf intnand adantr nrexdv imnan vex weq eleq1w anbi1d fveq1 eqeq1d ralbidv - mpbi breq1d rexbidv anbi2d eqeq2d breq2d mtbir raleq fveq2 breq12d bitrid - brab simplll simplrr an4 2rexbii reeanv bitri word eloni ordtri3or syl2an - wel w3o simp1l wss onelss imp adantll ssralv anim2d r19.26 syl6ibr ralimi - eqtr syl adantrd 3impia eqeq12d rspcv breq2 biimpd com3l ad2ant2lr impcom - syl6 3adant1 rspcev syl12anc 3exp ad2antrr ad2antlr ad2antll 3jca anim12i - potr anassrs sylan2 exp32 imbi1d syl5ibcom simp1r adantlr anim1d sylbir - a1d breq1 biimprd ad2ant2rl 3jaod mpd rexlimivv jca31 an4s syl2anb sylibr - pm3.2i a1i rgen3 df-po mpbir ) HEUEUAUFZUUPENZUGZUUPUBUFZENZUUSUCUFZENZOZ - UUPUVAENZUJZOZUCHPUBHPUAHPUVFUAUBUCHHHUVFUUPHUHZUUSHUHZUVAHUHZUKUURUVEUUQ - UVGUVGOZBUFZUUPQZUVLUIZBAUFZPZUVNUUPQZUVPDNZOZARSZOZUVJUVSUGZUJUVTUGUVGUW - AUVGUVGUVRARUVGUVRUGUVNRUHUVGUVQUVOUVGCULUMUNZDUEZUVPUWBUHUVQUGIUBCFHUUPU - VNHUVNCFUFZVCZARSZFUOUUSCUWDVCZUBRSZFUOJUWFUWHFUWEUWGAUBRUVNUUSCUWDUPUQUR - USUTUWBUVPDVAVBVDVEVFVEUVJUVSVGVOUWDHUHZGUFZHUHZOZUVKUWDQZUVKUWJQZUIZBUVN - PZUVNUWDQZUVNUWJQZDNZOZARSZOZUVGUWKOZUVLUWNUIZBUVNPZUVPUWRDNZOZARSZOUVTFG - UUPUUPEUAVHZUXIFUAVIZUWLUXCUXAUXHUXJUWIUVGUWKFUAHVJVKZUXJUWTUXGARUXJUWPUX - EUWSUXFUXJUWOUXDBUVNUXJUWMUVLUWNUVKUWDUUPVLVMZVNUXJUWQUVPUWRDUVNUWDUUPVLV - PTVQTGUAVIZUXCUVJUXHUVSUXMUWKUVGUVGGUAHVJVRUXMUXGUVRARUXMUXEUVOUXFUVQUXMU - XDUVMBUVNUXMUWNUVLUVLUVKUWJUUPVLVSVNUXMUWRUVPUVPDUVNUWJUUPVLVTTVQTKWFWAUV - CUVGUVIOZUVLUVKUVAQZUIZBUDUFZPZUXQUUPQZUXQUVAQZDNZOZUDRSZOZUVDUUTUVGUVHOZ - UVLUVKUUSQZUIZBLUFZPZUYHUUPQZUYHUUSQZDNZOZLRSZOZUVHUVIOZUYFUXOUIZBMUFZPZU - YRUUSQZUYRUVAQZDNZOZMRSZOZUYDUVBUXBUXCUXDBUYHPZUYJUYHUWJQZDNZOZLRSZOUYOFG - UUPUUSEUXIUBVHZUXJUWLUXCUXAVUJUXKUXAUWOBUYHPZUYHUWDQZVUGDNZOZLRSUXJVUJUWT - VUOALRALVIZUWPVULUWSVUNUWOBUVNUYHWBVUPUWQVUMUWRVUGDUVNUYHUWDWCUVNUYHUWJWC - WDTUQUXJVUOVUILRUXJVULVUFVUNVUHUXJUWOUXDBUYHUXLVNUXJVUMUYJVUGDUYHUWDUUPVL - VPTVQWETGUBVIZUXCUYEVUJUYNVUQUWKUVHUVGGUBHVJVRVUQVUIUYMLRVUQVUFUYIVUHUYLV - UQUXDUYGBUYHVUQUWNUYFUVLUVKUWJUUSVLVSVNVUQVUGUYKUYJDUYHUWJUUSVLVTTVQTKWFU - XBUVHUWKOZUYFUWNUIZBUYRPZUYTUYRUWJQZDNZOZMRSZOVUEFGUUSUVAEVUKUCVHZFUBVIZU - WLVURUXAVVDVVFUWIUVHUWKFUBHVJVKUXAUWOBUYRPZUYRUWDQZVVADNZOZMRSVVFVVDUWTVV - JAMRAMVIZUWPVVGUWSVVIUWOBUVNUYRWBVVKUWQVVHUWRVVADUVNUYRUWDWCUVNUYRUWJWCWD - TUQVVFVVJVVCMRVVFVVGVUTVVIVVBVVFUWOVUSBUYRVVFUWMUYFUWNUVKUWDUUSVLVMVNVVFV - VHUYTVVADUYRUWDUUSVLVPTVQWETGUCVIZVURUYPVVDVUDVVLUWKUVIUVHGUCHVJZVRVVLVVC - VUCMRVVLVUTUYSVVBVUBVVLVUSUYQBUYRVVLUWNUXOUYFUVKUWJUVAVLZVSVNVVLVVAVUAUYT - DUYRUWJUVAVLVTTVQTKWFUYEUYPUYNVUDUYDUYEUYPOZUYNVUDOZOUVGUVIUYCUVGUVHUYPVV - PWGUYEUVHUVIVVPWHVVPVVOUYCVVPUYIUYSOZUYLVUBOZOZMRSLRSZVVOUYCUJZVVTUYMVUCO - ZMRSLRSVVPVVSVWBLMRRUYIUYSUYLVUBWIWJUYMVUCLMRRWKWLVVSVWALMRRUYHRUHZUYRRUH - ZOZLMWQZLMVIZMLWQZWRZVVSVWAUJZVWCUYHWMUYRWMVWIVWDUYHWNUYRWNUYHUYRWOWPVWEV - WFVWJVWGVWHVWEVWFVVSVWAVWEVWFVVSUKZUYCVVOVWKVWCUXPBUYHPZUYJUYHUVAQZDNZUYC - VWCVWDVWFVVSWSVWEVWFVVSVWLVWEVWFOZVVQVWLVVRVWOUYHUYRWTZVVQVWLUJVWDVWFVWPV - WCVWDVWFVWPUYRUYHXAXBXCVWPVVQUYGUYQOZBUYHPZVWLVWPVVQUYIUYQBUYHPZOZVWRVWPU - YSVWSUYIUYQBUYHUYRXDXEUYGUYQBUYHXFZXGVWQUXPBUYHUVLUYFUXOXIZXHZXTXJXKXLVWF - VVSVWNVWEVVSVWFVWNUYSUYLVWFVWNUJZUYIVUBUYSUYLVXDVWFUYSUYLVWNVWFUYSUYKVWMU - IZUYLVWNUJUYQVXEBUYHUYRBLVIUYFUYKUXOVWMUVKUYHUUSWCUVKUYHUVAWCXMXNVXEUYLVW - NUYKVWMUYJDXOXPXTXQXBXRXSYAUYBVWLVWNOZUDUYHRUDLVIZUXRVWLUYAVWNUXPBUXQUYHW - BVXGUXSUYJUXTVWMDUXQUYHUUPWCUXQUYHUVAWCWDTYBZYCYTYDVWCVWGVWJUJVWDVWCVWRUY - LUYKVWMDNZOZOZVWAUJVWGVWJVWCVXKVVOUYCVXKVVOOVWCVXFUYCVWRVXJVVOVXFVWRVWLVX - JVVOOVWNVXCVVOVXJVWNVVOUWCUYJUWBUHZUYKUWBUHZVWMUWBUHZUKVXJVWNUJIVVOVXLVXM - VXNUVGVXLUVHUYPACFHUUPUYHJUTYEUVHVXMUVGUYPACFHUUSUYHJUTYFUVIVXNUYEUVHACFH - UVAUYHJUTYGYHUWBUYJUYKVWMDYJVBXSYIYKVXHYLYMVWGVXKVVSVWAVWGVWRVVQVXJVVRVWR - VWTVWGVVQVXAVWGVWSUYSUYIUYQBUYHUYRWBVRWEVWGVXIVUBUYLVWGUYKUYTVWMVUADUYHUY - RUUSWCUYHUYRUVAWCWDVRTYNYOVEVWEVWHVVSVWAVWEVWHVVSUKZUYCVVOVXOVWDUXPBUYRPZ - UYRUUPQZVUADNZUYCVWCVWDVWHVVSYPVWEVWHVVSVXPVWEVWHOUYRUYHWTZVVSVXPUJVWCVWH - VXSVWDVWCVWHVXSUYHUYRXAXBYQVXSVVQVXPVVRVXSVVQUYGBUYRPZUYSOZVXPVXSUYIVXTUY - SUYGBUYRUYHXDYRVYAVWQBUYRPVXPUYGUYQBUYRXFVWQUXPBUYRVXBXHYSXTXKXJXLVWHVVSV - XRVWEVVSVWHVXRUYIVUBVWHVXRUJZUYSUYLUYIVUBVYBVWHUYIVUBVXRVWHUYIVXQUYTUIZVU - BVXRUJUYGVYCBUYRUYHBMVIUVLVXQUYFUYTUVKUYRUUPWCUVKUYRUUSWCXMXNVYCVXRVUBVXQ - UYTVUADUUAUUBXTXQXBUUCXSYAUYBVXPVXROUDUYRRUDMVIZUXRVXPUYAVXRUXPBUXQUYRWBV - YDUXSVXQUXTVUADUXQUYRUUPWCUXQUYRUVAWCWDTYBYCYTYDUUDUUEUUFYSXSUUGUUHUUIUXB - UXCUXDBUXQPZUXSUXQUWJQZDNZOZUDRSZOUYDFGUUPUVAEUXIVVEUXJUWLUXCUXAVYIUXKUXA - UWOBUXQPZUXQUWDQZVYFDNZOZUDRSUXJVYIUWTVYMAUDRAUDVIZUWPVYJUWSVYLUWOBUVNUXQ - WBVYNUWQVYKUWRVYFDUVNUXQUWDWCUVNUXQUWJWCWDTUQUXJVYMVYHUDRUXJVYJVYEVYLVYGU - XJUWOUXDBUXQUXLVNUXJVYKUXSVYFDUXQUWDUUPVLVPTVQWETVVLUXCUXNVYIUYCVVLUWKUVI - UVGVVMVRVVLVYHUYBUDRVVLVYEUXRVYGUYAVVLUXDUXPBUXQVVLUWNUXOUVLVVNVSVNVVLVYF - UXTUXSDUXQUWJUVAVLVTTVQTKWFUUJUUKUULUUMUAUBUCHEUUNUUO $. - $} - - ${ - $d a b p q y $. $d A f p q x $. $d A y $. $d F a b f g x $. - $d f g x y $. $d R f g x $. $d S a b $. - soseq.1 $e |- R Or ( A u. { (/) } ) $. - soseq.2 $e |- F = { f | E. x e. On f : x --> A } $. - soseq.3 $e |- S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ - E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ - ( f ` x ) R ( g ` x ) ) ) } $. - soseq.4 $e |- -. (/) e. A $. - $( A linear ordering of sequences of ordinals. (Contributed by Scott - Fenton, 8-Jun-2011.) $) - soseq $p |- S Or F $= - ( wral wcel wa cfv wceq con0 wrex wi va vb vp wor wpo wbr weq w3o csn cun - vq cv c0 sopo ax-mp poseq wo wn eleq1w anbi1d fveq1 eqeq1d ralbidv breq1d - anbi12d rexbidv anbi2d eqeq2d breq2d brabg bianabs ancoms notbid ralinexa - wb orbi12d andi eqcom ralbii anbi1i orbi2i bitri rexbii r19.43 xchbinx wf - cab feq2 cbvrexvw abbii eqtri orderseqlem sotrieq mpan syl2an imbi2d wsbc - vex fveq2 eqeq12d sbcie imbi1i tfisg sylbir feq1 elab2 anbi12i reeanv wss - bitr4i onss ssralv syl ad2antlr rspcv a1i ffvelcdm cdm eloni ordirr eleq2 - fdm word biimparc sylan ndmfv eleq1 ex com23 sylan2 exp4b imp32 syldd imp - syl5 mtoi syld jcad wfn ffn eqtr2 biimprd 3syl adantlr eqtr biimpd expcom - ad2antrr adantll ordtri3or adantr 3orel13 syl6ci eqfnfv2 adantl rexlimivv - sylibrd sylbi sylbird syl5bir sylbid orrd df-3or bitr2i sylib rgen2 df-so - 3orcomb mpbir2an ) HEUDHEUEUAULZUBULZEUFZUAUBUGZUVKUVJEUFZUHZUBHMUAHMABCD - EFGHCUMUIUJZDUDZUVPDUEIUVPDUNUOJKUPUVOUAUBHHUVJHNZUVKHNZOZUVLUVNUQZUVMUQZ - UVOUVTUWAUVMUVTUWAURBULZUVJPZUWCUVKPZQZBAULZMZUWGUVJPZUWGUVKPZDUFZOZARSZU - WEUWDQZBUWGMZUWJUWIDUFZOZARSZUQZURZUVMUVTUWAUWSUVTUVLUWMUVNUWRUVTUVLUWMFU - LZHNZGULZHNZOZUWCUXAPZUWCUXCPZQZBUWGMZUWGUXAPZUWGUXCPZDUFZOZARSZOZUVRUXDO - ZUWDUXGQZBUWGMZUWIUXKDUFZOZARSZOUVTUWMOFGUVJUVKHHEFUAUGZUXEUXPUXNUYAUYBUX - BUVRUXDFUAHUSUTUYBUXMUXTARUYBUXIUXRUXLUXSUYBUXHUXQBUWGUYBUXFUWDUXGUWCUXAU - VJVAVBVCUYBUXJUWIUXKDUWGUXAUVJVAVDVEVFVEGUBUGZUXPUVTUYAUWMUYCUXDUVSUVRGUB - HUSVGUYCUXTUWLARUYCUXRUWHUXSUWKUYCUXQUWFBUWGUYCUXGUWEUWDUWCUXCUVKVAVHVCUY - CUXKUWJUWIDUWGUXCUVKVAVIVEVFVEKVJVKUVSUVRUVNUWRVOUVSUVROZUVNUWRUXOUVSUXDO - ZUWEUXGQZBUWGMZUWJUXKDUFZOZARSZOUYDUWROFGUVKUVJHHEFUBUGZUXEUYEUXNUYJUYKUX - BUVSUXDFUBHUSUTUYKUXMUYIARUYKUXIUYGUXLUYHUYKUXHUYFBUWGUYKUXFUWEUXGUWCUXAU - VKVAVBVCUYKUXJUWJUXKDUWGUXAUVKVAVDVEVFVEGUAUGZUYEUYDUYJUWRUYLUXDUVRUVSGUA - HUSVGUYLUYIUWQARUYLUYGUWOUYHUWPUYLUYFUWNBUWGUYLUXGUWDUWEUWCUXCUVJVAVHVCUY - LUXKUWIUWJDUWGUXCUVJVAVIVEVFVEKVJVKVLVPVMUWTUWHUWKUWPUQZURZTZARMZUVTUVMUY - PUWHUYMOZARSZUWSUWHUYMARVNUYRUWLUWQUQZARSUWSUYQUYSARUYQUWLUWHUWPOZUQUYSUW - HUWKUWPVQUYTUWQUWLUWHUWOUWPUWFUWNBUWGUWDUWEVRVSVTWAWBWCUWLUWQARWDWBWEUVTU - YPUWHUWIUWJQZTZARMZUVMUVTVUBUYOARUVTVUAUYNUWHUVRUWIUVPNZUWJUVPNZVUAUYNVOZ - UVSBCFHUVJUWGHUWGCUXAWFZARSZFWGUWCCUXAWFZBRSZFWGJVUHVUJFVUGVUIABRUWGUWCCU - XAWHWIWJWKZWLBCFHUVKUWGVUKWLUVQVUDVUEOVUFIUVPUWIUWJDWMWNWOWPVCVUCVUAARMZU - VTUVMVUCVUAAUWCWQZBUWGMZVUATZARMVULVUOVUBARVUNUWHVUAVUMUWFBUWGVUAUWFAUWCB - WRABUGUWIUWDUWJUWEUWGUWCUVJWSUWGUWCUVKWSWTXAVSXBVSVUAABXCXDUVTUCULZCUVJWF - ZUKULZCUVKWFZOZUKRSUCRSZVULUVMTZUVTVUQUCRSZVUSUKRSZOVVAUVRVVCUVSVVDUVRUWG - CUVJWFZARSZVVCVUHVVFFUVJHUAWRUYBVUGVVEARUWGCUXAUVJXEVFJXFVVEVUQAUCRUWGVUP - CUVJWHWIWBUVSUWGCUVKWFZARSZVVDVUHVVHFUVKHUBWRUYKVUGVVGARUWGCUXAUVKXEVFJXF - VVGVUSAUKRUWGVURCUVKWHWIWBXGVUQVUSUCUKRRXHXJVUTVVBUCUKRRVUPRNZVURRNZOZVUT - VVBVVKVUTOZVULUCUKUGZVUAAVUPMZOZUVMVVLVULVVMVVNVVLVULVUPVURNZURZVURVUPNZU - RZOVVPVVMVVRUHZVVMVVLVULVVQVVSVVLVULVUAAVURMZVVQVVJVULVWATZVVIVUTVVJVURRX - IVWBVURXKVUAAVURRXLXMXNVVLVWAVVQVVLVWAOVVPUMCNZLVVLVWAVVPVWCTVVLVVPVWAVWC - VVLVVPVWAVUPUVJPZVUPUVKPZQZVWCVVPVWAVWFTTVVLVUAVWFAVUPVURAUCUGUWIVWDUWJVW - EUWGVUPUVJWSUWGVUPUVKWSWTXOXPVVKVUQVUSVVPVWFVWCTZTVVKVUQVUSVVPVWGVUSVVPOV - WECNZVVKVUQOVWGVURCVUPUVKXQVVIVUQVWHVWGTZVVJVUQVVIUVJXRZVUPQZVWIVUPCUVJYB - VVIVWKOZVWFVWHVWCVWLVUPVWJNZURZVWDUMQZVWFVWHVWCTZTVVIVUPVUPNZURZVWKVWNVVI - VUPYCZVWRVUPXSZVUPXTXMVWKVWNVWRVWKVWMVWQVWJVUPVUPYAVMYDYEVUPUVJYFVWOVWFVW - PVWOVWFOUMVWEQZVWPVWDUMVWEUUAVXAVWCVWHUMVWECYGUUBXMYHUUCYIYJUUDYOYKYLYMYI - YNYPYHYQVVLVULVVNVVSVVIVULVVNTZVVJVUTVVIVUPRXIVXBVUPXKVUAAVUPRXLXMUUHZVVL - VVNVVSVVLVVNOVVRVWCLVVLVVNVVRVWCTVVLVVRVVNVWCVVLVVRVVNVURUVJPZVURUVKPZQZV - WCVVRVVNVXFTTVVLVUAVXFAVURVUPAUKUGUWIVXDUWJVXEUWGVURUVJWSUWGVURUVKWSWTXOX - PVVKVUQVUSVVRVXFVWCTZTZVVKVUSVUQVXHVVKVUSVUQVVRVXGVUQVVROVXDCNZVVKVUSOVXG - VUPCVURUVJXQVUSVVKUVKXRZVURQZVXIVXGTZVURCUVKYBVVJVXKVXLVVIVVJVXKOVXEUMQZV - XLVVJVURVURNZURZVXKVXMVVJVURYCZVXOVURXSZVURXTXMVXOVXKOVURVXJNZURZVXMVXKVX - SVXOVXKVXRVXNVXJVURVURYAVMYDVURUVKYFXMYEVXMVXFVXIVWCVXFVXMVXIVWCTZVXFVXMO - VXDUMQZVXTVXDVXEUMUUEVYAVXIVWCVXDUMCYGUUFXMUUGYIXMUUIYJYOYKYIYLYMYIYNYPYH - YQYRVVKVVTVUTVVIVWSVXPVVTVVJVWTVXQVUPVURUUJWOUUKVVPVVMVVRUULUUMVXCYRVUTUV - MVVOVOZVVKVUQUVJVUPYSUVKVURYSVYBVUSVUPCUVJYTVURCUVKYTAVUPVURUVJUVKUUNWOUU - OUUQYHUUPUURYOUUSUUTUVAUVBUVOUVLUVNUVMUHUWBUVLUVMUVNUVHUVLUVNUVMUVCUVDUVE - UVFUAUBHEUVGUVI $. - $} - - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Well-founded zero, successor, and limits @@ -535916,54 +535958,6 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $= wss ) ADEZBDEZCDEZFZABPACGHZBCGHZPCAGHZCBGHZPABCITUAUCUBUDQSUAUCJRACKLRSUBU DJQBCKMNO $. - -$( -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - Surreal Numbers: Ordering -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -$) - - ${ - $d x y z $. - $( Lemma for ~ sltso . The sign expansion relationship totally orders the - surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.) $) - sltsolem1 $p |- { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } - Or ( { 1o , 2o } u. { (/) } ) $= - ( vx vy vz c1o c2o c0 cop cv wbr wcel wceq wa w3o eqtr2 brtp expcom 3jaod - mto ex ad2ant2lr ctp wor cpr csn cun wn 1n0 neii con0 wb 0elon csuc df-2o - 1on df-1o eqeq12i suc11 bitrid nemtbir ancoms nsuceq0 eqeq1i 3pm3.2ni vex - mp2an mtbir a1i w3a pm2.21i ad2ant2rl 3mix2 3jaoi imp syl2anb sylibr eltp - wi eqtr3 3mix2d 3mix1d 3mix1 3mix3 biid 3orbi123i issoi df-tp soeq2 ax-mp - 3mix3d mpbi ) DEFUAZDFGDEGFEGUAZUBZDEUCFUDUEZWLUBZABCWKWLAHZWPWLIZUFWPWKJ - ZWQWPDKZWPFKZLZWSWPEKZLZWTXBLZMXAXCXDXADFKZDFUGUHZWPDFNRXCEDKZXGDFUGDUIJZ - FUIJZXGXEUJUNUKXGDULZFULZKXHXILXEEXJDXKUMUOUPDFUQURVEUSZXBWSXGWPEDNUTRXDE - FKZXMXJFDVAEXJFUMVBUSZXBWTXMWPEFNUTRVCDFDEFEWPWPAVDZXOOVFVGWPBHZWLIZXPCHZ - WLIZLZWPXRWLIZVQWRXPWKJZXRWKJVHXTWSXRFKZLZWSXREKZLZWTYELZMZYAXQWSXPFKZLZW - SXPEKZLZWTYKLZMZXPDKZYCLZYOYELZYIYELZMZYHXSDFDEFEWPXPXOBVDZOZDFDEFEXPXRYT - CVDZOYNYSYHYJYSYHVQYLYMYJYPYHYQYRYPYJYHYOYIYHYCWSYOYILZYHUUCXEXFXPDFNRVIZ - VJPYQYJYHYOYIYHYEWSUUDVJPYJYRYHWSYEYHYIYIYFYDYGVKVJSQYLYPYHYQYRYLYPYHYKYO - YHWSYCYKYOLZYHUUEXGXLXPEDNRVIZTSYLYQYHYKYOYHWSYEUUFTSYLYRYHYKYIYHWSYEYKYI - LZYHUUGXMXNXPEFNRVIZTSQYMYPYHYQYRYMYPYHYKYOYHWTYCUUFTSYMYQYHYKYOYHWTYEUUF - TSYMYRYHYKYIYHWTYEUUHTSQVLVMVNDFDEFEWPXRXOUUBOVOVGWRYBLYNWPXPKZYOWTLZYOXB - LZYIXBLZMZMZXQUUIXPWPWLIZMWRWSXBWTMZYOYKYIMZUUNYBWPDEFXOVPXPDEFYTVPUUPUUQ - UUNWSUUQUUNVQXBWTWSYOUUNYKYIWSYOUUNWSYOLUUIYNUUMWPXPDVRVSSWSYKUUNYLYNUUIU - UMYLYJYMVKVTSWSYIUUNYJYNUUIUUMYJYLYMWAVTSQXBYOUUNYKYIYOXBUUNUUKUUMYNUUIUU - KUUJUULVKWIPXBYKUUNXBYKLUUIYNUUMWPXPEVRVSSYIXBUUNUULUUMYNUUIUULUUJUUKWBWI - PQWTYOUUNYKYIYOWTUUNUUJUUMYNUUIUUJUUKUULWAWIPWTYKUUNYMYNUUIUUMYMYJYLWBVTS - WTYIUUNWTYILUUIYNUUMWPXPFVRVSSQVLVMVNXQYNUUIUUIUUOUUMUUAUUIWCDFDEFEXPWPYT - XOOWDVOWEWKWNKWMWOUJDEFWFWKWNWLWGWHWJ $. - $} - - ${ - $d f g x y $. - $( Surreal less than totally orders the surreals. Axiom O of [Alling] - p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) $) - sltso $p |-