From afffed239e2d49a6f4cf739c5170992b6ced6d90 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Sun, 4 Feb 2024 18:45:12 +0100 Subject: [PATCH] minimize ax-13 usage 7 (#3813) --- set.mm | 1142 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 571 insertions(+), 571 deletions(-) diff --git a/set.mm b/set.mm index c5015c64df..4716c10c71 100644 --- a/set.mm +++ b/set.mm @@ -109290,15 +109290,15 @@ it contains AC as a simple corollary (letting ` m ( i ) = (/) ` , this ( v F ( s i^i ( v X. v ) ) ) = z ) ) } $= ( cv wss cxp wa wwe wceq wsbc weq cin co ccnv csn cima copab simpl sseq1d wral simpr sqxpeqd sseq12d anbi12d weeq2 weeq1 sylan9bb id ineq2d oveq12d - eqeq1d cbvsbcv sneq imaeq2d sbceqbid syl5bb cbvralv cnveqd imaeq1d ineq1d - eqeq2 oveq2d raleqbidv cbvopabv eqtri ) HAMZFNZJMZVOVOOZNZPZVOVQQZEMZVQWB - WBOZUAZGUBZBMZRZEVQUCZWFUDZUEZSZBVOUIZPZPZAJUFKMZFNZIMZWOWOOZNZPZWOWQQZDM - ZWQXBXBOZUAZGUBZCMZRZDWQUCZXFUDZUEZSZCWOUIZPZPZKIUFLWNXNAJKIAKTZJITZPZVTW - TWMXMXQVPWPVSWSXQVOWOFXOXPUGZUHXQVQWQVRWRXOXPUJZXQVOWOXRUKULUMXQWAXAWLXLX - OWAWOVQQXPXAVOWOVQUNWOVQWQUOUPWLXBVQXCUAZGUBZXFRZDWHXIUEZSZCVOUIXQXLWKYDB - CVOWKYAWFRZDWJSBCTZYDWGYEEDWJEDTZWEYAWFYGWBXBWDXTGYGUQZYGWCXCVQYGWBXBYHUK - URUSUTVAYFYEYBDWJYCYFWIXIWHWFXFVBVCWFXFYAVJVDVEVFXQYDXKCVOWOXRXQYBXGDYCXJ - XQWHXHXIXQVQWQXSVGVHXQYAXEXFXQXTXDXBGXQVQWQXCXSVIVKUTVDVLVEUMUMVMVN $. + eqeq1d cbvsbcvw sneq imaeq2d eqeq2 sbceqbid syl5bb cbvralvw cnveqd ineq1d + imaeq1d oveq2d raleqbidv cbvopabv eqtri ) HAMZFNZJMZVOVOOZNZPZVOVQQZEMZVQ + WBWBOZUAZGUBZBMZRZEVQUCZWFUDZUEZSZBVOUIZPZPZAJUFKMZFNZIMZWOWOOZNZPZWOWQQZ + DMZWQXBXBOZUAZGUBZCMZRZDWQUCZXFUDZUEZSZCWOUIZPZPZKIUFLWNXNAJKIAKTZJITZPZV + TWTWMXMXQVPWPVSWSXQVOWOFXOXPUGZUHXQVQWQVRWRXOXPUJZXQVOWOXRUKULUMXQWAXAWLX + LXOWAWOVQQXPXAVOWOVQUNWOVQWQUOUPWLXBVQXCUAZGUBZXFRZDWHXIUEZSZCVOUIXQXLWKY + DBCVOWKYAWFRZDWJSBCTZYDWGYEEDWJEDTZWEYAWFYGWBXBWDXTGYGUQZYGWCXCVQYGWBXBYH + UKURUSUTVAYFYEYBDWJYCYFWIXIWHWFXFVBVCWFXFYAVDVEVFVGXQYDXKCVOWOXRXQYBXGDYC + XJXQWHXHXIXQVQWQXSVHVJXQYAXEXFXQXTXDXBGXQVQWQXCXSVIVKUTVEVLVFUMUMVMVN $. $d a b n r s t u v w x y z W $. $( Lemma for ~ fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015.) $) @@ -109944,33 +109944,33 @@ set maps to an element of the set (so that it cannot be extended without 31-May-2015.) $) canthwelem $p |- ( A e. V -> -. F : O -1-1-> A ) $= ( wcel wa wceq cvv wss wf1 cfv co wbr ccnv cima eqid pm3.2i elex adantr - csn cv cxp wwe w3a cop df-ov f1f ad2antlr copab opabid sylibr syl6eleqr - simpr ffvelrnd eqeltrid fpwwe2 mpbiri simprd cin xpeq12i ineq2i oveq12i - wf simpld fpwwe2lem3 mpdan syl5eq 3eqtr3g cnvimass wsbc wral fpwwe2lem2 - wb cdm mpbid dmss syl dmxpss syl6ss sstrid eqsstrid sstrd a1i wess sylc - inss2 weinxp sylib fvex cnvex imaex eqeltri inex1 simpl sqxpeqd sseq12d - sseq1d weeq2 weeq1 sylan9bb 3anbi123d opelopaba syl3anbrc ssexd syl2anc - opelopabga mpbir3and syl12anc opth1 eleqtrrd syl6eleq ovex eliniseg wor - f1fveq wn weso sonr pm2.65da ) DIPZHDGUAZEEJUBZGUCZYNYMUDZYKYLQZYNYMUEZ - YNUKZUFZPZYOYPYNFYSYPYNEFYPEYMJUDZYNEPZYPUUAUUBQEERZYMYMRZQUUCUUDEUGYMU - GUHYPABCDYMGJEEKMYKDSPYLDIUIUJZYPAULZDTZKULZUUFUUFUMZTZUUFUUHUNZUOZQZUU - FUUHGUCUUFUUHUPZGUBDUUFUUHGUQUUMHDUUNGYLHDGVNYKUULHDGURUSUUMUUNUULAKUTZ - HUUMUULUUNUUOPYPUULVDUULAKVAVBLVCVEVFNVGVHZVIZYPFYMFFUMZVJZUPZEYMUPZRZF - ERYPUUTGUBZUVAGUBZRZUVBYPFUUSGUCZYNUVCUVDYPUVFYSYMYSYSUMZVJZGUCZYNFYSUU - SUVHGOUURUVGYMFYSFYSOOVKVLVMYPUUBUVIYNRUUQYPABCDYNYMGJEKMUUEYPUUAUUBUUP - VOZVPVQVRFUUSGUQEYMGUQVSYPYLUUTHPUVAHPUVEUVBWDYKYLVDYPUUTUUOHYPFDTZUUSU - URTZFUUSUNZUUTUUOPYPFEDYPFYSEOYPYSYMWEZEYMYRVTYPUVNEEUMZWEZEYPYMUVOTZUV - NUVPTYPEDTZUVQYPUVRUVQQZEYMUNZCULZYMUWAUWAUMVJGUCBULZRCYQUWBUKUFWABEWBZ - QZYPUUAUVSUWDQUVJYPABCDYMGJEKMUUEWCWFZVOZVIZYMUVOWGWHEEWIWJWKWLZYPUVRUV - QUWFVOZWMUVLYPYMUURWQWNYPFYMUNZUVMYPFETUVTUWJUWHYPUVTUWCYPUVSUWDUWEVIVO - ZFEYMWOWPFYMWRWSUULUVKUVLUVMUOAKFUUSFYSSOYQYRYMEJWTZXAXBXCZYMUURUWLXDZU - UFFRZUUHUUSRZQZUUGUVKUUJUVLUUKUVMUWQUUFFDUWOUWPXEZXHUWQUUHUUSUUIUURUWOU - WPVDUWQUUFFUWRXFXGUWOUUKFUUHUNUWPUVMUUFFUUHXIFUUHUUSXJXKXLXMXNLVCYPUVAU - UOHYPUVAUUOPZUVRUVQUVTUWIUWGUWKYPESPYMSPZUWSUVRUVQUVTUOZWDYPEDSUUEUWIXO - UWTYPUWLWNUULUXAAKEYMSSUUFERZUUHYMRZQZUUGUVRUUJUVQUUKUVTUXDUUFEDUXBUXCX - EZXHUXDUUHYMUUIUVOUXBUXCVDUXDUUFEUXEXFXGUXBUUKEUUHUNUXCUVTUUFEUUHXIEUUH - YMXJXKXLXQXPXRLVCHDUUTUVAGYFXSWFFUUSEYMUWMUWNXTWHYAOYBYPUUBYTYOWDUUQYMY - NYNEEYMGYCYDWHWFYPEYMYEZUUBYOYGYPUVTUXFUWKEYMYHWHUUQEYNYMYIXPYJ $. + csn cv cxp wwe w3a cop df-ov wf f1f ad2antlr copab simpr opabidw sylibr + syl6eleqr ffvelrnd eqeltrid fpwwe2 mpbiri simprd xpeq12i ineq2i oveq12i + cin simpld fpwwe2lem3 mpdan syl5eq 3eqtr3g cdm cnvimass wsbc fpwwe2lem2 + wral mpbid dmss syl dmxpss syl6ss sstrid eqsstrid sstrd inss2 wess sylc + wb a1i weinxp sylib fvex cnvex imaex eqeltri inex1 simpl sseq1d sqxpeqd + sseq12d weeq2 sylan9bb 3anbi123d opelopaba syl3anbrc opelopabga syl2anc + weeq1 ssexd mpbir3and syl12anc opth1 eleqtrrd syl6eleq ovex eliniseg wn + f1fveq wor weso sonr pm2.65da ) DIPZHDGUAZEEJUBZGUCZYNYMUDZYKYLQZYNYMUE + ZYNUKZUFZPZYOYPYNFYSYPYNEFYPEYMJUDZYNEPZYPUUAUUBQEERZYMYMRZQUUCUUDEUGYM + UGUHYPABCDYMGJEEKMYKDSPYLDIUIUJZYPAULZDTZKULZUUFUUFUMZTZUUFUUHUNZUOZQZU + UFUUHGUCUUFUUHUPZGUBDUUFUUHGUQUUMHDUUNGYLHDGURYKUULHDGUSUTUUMUUNUULAKVA + ZHUUMUULUUNUUOPYPUULVBUULAKVCVDLVEVFVGNVHVIZVJZYPFYMFFUMZVNZUPZEYMUPZRZ + FERYPUUTGUBZUVAGUBZRZUVBYPFUUSGUCZYNUVCUVDYPUVFYSYMYSYSUMZVNZGUCZYNFYSU + USUVHGOUURUVGYMFYSFYSOOVKVLVMYPUUBUVIYNRUUQYPABCDYNYMGJEKMUUEYPUUAUUBUU + PVOZVPVQVRFUUSGUQEYMGUQVSYPYLUUTHPUVAHPUVEUVBWPYKYLVBYPUUTUUOHYPFDTZUUS + UURTZFUUSUNZUUTUUOPYPFEDYPFYSEOYPYSYMVTZEYMYRWAYPUVNEEUMZVTZEYPYMUVOTZU + VNUVPTYPEDTZUVQYPUVRUVQQZEYMUNZCULZYMUWAUWAUMVNGUCBULZRCYQUWBUKUFWBBEWD + ZQZYPUUAUVSUWDQUVJYPABCDYMGJEKMUUEWCWEZVOZVJZYMUVOWFWGEEWHWIWJWKZYPUVRU + VQUWFVOZWLUVLYPYMUURWMWQYPFYMUNZUVMYPFETUVTUWJUWHYPUVTUWCYPUVSUWDUWEVJV + OZFEYMWNWOFYMWRWSUULUVKUVLUVMUOAKFUUSFYSSOYQYRYMEJWTZXAXBXCZYMUURUWLXDZ + UUFFRZUUHUUSRZQZUUGUVKUUJUVLUUKUVMUWQUUFFDUWOUWPXEZXFUWQUUHUUSUUIUURUWO + UWPVBUWQUUFFUWRXGXHUWOUUKFUUHUNUWPUVMUUFFUUHXIFUUHUUSXPXJXKXLXMLVEYPUVA + UUOHYPUVAUUOPZUVRUVQUVTUWIUWGUWKYPESPYMSPZUWSUVRUVQUVTUOZWPYPEDSUUEUWIX + QUWTYPUWLWQUULUXAAKEYMSSUUFERZUUHYMRZQZUUGUVRUUJUVQUUKUVTUXDUUFEDUXBUXC + XEZXFUXDUUHYMUUIUVOUXBUXCVBUXDUUFEUXEXGXHUXBUUKEUUHUNUXCUVTUUFEUUHXIEUU + HYMXPXJXKXNXOXRLVEHDUUTUVAGYFXSWEFUUSEYMUWMUWNXTWGYAOYBYPUUBYTYOWPUUQYM + YNYNEEYMGYCYDWGWEYPEYMYGZUUBYOYEYPUVTUXFUWKEYMYHWGUUQEYNYMYIXOYJ $. $} $( The set of well-orders of a set ` A ` strictly dominates ` A ` . A @@ -110244,22 +110244,22 @@ set maps to an element of the set (so that it cannot be extended without con0 wex 19.8ad ween sylibr domtri2 sylancr cdif nfv nfcv crab cif nfmpo2 cint cmpo nfcxfr nfov nfel1 nfim sseq1 weeq1 3anbi23d anbi1d anbi2d oveq2 eleq1d imbi12d nfmpo1 xpeq12 anidms sseq2d weeq2 3anbi123d anbi12d syl5bb - breq2 oveq1 difeq2 eleq12d pwfseqlem3 chvar eldifad expr sylbird pm2.61d - weq ) APUDZFUEZNUDZYLYLUFZUEZYLYNUGZUHZUIZYLUJUKULZYLYNIUMZFUNZYTYLUOUNZY - SUUBYLUPAUUCUUBUQYRAUUCUUBAUUCUIZUUAYLURUSZKUSZFUUDUUCYNUTUNUUAUUFVAAUUCV - MNVBABCDEFGYNHIJKLUTMYLOQRSTUAUBUCVCVDAUJFKVEUUEUJUNUUFFUNUUCAUJMFKAUJMKV - FUJMKVESUJMKVGVHRVIYLVJUJFUUEKVKVLVNVOVPVQYSYTVRZUJYLVSULZUUBYSUJURVTZUNZ - YLUUIUNZUUHUUGWAUJWFUNUUJWBUJWCWDYSYQNWGUUKYSYQNAYMYPYQWEWHYLNWIWJUJYLWKW - LAYRUUHUUBAYRUUHUIZUIZUUAFYLAYMOUDZYOUEZYLUUNUGZUHZUUHUIZUIZYLUUNIUMZFYLW - MZUNZUQZUUMUUAUVAUNZUQONUUMUVDOUUMOWNOUUAUVAOYLYNIOYLWOOICOUTUTCUDZUOUNUV - EURUSKUSDUDGUSUVEUNVRDUJWPWSGUSWQZWTZUCCOUTUTUVFWRXAOYNWOXBXCXDONYKZUUSUU - MUVBUVDUVHUURUULAUVHUUQYRUUHUVHUUOYPUUPYQYMUUNYNYOXEYLUUNYNXFXGXHXIUVHUUT - UUAUVAUUNYNYLIXJXKXLABUIZUVEUUNIUMZFUVEWMZUNZUQUVCCPUUSUVBCUUSCWNCUUTUVAC - YLUUNICYLWOCIUVGUCCOUTUTUVFXMXACUUNWOXBXCXDCPYKZUVIUUSUVLUVBUVMBUURABUVEF - UEZUUNUVEUVEUFZUEZUVEUUNUGZUHZUJUVEVSULZUIUVMUURTUVMUVRUUQUVSUUHUVMUVNYMU - VPUUOUVQUUPUVEYLFXEUVMUVOYOUUNUVMUVOYOVAUVEYLUVEYLXNXOXPUVEYLUUNXQXRUVEYL - UJVSYAXSXTXIUVMUVJUUTUVKUVAUVEYLUUNIYBUVEYLFYCYDXLABCDEFGHIJKLMOQRSTUAUBU - CYEYFYFYGYHYIYJ $. + weq breq2 oveq1 difeq2 eleq12d pwfseqlem3 chvarfv eldifad sylbird pm2.61d + expr ) APUDZFUEZNUDZYLYLUFZUEZYLYNUGZUHZUIZYLUJUKULZYLYNIUMZFUNZYTYLUOUNZ + YSUUBYLUPAUUCUUBUQYRAUUCUUBAUUCUIZUUAYLURUSZKUSZFUUDUUCYNUTUNUUAUUFVAAUUC + VMNVBABCDEFGYNHIJKLUTMYLOQRSTUAUBUCVCVDAUJFKVEUUEUJUNUUFFUNUUCAUJMFKAUJMK + VFUJMKVESUJMKVGVHRVIYLVJUJFUUEKVKVLVNVOVPVQYSYTVRZUJYLVSULZUUBYSUJURVTZUN + ZYLUUIUNZUUHUUGWAUJWFUNUUJWBUJWCWDYSYQNWGUUKYSYQNAYMYPYQWEWHYLNWIWJUJYLWK + WLAYRUUHUUBAYRUUHUIZUIZUUAFYLAYMOUDZYOUEZYLUUNUGZUHZUUHUIZUIZYLUUNIUMZFYL + WMZUNZUQZUUMUUAUVAUNZUQONUUMUVDOUUMOWNOUUAUVAOYLYNIOYLWOOICOUTUTCUDZUOUNU + VEURUSKUSDUDGUSUVEUNVRDUJWPWSGUSWQZWTZUCCOUTUTUVFWRXAOYNWOXBXCXDONYAZUUSU + UMUVBUVDUVHUURUULAUVHUUQYRUUHUVHUUOYPUUPYQYMUUNYNYOXEYLUUNYNXFXGXHXIUVHUU + TUUAUVAUUNYNYLIXJXKXLABUIZUVEUUNIUMZFUVEWMZUNZUQUVCCPUUSUVBCUUSCWNCUUTUVA + CYLUUNICYLWOCIUVGUCCOUTUTUVFXMXACUUNWOXBXCXDCPYAZUVIUUSUVLUVBUVMBUURABUVE + FUEZUUNUVEUVEUFZUEZUVEUUNUGZUHZUJUVEVSULZUIUVMUURTUVMUVRUUQUVSUUHUVMUVNYM + UVPUUOUVQUUPUVEYLFXEUVMUVOYOUUNUVMUVOYOVAUVEYLUVEYLXNXOXPUVEYLUUNXQXRUVEY + LUJVSYBXSXTXIUVMUVJUUTUVKUVAUVEYLUUNIYCUVEYLFYDYEXLABCDEFGHIJKLMOQRSTUAUB + UCYFYGYGYHYKYIYJ $. pwfseqlem4.w $e |- W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. b e. a @@ -110281,49 +110281,49 @@ set maps to an element of the set (so that it cannot be extended without wi ssexd w3a sseq1 id sqxpeqd sseq2d weeq2 3anbi123d anbi2d 3expa adantrr syl pm4.71i syl6bbr oveq1 eleq12d breq1 imbi12d fvex weeq1 3anbi23d oveq2 eleq1d imbi1d wn cdom cdm con0 omelon onenon ax-mp wex simpr3 19.8ad cdif - wb nfv nfcv nfcxfr nfov nfel1 nfim weq sylbird pwfseqlem2 ficardom finnum - chvar syl2anc ween domtri2 crab cint cif cmpo nfmpo2 anbi1d nfmpo1 xpeq12 - sylancr anidms breq2 anbi12d syl5bb difeq2 pwfseqlem3 eldifbd con4d vtocl - expr vtoclg mpcom isfinite eqeltrrd fpwwe2lem3 mpdan cnvimass dmss dmxpss - mpd cen syl6ss sstrid ssfid inex1 eqtr3d wf1o f1of1 f1fveq eqcomd carden2 - syl12anc wpss dfpss2 baib php3 sdomnen ex mt4d eleqtrrd eliniseg wor weso - sylib sonr pm2.65i ) APUJUKZLUKZUWSPNUKZULZAUWSUWTUMZUWSUNZUOZUPZUXAAUWSP - UXDAPUWTJUQZUWSPAPURUPZUWTUSUPUXFUWSUTAPVAVBULZUXGAUXFPUPZUXHAPUWTNULZUXI - AUXJUXIVCPPUTZUWTUWTUTZVCUXKUXLPVDUWTVDVEASTFGUWTJNPPQUHAGVFZUSUPZGUSUPAU - XMIVAGIVRZVGUQZVHZKVIUXQUSUPUXNUAIVAUXPVJGUXOVGVKVLUXMUXQUSKVMVNGVOVPZABC - DEGHIJKLMOQRSUAUBUCUDUEUFUGVQUIVSVTZWAZPUSUPAUXIUXHWKZAPGUSUXRAPGWBZUWTPP - WCZWBZAUYBUYDVCZPUWTWDZFVRZUWTUYGUYGWCWEJUQTVRZUTFUXBUYHUNUOWFTPWGZVCZAUX - JUYEUYJVCZAUXJUXIUXSWHZASTFGUWTJNPQUHUXRWIWJZWHZWHWLASVRZGWBZUWTUYOUYOWCZ - WBZUYOUWTWDZWMZVCZUYOUWTJUQZUYOUPZUYOVAVBULZWKZWKZAUYAWKSPUSUYOPUTZVUAAVU - EUYAVUGVUAAUYBUYDUYFWMZVCAVUGUYTVUHAVUGUYPUYBUYRUYDUYSUYFUYOPGWNVUGUYQUYC - UWTVUGUYOPVUGWOZWPWQUYOPUWTWRWSWTAVUHAUYKVUHUYMUYEUYFVUHUYIUYBUYDUYFVUHVU - HWOXAXBXCXDXEVUGVUCUXIVUDUXHVUGVUBUXFUYOPUYOPUWTJXFVUIXGUYOPVAVBXHXIXIAUY - PQVRZUYQWBZUYOVUJWDZWMZVCZUYOVUJJUQZUYOUPZVUDWKZWKVUFQUWTPNXJZVUJUWTUTZVU - NVUAVUQVUEVUSVUMUYTAVUSVUKUYRVULUYSUYPVUJUWTUYQWNUYOVUJUWTXKXLWTVUSVUPVUC - VUDVUSVUOVUBUYOVUJUWTUYOJXMXNXOXIVUNVUDVUPVUNVUDXPZVAUYOXQULZVUPXPZVUNVAU - JXRZUPZUYOVVCUPZVVAVUTYGVAXSUPVVDXTVAYAYBVUNVULQYCVVEVUNVULQAUYPVUKVULYDY - EUYOQUUAVPVAUYOUUBUUKAVUMVVAVVBAVUMVVAVCZVCZVUOGUYOAUYPRVRZUYQWBZUYOVVHWD - ZWMZVVAVCZVCZUYOVVHJUQZGUYOYFZUPZWKZVVGVUOVVOUPZWKRQVVGVVRRVVGRYHRVUOVVOR - UYOVUJJRUYOYIRJCRUSUSCVRZURUPVVSUJUKLUKDVRHUKVVSUPXPDVAUUCUUDHUKUUEZUUFZU - GCRUSUSVVTUUGYJRVUJYIYKYLYMRQYNZVVMVVGVVPVVRVWBVVLVVFAVWBVVKVUMVVAVWBVVIV - UKVVJVULUYPVVHVUJUYQWNUYOVVHVUJXKXLUUHWTVWBVVNVUOVVOVVHVUJUYOJXMXNXIABVCZ - VVSVVHJUQZGVVSYFZUPZWKVVQCSVVMVVPCVVMCYHCVVNVVOCUYOVVHJCUYOYICJVWAUGCRUSU - SVVTUUIYJCVVHYIYKYLYMCSYNZVWCVVMVWFVVPVWGBVVLABVVSGWBZVVHVVSVVSWCZWBZVVSV - VHWDZWMZVAVVSXQULZVCVWGVVLUDVWGVWLVVKVWMVVAVWGVWHUYPVWJVVIVWKVVJVVSUYOGWN - VWGVWIUYQVVHVWGVWIUYQUTVVSUYOVVSUYOUUJUULWQVVSUYOVVHWRWSVVSUYOVAXQUUMUUNU - UOWTVWGVWDVVNVWEVVOVVSUYOVVHJXFVVSUYOGUUPXGXIABCDEGHIJKLMORUAUBUCUDUEUFUG - UUQYSYSUURUVAYOUUSUUTUVBUVCUVKPUVDVPZVURABCDEGHUWTIJKLMUSOPRUAUBUCUDUEUFU - GYPVNUXTUVEZAUXDPUVLULZUXDPUTZAUXDUJUKZUWRUTZVWPAUWRVWRAUWSVWRLUKZUTZUWRV - WRUTZAUXDUWTUXDUXDWCZWEZJUQZUWSVWTAUWSPUPZVXEUWSUTVWOASTFGUWSUWTJNPQUHUXR - UYLUVFUVGAUXDURUPZVXDUSUPVXEVWTUTAPUXDVWNAUXDUWTXRZPUWTUXCUVHAVXHUYCXRZPA - UYDVXHVXIWBAUYBUYDUYNWAUWTUYCUVIXCPPUVJUVMUVNZUVOZUWTVXCVURUVPABCDEGHVXDI - JKLMUSOUXDRUAUBUCUDUEUFUGYPVNUVQAVAOLVIZUWRVAUPZVWRVAUPZVXAVXBYGAVAOLUVRV - XLUCVAOLUVSXCAUXGVXMVWNPYQXCAVXGVXNVXKUXDYQXCVAOUWRVWRLUVTUWCWJUWAAUXDVVC - UPZPVVCUPZVWSVWPYGAVXGVXOVXKUXDYRXCAUXGVXPVWNPYRXCUXDPUWBYTWJAVWQXPZUXDPU - WDZVWPXPZAUXDPWBZVXRVXQYGVXJVXRVXTVXQUXDPUWEUWFXCAUXGVXRVXSWKVWNUXGVXRVXS - UXGVXRVCUXDPVBULVXSPUXDUWGUXDPUWHXCUWIXCYOUWJUWKUWSUSUPUXEUXAYGUWRLXJZUWT - UWSUWSUSVYAUWLYBUWOAPUWTUWMZVXFUXAXPAUYFVYBAUYFUYIAUYEUYJUYMWAWHPUWTUWNXC - VWOPUWSUWTUWPYTUWQ $. + wb nfv nfcv nfcxfr nfov nfel1 nfim weq chvarfv pwfseqlem2 ficardom finnum + sylbird syl2anc ween domtri2 sylancr crab cif nfmpo2 anbi1d nfmpo1 xpeq12 + cint cmpo anidms breq2 anbi12d syl5bb pwfseqlem3 eldifbd expr con4d vtocl + difeq2 vtoclg mpcom mpd isfinite eqeltrrd fpwwe2lem3 cnvimass dmss dmxpss + mpdan syl6ss sstrid ssfid inex1 eqtr3d wf1o f1of1 f1fveq syl12anc carden2 + cen eqcomd wpss dfpss2 baib php3 sdomnen mt4d eleqtrrd eliniseg sylib wor + ex weso sonr pm2.65i ) APUJUKZLUKZUWSPNUKZULZAUWSUWTUMZUWSUNZUOZUPZUXAAUW + SPUXDAPUWTJUQZUWSPAPURUPZUWTUSUPUXFUWSUTAPVAVBULZUXGAUXFPUPZUXHAPUWTNULZU + XIAUXJUXIVCPPUTZUWTUWTUTZVCUXKUXLPVDUWTVDVEASTFGUWTJNPPQUHAGVFZUSUPZGUSUP + AUXMIVAGIVRZVGUQZVHZKVIUXQUSUPUXNUAIVAUXPVJGUXOVGVKVLUXMUXQUSKVMVNGVOVPZA + BCDEGHIJKLMOQRSUAUBUCUDUEUFUGVQUIVSVTZWAZPUSUPAUXIUXHWKZAPGUSUXRAPGWBZUWT + PPWCZWBZAUYBUYDVCZPUWTWDZFVRZUWTUYGUYGWCWEJUQTVRZUTFUXBUYHUNUOWFTPWGZVCZA + UXJUYEUYJVCZAUXJUXIUXSWHZASTFGUWTJNPQUHUXRWIWJZWHZWHWLASVRZGWBZUWTUYOUYOW + CZWBZUYOUWTWDZWMZVCZUYOUWTJUQZUYOUPZUYOVAVBULZWKZWKZAUYAWKSPUSUYOPUTZVUAA + VUEUYAVUGVUAAUYBUYDUYFWMZVCAVUGUYTVUHAVUGUYPUYBUYRUYDUYSUYFUYOPGWNVUGUYQU + YCUWTVUGUYOPVUGWOZWPWQUYOPUWTWRWSWTAVUHAUYKVUHUYMUYEUYFVUHUYIUYBUYDUYFVUH + VUHWOXAXBXCXDXEVUGVUCUXIVUDUXHVUGVUBUXFUYOPUYOPUWTJXFVUIXGUYOPVAVBXHXIXIA + UYPQVRZUYQWBZUYOVUJWDZWMZVCZUYOVUJJUQZUYOUPZVUDWKZWKVUFQUWTPNXJZVUJUWTUTZ + VUNVUAVUQVUEVUSVUMUYTAVUSVUKUYRVULUYSUYPVUJUWTUYQWNUYOVUJUWTXKXLWTVUSVUPV + UCVUDVUSVUOVUBUYOVUJUWTUYOJXMXNXOXIVUNVUDVUPVUNVUDXPZVAUYOXQULZVUPXPZVUNV + AUJXRZUPZUYOVVCUPZVVAVUTYGVAXSUPVVDXTVAYAYBVUNVULQYCVVEVUNVULQAUYPVUKVULY + DYEUYOQUUAVPVAUYOUUBUUCAVUMVVAVVBAVUMVVAVCZVCZVUOGUYOAUYPRVRZUYQWBZUYOVVH + WDZWMZVVAVCZVCZUYOVVHJUQZGUYOYFZUPZWKZVVGVUOVVOUPZWKRQVVGVVRRVVGRYHRVUOVV + ORUYOVUJJRUYOYIRJCRUSUSCVRZURUPVVSUJUKLUKDVRHUKVVSUPXPDVAUUDUUJHUKUUEZUUK + ZUGCRUSUSVVTUUFYJRVUJYIYKYLYMRQYNZVVMVVGVVPVVRVWBVVLVVFAVWBVVKVUMVVAVWBVV + IVUKVVJVULUYPVVHVUJUYQWNUYOVVHVUJXKXLUUGWTVWBVVNVUOVVOVVHVUJUYOJXMXNXIABV + CZVVSVVHJUQZGVVSYFZUPZWKVVQCSVVMVVPCVVMCYHCVVNVVOCUYOVVHJCUYOYICJVWAUGCRU + SUSVVTUUHYJCVVHYIYKYLYMCSYNZVWCVVMVWFVVPVWGBVVLABVVSGWBZVVHVVSVVSWCZWBZVV + SVVHWDZWMZVAVVSXQULZVCVWGVVLUDVWGVWLVVKVWMVVAVWGVWHUYPVWJVVIVWKVVJVVSUYOG + WNVWGVWIUYQVVHVWGVWIUYQUTVVSUYOVVSUYOUUIUULWQVVSUYOVVHWRWSVVSUYOVAXQUUMUU + NUUOWTVWGVWDVVNVWEVVOVVSUYOVVHJXFVVSUYOGUVAXGXIABCDEGHIJKLMORUAUBUCUDUEUF + UGUUPYOYOUUQUURYSUUSUUTUVBUVCUVDPUVEVPZVURABCDEGHUWTIJKLMUSOPRUAUBUCUDUEU + FUGYPVNUXTUVFZAUXDPUWBULZUXDPUTZAUXDUJUKZUWRUTZVWPAUWRVWRAUWSVWRLUKZUTZUW + RVWRUTZAUXDUWTUXDUXDWCZWEZJUQZUWSVWTAUWSPUPZVXEUWSUTVWOASTFGUWSUWTJNPQUHU + XRUYLUVGUVKAUXDURUPZVXDUSUPVXEVWTUTAPUXDVWNAUXDUWTXRZPUWTUXCUVHAVXHUYCXRZ + PAUYDVXHVXIWBAUYBUYDUYNWAUWTUYCUVIXCPPUVJUVLUVMZUVNZUWTVXCVURUVOABCDEGHVX + DIJKLMUSOUXDRUAUBUCUDUEUFUGYPVNUVPAVAOLVIZUWRVAUPZVWRVAUPZVXAVXBYGAVAOLUV + QVXLUCVAOLUVRXCAUXGVXMVWNPYQXCAVXGVXNVXKUXDYQXCVAOUWRVWRLUVSUVTWJUWCAUXDV + VCUPZPVVCUPZVWSVWPYGAVXGVXOVXKUXDYRXCAUXGVXPVWNPYRXCUXDPUWAYTWJAVWQXPZUXD + PUWDZVWPXPZAUXDPWBZVXRVXQYGVXJVXRVXTVXQUXDPUWEUWFXCAUXGVXRVXSWKVWNUXGVXRV + XSUXGVXRVCUXDPVBULVXSPUXDUWGUXDPUWHXCUWNXCYSUWIUWJUWSUSUPUXEUXAYGUWRLXJZU + WTUWSUWSUSVYAUWKYBUWLAPUWTUWMZVXFUXAXPAUYFVYBAUYFUYIAUYEUYJUYMWAWHPUWTUWO + XCVWOPUWSUWTUWPYTUWQ $. $} ${ @@ -110428,21 +110428,21 @@ set maps to an element of the set (so that it cannot be extended without bren cxp char wral con0 harcl infxpenc2 wf1 wwe w3a coi cdm ccom cop cmpo ax-mp ccnv csuc cres cmpt c0 csn cseqom simpr wceq wb oveq2 cbviunv f1eq3 sylib simpllr simplll simplr sseq2 fveq2 f1oeq1 syl xpeq12 anidms f1oeq2d - biid f1oeq3 3bitrd imbi12d cbvralv mpteq1i pwfseqlem5 imnani nexdv brdomi - nsyl ex exlimdv mpi exlimiv sylbi imp syl6bi mpcom ) AUGUHZLAUIUJZAUKZBLA - BMZNOZULZUIUJZUMZLAUIUNUOXSXTLCMZUPUJZYGAPZQZCUQYFCLAUGURYJYFCYHYIYFYHLYG - DMZRZDUQYIYFUSZLYGDUTYLYMDYLYIYFYLYIQZLEMZPZYOYOVAZYOYOFMZSZRZUSZEYAVBSZV - CZFUQZYFUUBVDUHUUDYAVEUUBFEVFVOYNUUCYFFYNUUCYFYNUUCQZYAYDGMZVGZGUQYEUUEUU - GGUUEUUGUUEUUGQZUAMZAPUBMZUUIUUIVAPUUIUUJVHVILUUIUIUJQZHIUCUDUAAUUIUUJVJZ - UULVKZYRSVLUDUCUUMUUMUDMUULSUCMUULSVMVNZVPVLZIBLUUIYBNOZULZIMZVKZUURUUSUE - UFUGUGHUUIUEMZVQNOHMZUUTVRUFMSUUTUVASUUOOVSVNVTVTUULSVMWAWBZSSVMZVSZUVBUU - NUFUEJUUFYKHILUUIUVAUULSUURVMVNZUUOUVEVLUVDVLZYRUULYGUBKUUHUUGYAJLAJMZNOZ - ULZUUFVGZUUEUUGWCYDUVIWDUUGUVJWEBJLYCUVHYBUVGANWFWGYDUVIYAUUFWHVOWIYLYIUU - CUUGWJYLYIUUCUUGWKUUKWTUUHUUCLKMZPZUVKUVKVAZUVKUVKYRSZRZUSZKUUBVCYNUUCUUG - WLUUAUVPEKUUBYOUVKWDZYPUVLYTUVOYOUVKLWMUVQYTYQYOUVNRZUVMYOUVNRUVOUVQYSUVN - WDYTUVRWEYOUVKYRWNYQYOYSUVNWOWPUVQYQUVMYOUVNUVQYQUVMWDYOUVKYOUVKWQWRWSYOU - VKUVMUVNXAXBXCXDWIUULTUUNTUUOTUVBTIUUQJLUUIUVGNOZULUVCBJLUUPUVSYBUVGUUINW - FWGXEUVETUVFTXFXGXHYAYDGXIXJXKXLXMXKXNXOXPXNXQXR $. + biid f1oeq3 3bitrd imbi12d cbvralvw mpteq1i pwfseqlem5 imnani brdomi nsyl + nexdv ex exlimdv mpi exlimiv sylbi imp syl6bi mpcom ) AUGUHZLAUIUJZAUKZBL + ABMZNOZULZUIUJZUMZLAUIUNUOXSXTLCMZUPUJZYGAPZQZCUQYFCLAUGURYJYFCYHYIYFYHLY + GDMZRZDUQYIYFUSZLYGDUTYLYMDYLYIYFYLYIQZLEMZPZYOYOVAZYOYOFMZSZRZUSZEYAVBSZ + VCZFUQZYFUUBVDUHUUDYAVEUUBFEVFVOYNUUCYFFYNUUCYFYNUUCQZYAYDGMZVGZGUQYEUUEU + UGGUUEUUGUUEUUGQZUAMZAPUBMZUUIUUIVAPUUIUUJVHVILUUIUIUJQZHIUCUDUAAUUIUUJVJ + ZUULVKZYRSVLUDUCUUMUUMUDMUULSUCMUULSVMVNZVPVLZIBLUUIYBNOZULZIMZVKZUURUUSU + EUFUGUGHUUIUEMZVQNOHMZUUTVRUFMSUUTUVASUUOOVSVNVTVTUULSVMWAWBZSSVMZVSZUVBU + UNUFUEJUUFYKHILUUIUVAUULSUURVMVNZUUOUVEVLUVDVLZYRUULYGUBKUUHUUGYAJLAJMZNO + ZULZUUFVGZUUEUUGWCYDUVIWDUUGUVJWEBJLYCUVHYBUVGANWFWGYDUVIYAUUFWHVOWIYLYIU + UCUUGWJYLYIUUCUUGWKUUKWTUUHUUCLKMZPZUVKUVKVAZUVKUVKYRSZRZUSZKUUBVCYNUUCUU + GWLUUAUVPEKUUBYOUVKWDZYPUVLYTUVOYOUVKLWMUVQYTYQYOUVNRZUVMYOUVNRUVOUVQYSUV + NWDYTUVRWEYOUVKYRWNYQYOYSUVNWOWPUVQYQUVMYOUVNUVQYQUVMWDYOUVKYOUVKWQWRWSYO + UVKUVMUVNXAXBXCXDWIUULTUUNTUUOTUVBTIUUQJLUUIUVGNOZULUVCBJLUUPUVSYBUVGUUIN + WFWGXEUVETUVFTXFXGXJYAYDGXHXIXKXLXMXKXNXOXPXNXQXR $. $( The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, @@ -110863,17 +110863,17 @@ Tarski classes ( ~ df-tsk ), and Grothendieck universes ( ~ df-gru ). We A. x e. A E. y e. A x ~< y ) -> _om C_ A ) $= ( vz vw c0 con0 wcel cv csdm wbr wrex w3a com wss wn wceq wa eleq2 syl wo wne wral csuc nn0suc simp1 necon2bi vex sucid mpbiri adantl breq1 rexbidv - wi breq2 cbvrexv syl6bb rspcv cdom cvv biimpa 3ad2antl2 wb suceloni eleq1 - nnon biimparc 3adant3 onelon simpl1 onsssuc syl2anc mpbird ssdomg domnsym - sylan mpsyl nrexdv 3expia intn3an3d rexlimiva jaoi con2i word ordom eloni - pm2.65d 3ad2ant2 ordtri1 sylancr ) CFUBZCGHZAIZBIZJKZBCLZACUCZMZNCOZCNHZP - ZWTWRWTCFQZCDIZUDZQZDNLZUAWRPZDCUEXBXGXFWRCFWKWLWQUFUGXEXGDNXCNHZXERZWQWK - WLXIWQXCEIZJKZECLZXIXCCHZWQXLUNXEXMXHXEXMXCXDHXCDUHZUICXDXCSUJUKWPXLAXCCW - MXCQZWPXCWNJKZBCLXLXOWOXPBCWMXCWNJULUMXPXKBECWNXJXCJUOUPUQURTXHXEWQXLPXHX - EWQMZXKECXQXJCHZRZXJXCUSKZXKPXCUTHXSXJXCOZXTXNXSYAXJXDHZXEXHXRYBWQXEXRYBC - XDXJSVAVBXSXJGHZXCGHZYAYBVCXQWLXRYCXHXEWLWQXHXDGHZXEWLXHYDYEXCVFZXCVDTXEW - LYECXDGVEVGVPVHCXJVIVPXSXHYDXHXEWQXRVJYFTXJXCVKVLVMXJXCUTVNVQXJXCVOTVRVSW - GVTWAWBTWCWRNWDCWDZWSXAVCWEWLWKYGWQCWFWHNCWIWJVM $. + wi breq2 cbvrexvw syl6bb rspcv cdom cvv biimpa 3ad2antl2 wb nnon suceloni + eleq1 biimparc sylan 3adant3 onelon simpl1 onsssuc syl2anc mpbird domnsym + ssdomg mpsyl nrexdv 3expia pm2.65d intn3an3d rexlimiva jaoi word 3ad2ant2 + con2i ordom eloni ordtri1 sylancr ) CFUBZCGHZAIZBIZJKZBCLZACUCZMZNCOZCNHZ + PZWTWRWTCFQZCDIZUDZQZDNLZUAWRPZDCUEXBXGXFWRCFWKWLWQUFUGXEXGDNXCNHZXERZWQW + KWLXIWQXCEIZJKZECLZXIXCCHZWQXLUNXEXMXHXEXMXCXDHXCDUHZUICXDXCSUJUKWPXLAXCC + WMXCQZWPXCWNJKZBCLXLXOWOXPBCWMXCWNJULUMXPXKBECWNXJXCJUOUPUQURTXHXEWQXLPXH + XEWQMZXKECXQXJCHZRZXJXCUSKZXKPXCUTHXSXJXCOZXTXNXSYAXJXDHZXEXHXRYBWQXEXRYB + CXDXJSVAVBXSXJGHZXCGHZYAYBVCXQWLXRYCXHXEWLWQXHXDGHZXEWLXHYDYEXCVDZXCVETXE + WLYECXDGVFVGVHVICXJVJVHXSXHYDXHXEWQXRVKYFTXJXCVLVMVNXJXCUTVPVQXJXCVOTVRVS + VTWAWBWCTWFWRNWDCWDZWSXAVCWGWLWKYGWQCWHWENCWIWJVN $. $( A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) $) @@ -111309,58 +111309,58 @@ prove that every set is contained in a weak universe in ZF (see fneq1i mpbir fnunirn ax-mp bitri csuc elssuni ad2antll ssun2 ssun1 syl6ss c1o sstri wceq simprl fvex uniex unex prex mptex rnex iunex unieq uneq12d weq pweq preq12d preq2 cbvmptv preq1 mpteq2dv syl5eq rneqd cbviunv mpteq1 - id uneq2d iuneq12d frsucmpt2 sylancl sseqtrrd fvssunirn rexlimdvaa syl5bi - sseqtrri ralrimiv dftr3 sylibr con0 1on unexg mpan2 fveq1i fr0g syl6eqssr - syl unssbd 1n0 ssn0 sseqtrrid sstrd unssad vpwex vuniex prss simprd fveq2 - ssiun2s sseq2d vtoclga findsg sseldd wi imbi12d eqeltri simpld word ordom - simplrl ordunel mp3an2i ssidd suceq fveq2d sseq12d ad2antrr sstr2 syl5com - syl2anc simplrr biantrud bicomd eleq1w anbi2d sseq1 anbi12d sseq1d chvarv - expl sylc simprr eqid elrnmpt1s 3jca wfun rdgfun omex resfunexg syl3anbrc - mp2an iswun jca ) DGNZEUFNZDEOUVREUGZEUJUHZJPZUIZENZUWBUKZENZUWBUAPZULZEN - ZUAEUMZUNZJEUMZUVSUVRUWBEOZJEUMUVTUVRUWMJEUWBENZUWBKPZFUOZNZKQUPZUVRUWMUW - NUWBFUQZUIZNZUWREUWTUWBIURFQUSZUXAUWRUTUXBCRCPZUXCUIZSZAUXCAPZUKZUXFUIZUL - ZBUXCUXFBPZULZVAZUQZSZVBZSZVAZDVQSZVCZQVDZQUSUXRUXQVEQFUXTHVFVGZKUWBFQVHV - IVJZUVRUWQUWMKQUVRUWOQNZUWQTTZUWBUWOVKZFUOZEUYDUWBUWPUWPUIZSZLUWPLPZUKZUY - IUIZULZMUWPUYIMPZULZVAZUQZSZVBZSZUYFUYDUWBUYGUYSUWQUWBUYGOUVRUYCUWBUWPVLV - MUYGUYHUYSUYGUWPVNUYHUYRVOZVRVPUYDUYCUYSRNZUYFUYSVSZUVRUYCUWQVTUYHUYRUWPU - YGUWOFWAZUWPVUCWBWCLUWPUYQVUCUYLUYPUYJUYKWDZUYOMUWPUYNVUCWEWFWCWGWCZCUBUX - RUWOUXPUYSUBPZVUFUIZSZLVUFUYLMVUFUYNVAZUQZSZVBZSZFRHUBCWJZVUHUXEVULUXOVUN - VUFUXCVUGUXDVUNXAZVUFUXCWHWIVUNVULAVUFUXIBVUFUXKVAZUQZSZVBUXOLAVUFVUKVURL - AWJZUYLUXIVUJVUQVUSUYJUXGUYKUXHUYIUXFWKUYIUXFWHWLVUSVUIVUPVUSVUIBVUFUYIUX - JULZVAVUPMBVUFUYNVUTUYMUXJUYIWMWNVUSBVUFVUTUXKUYIUXFUXJWOWPWQWRWIWSVUNAVU - FUXCVURUXNVUOVUNVUQUXMUXIVUNVUPUXLBVUFUXCUXKWTWRXBXCWQWIZVUFUWPVSZVUHUYHV - ULUYRVVBVUFUWPVUGUYGVVBXAZVUFUWPWHWIVVBLVUFUWPVUKUYQVVCVVBVUJUYPUYLVVBVUI - UYOMVUFUWPUYNWTWRXBXCWIXDZXEZXFUYFUWTEFUYEXGIXJZVPXHXIXKJEXLXMUVRVQEOVQUJ - UHUWAUVRDVQEUVRUXRUJFUOZEUVRUXRRNZVVGUXRVSUVRVQXNNVVHXODVQGXNXPXQVVHVVGUJ - UXTUOUXRUJFUXTHXRUXRRUXQXSWQYAVVGUWTEFUJXGIXJXTZYBYCVQEYDXEUVRUWKJEUWNUWR - UVRUWKUYBUVRUWQUWKKQUYDUWDUWFUWJUYDUWFUWDUYDUWEUWCULZEOUWFUWDTUYDVVJMUWPU - WBUYMULZVAZUQZEUYDVVJVVMSZUYREUWQVVNUYROUVRUYCLUWPUYQUWBVVNLJWJZUYLVVJUYP - VVMVVOUYJUWEUYKUWCUYIUWBWKUYIUWBWHWLZVVOUYOVVLVVOMUWPUYNVVKUYIUWBUYMWOZWP - WRWIYMVMUYDUYRUYFEUYDUYSUYRUYFUYRUYHVNVVEYEVVFVPYFYGUWEUWCEJYHJYIYJXMZYKU - YDUWFUWDVVRUUAUYDUWIUAEUWGENZUWGUCPZFUOZNZUCQUPZUYDUWIVVSUWGUWTNZVWCEUWTU - WGIURUXBVWDVWCUTUYAUCUWGFQVHVIVJUYDVWBUWIUCQUYDVVTQNZVWBTZTZMUWOVVTSZFUOZ - VVKVAZUQZEUWHVWGVVJVWKEVWGVVJVWKSZLVWIUYLMVWIUYNVAZUQZSZVBZEVWGUWBVWINVWL - VWPOVWGUWPVWIUWBVWGVWHQNZUYCUWPVWIOZQUUBVWGUYCVWEVWQUUCUVRUYCUWQVWFUUDZUY - DVWEVWBVTZQUWOVVTUUEUUFZVWSVWQUYCTUWOVWHOVWRUWOVVTVOUWPUDPZFUOZOZUWPUWPOZ - UWPUEPZFUOZOZUWPVXFVKZFUOZOZVWRUDUEVWHUWOUDKWJVXCUWPUWPVXBUWOFYLYNZUDUEWJ - VXCVXGUWPVXBVXFFYLYNZVXBVXIVSVXCVXJUWPVXBVXIFYLYNZVXBVWHVSVXCVWIUWPVXBVWH - FYLYNUYCUWPUUGZVXFQNZUYCTZUWOVXFOZTZVXGVXJOZVXHVXKVXPVXTUYCVXRUWPUYFOVXTK - VXFQKUEWJZUWPVXGUYFVXJUWOVXFFYLVYAUYEVXIFUWOVXFUUHUUIUUJUYCUYSUWPUYFUWPUY - HUYSUWPUYGVOUYTVRUYCVUAVUBVUEVVDXQYEYOUUKUWPVXGVXJUULUUMZYPXQUUNUVRUYCUWQ - VWFUUOYQLVWIVWOUWBVWLVVOUYLVVJVWNVWKVVPVVOVWMVWJVVOMVWIUYNVVKVVQWPWRWIYMY - AVWGVWPVWHVKZFUOZEVWGVWIVWIUIZSZVWPSZVWPVYDVWPVYFVNVWGVWQVYGRNVYDVYGVSVXA - VYFVWPVWIVYEVWHFWAZVWIVYHWBWCLVWIVWOVYHUYLVWNVUDVWMMVWIUYNVYHWEWFWCWGWCCU - BUXRVWHUXPVYGVUMFRHVVAVUFVWIVSZVUHVYFVULVWPVYIVUFVWIVUGVYEVYIXAZVUFVWIWHW - IVYILVUFVWIVUKVWOVYJVYIVUJVWNUYLVYIVUIVWMMVUFVWIUYNWTWRXBXCWIXDXEYEVYDUWT - EFVYCXGIXJVPYFYBVWGUWGVWINUWHRNUWHVWKNVWGVWAVWIUWGVWGVWQVWEVWAVWIOZVXAVWT - VWEVVTVXFOZTZVWAVXGOZYRVWEVYKYRUEVWHQVXFVWHVSZVYMVWEVYNVYKVYOVWEVYMVYOVYL - VWEVYOVWHVVTVXFVVTUWOVNVYOXAYEUUPUUQVYOVXGVWIVWAVXFVWHFYLYNYSVXPVWEVYLVYN - VXSVXHYRVXPVWETZVYLTZVYNYRKUCKUCWJZVXSVYQVXHVYNVYRVXQVYPVXRVYLVYRUYCVWEVX - PKUCQUURUUSUWOVVTVXFUUTUVAVYRUWPVWAVXGUWOVVTFYLUVBYSVXDVXEVXHVXKVXHUDUEVX - FUWOVXLVXMVXNVXMVXOVYBYPUVCUVDYOUVEUYDVWEVWBUVFYQUWBUWGWDMVWIVVKUWHUWGVWJ - RVWJUVGUYMUWGUWBWMUVHXEYQXHXIXKUVIXHXIXKERNUVSUVTUWAUWLUNUTEUWTRIUWSFFUXT - RHUXSUVJQRNUXTRNUXRUXQUVKUVLUXSQRUVMUVOYTWFWBYTJUAERUVPVIUVNUVRDVQEVVIYGU - VQ $. + uneq2d iuneq12d frsucmpt2w sylancl sseqtrrd fvssunirn sseqtrri rexlimdvaa + id syl5bi ralrimiv dftr3 sylibr con0 1on unexg mpan2 fveq1i syl syl6eqssr + fr0g unssbd ssn0 ssiun2s sseqtrrid sstrd unssad vpwex vuniex simprd fveq2 + 1n0 prss sseq2d vtoclga findsg sseldd wi imbi12d eqeltri word ordom ssidd + simpld simplrl ordunel mp3an2i suceq fveq2d sseq12d sstr2 syl5com syl2anc + ad2antrr simplrr biantrud bicomd eleq1w anbi2d sseq1 anbi12d chvarvv expl + sseq1d sylc eqid elrnmpt1s 3jca wfun omex resfunexg mp2an iswun syl3anbrc + simprr rdgfun jca ) DGNZEUFNZDEOUVREUGZEUJUHZJPZUIZENZUWBUKZENZUWBUAPZULZ + ENZUAEUMZUNZJEUMZUVSUVRUWBEOZJEUMUVTUVRUWMJEUWBENZUWBKPZFUOZNZKQUPZUVRUWM + UWNUWBFUQZUIZNZUWREUWTUWBIURFQUSZUXAUWRUTUXBCRCPZUXCUIZSZAUXCAPZUKZUXFUIZ + ULZBUXCUXFBPZULZVAZUQZSZVBZSZVAZDVQSZVCZQVDZQUSUXRUXQVEQFUXTHVFVGZKUWBFQV + HVIVJZUVRUWQUWMKQUVRUWOQNZUWQTTZUWBUWOVKZFUOZEUYDUWBUWPUWPUIZSZLUWPLPZUKZ + UYIUIZULZMUWPUYIMPZULZVAZUQZSZVBZSZUYFUYDUWBUYGUYSUWQUWBUYGOUVRUYCUWBUWPV + LVMUYGUYHUYSUYGUWPVNUYHUYRVOZVRVPUYDUYCUYSRNZUYFUYSVSZUVRUYCUWQVTUYHUYRUW + PUYGUWOFWAZUWPVUCWBWCLUWPUYQVUCUYLUYPUYJUYKWDZUYOMUWPUYNVUCWEWFWCWGWCZCUB + UXRUWOUXPUYSUBPZVUFUIZSZLVUFUYLMVUFUYNVAZUQZSZVBZSZFRHUBCWJZVUHUXEVULUXOV + UNVUFUXCVUGUXDVUNXIZVUFUXCWHWIVUNVULAVUFUXIBVUFUXKVAZUQZSZVBUXOLAVUFVUKVU + RLAWJZUYLUXIVUJVUQVUSUYJUXGUYKUXHUYIUXFWKUYIUXFWHWLVUSVUIVUPVUSVUIBVUFUYI + UXJULZVAVUPMBVUFUYNVUTUYMUXJUYIWMWNVUSBVUFVUTUXKUYIUXFUXJWOWPWQWRWIWSVUNA + VUFUXCVURUXNVUOVUNVUQUXMUXIVUNVUPUXLBVUFUXCUXKWTWRXAXBWQWIZVUFUWPVSZVUHUY + HVULUYRVVBVUFUWPVUGUYGVVBXIZVUFUWPWHWIVVBLVUFUWPVUKUYQVVCVVBVUJUYPUYLVVBV + UIUYOMVUFUWPUYNWTWRXAXBWIXCZXDZXEUYFUWTEFUYEXFIXGZVPXHXJXKJEXLXMUVRVQEOVQ + UJUHUWAUVRDVQEUVRUXRUJFUOZEUVRUXRRNZVVGUXRVSUVRVQXNNVVHXODVQGXNXPXQVVHVVG + UJUXTUOUXRUJFUXTHXRUXRRUXQYAWQXSVVGUWTEFUJXFIXGXTZYBYLVQEYCXDUVRUWKJEUWNU + WRUVRUWKUYBUVRUWQUWKKQUYDUWDUWFUWJUYDUWFUWDUYDUWEUWCULZEOUWFUWDTUYDVVJMUW + PUWBUYMULZVAZUQZEUYDVVJVVMSZUYREUWQVVNUYROUVRUYCLUWPUYQUWBVVNLJWJZUYLVVJU + YPVVMVVOUYJUWEUYKUWCUYIUWBWKUYIUWBWHWLZVVOUYOVVLVVOMUWPUYNVVKUYIUWBUYMWOZ + WPWRWIYDVMUYDUYRUYFEUYDUYSUYRUYFUYRUYHVNVVEYEVVFVPYFYGUWEUWCEJYHJYIYMXMZY + JUYDUWFUWDVVRUUDUYDUWIUAEUWGENZUWGUCPZFUOZNZUCQUPZUYDUWIVVSUWGUWTNZVWCEUW + TUWGIURUXBVWDVWCUTUYAUCUWGFQVHVIVJUYDVWBUWIUCQUYDVVTQNZVWBTZTZMUWOVVTSZFU + OZVVKVAZUQZEUWHVWGVVJVWKEVWGVVJVWKSZLVWIUYLMVWIUYNVAZUQZSZVBZEVWGUWBVWINV + WLVWPOVWGUWPVWIUWBVWGVWHQNZUYCUWPVWIOZQUUAVWGUYCVWEVWQUUBUVRUYCUWQVWFUUEZ + UYDVWEVWBVTZQUWOVVTUUFUUGZVWSVWQUYCTUWOVWHOVWRUWOVVTVOUWPUDPZFUOZOZUWPUWP + OZUWPUEPZFUOZOZUWPVXFVKZFUOZOZVWRUDUEVWHUWOUDKWJVXCUWPUWPVXBUWOFYKYNZUDUE + WJVXCVXGUWPVXBVXFFYKYNZVXBVXIVSVXCVXJUWPVXBVXIFYKYNZVXBVWHVSVXCVWIUWPVXBV + WHFYKYNUYCUWPUUCZVXFQNZUYCTZUWOVXFOZTZVXGVXJOZVXHVXKVXPVXTUYCVXRUWPUYFOVX + TKVXFQKUEWJZUWPVXGUYFVXJUWOVXFFYKVYAUYEVXIFUWOVXFUUHUUIUUJUYCUYSUWPUYFUWP + UYHUYSUWPUYGVOUYTVRUYCVUAVUBVUEVVDXQYEYOUUNUWPVXGVXJUUKUULZYPXQUUMUVRUYCU + WQVWFUUOYQLVWIVWOUWBVWLVVOUYLVVJVWNVWKVVPVVOVWMVWJVVOMVWIUYNVVKVVQWPWRWIY + DXSVWGVWPVWHVKZFUOZEVWGVWIVWIUIZSZVWPSZVWPVYDVWPVYFVNVWGVWQVYGRNVYDVYGVSV + XAVYFVWPVWIVYEVWHFWAZVWIVYHWBWCLVWIVWOVYHUYLVWNVUDVWMMVWIUYNVYHWEWFWCWGWC + CUBUXRVWHUXPVYGVUMFRHVVAVUFVWIVSZVUHVYFVULVWPVYIVUFVWIVUGVYEVYIXIZVUFVWIW + HWIVYILVUFVWIVUKVWOVYJVYIVUJVWNUYLVYIVUIVWMMVUFVWIUYNWTWRXAXBWIXCXDYEVYDU + WTEFVYCXFIXGVPYFYBVWGUWGVWINUWHRNUWHVWKNVWGVWAVWIUWGVWGVWQVWEVWAVWIOZVXAV + WTVWEVVTVXFOZTZVWAVXGOZYRVWEVYKYRUEVWHQVXFVWHVSZVYMVWEVYNVYKVYOVWEVYMVYOV + YLVWEVYOVWHVVTVXFVVTUWOVNVYOXIYEUUPUUQVYOVXGVWIVWAVXFVWHFYKYNYSVXPVWEVYLV + YNVXSVXHYRVXPVWETZVYLTZVYNYRKUCKUCWJZVXSVYQVXHVYNVYRVXQVYPVXRVYLVYRUYCVWE + VXPKUCQUURUUSUWOVVTVXFUUTUVAVYRUWPVWAVXGUWOVVTFYKUVDYSVXDVXEVXHVXKVXHUDUE + VXFUWOVXLVXMVXNVXMVXOVYBYPUVBUVCYOUVEUYDVWEVWBUVOYQUWBUWGWDMVWIVVKUWHUWGV + WJRVWJUVFUYMUWGUWBWMUVGXDYQXHXJXKUVHXHXJXKERNUVSUVTUWAUWLUNUTEUWTRIUWSFFU + XTRHUXSUVIQRNUXTRNUXRUXQUVPUVJUXSQRUVKUVLYTWFWBYTJUAERUVMVIUVNUVRDVQEVVIY + GUVQ $. $} ${ @@ -112598,19 +112598,19 @@ values in the universe (see ~ gruiun for a more intuitive version). axgroth6 $p |- E. y ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) /\ A. z e. ~P y ( z ~< y -> z e. y ) ) $= ( vw vv wel cv cpw wss wcel wa wral wbr wi w3a wex wb wceq pweq sylbi cen - csdm wrex axgroth5 biid sseq1d cbvralv ssid sseq2 rspcev mpan2 rspccv wal + csdm wrex wo axgroth5 biid sseq1d cbvralvw ssid sseq2 rspcev mpan2 rspccv pwss vpwex sseq1 eleq1 imbi12d spcv syl6 rexlimdv impbid2 ralbidv pm5.32i - wo r19.26 3bitr4i velpw wn cdom impexp cvv ssdomg elv imbi1i brsdom bitri - pm4.71i imbi2i 3bitr4ri pm5.74ri pm4.64 syl6bb ralbiia 3anbi123i exbii + wal r19.26 3bitr4i velpw cdom impexp cvv ssdomg elv pm4.71i imbi1i brsdom + wn bitri imbi2i 3bitr4ri pm5.74ri pm4.64 syl6bb ralbiia 3anbi123i exbii mpbir ) ABFZCGZHZBGZIZWJWKJZKCWKLZWIWKUBMZCBFZNZCWKHZLZOZBPWHWLWJDGZIZDWK - UCZKCWKLZWIWKUAMZWPVEZCWRLZOZBPABCDUDWTXHBWHWHWNXDWSXGWHUEWLCWKLZWMCWKLZK - XIXCCWKLZKWNXDXIXJXKXIEGZHZWKIZEWKLZXJXKQWLXNCEWKWIXLRWJXMWKWIXLSUFUGXOWM - XCCWKXOWMXCWMWJWJIZXCWJUHXBXPDWJWKXAWJWJUIUJUKXOXBWMDWKXODBFXAHZWKIZXBWMN - ZXNXREXAWKXLXARXMXQWKXLXASUFULXRXLXAIZEBFZNZEUMXSEXAWKUNYBXSEWJCUOXLWJRXT + UCZKCWKLZWIWKUAMZWPUDZCWRLZOZBPABCDUEWTXHBWHWHWNXDWSXGWHUFWLCWKLZWMCWKLZK + XIXCCWKLZKWNXDXIXJXKXIEGZHZWKIZEWKLZXJXKQWLXNCEWKWIXLRWJXMWKWIXLSUGUHXOWM + XCCWKXOWMXCWMWJWJIZXCWJUIXBXPDWJWKXAWJWJUJUKULXOXBWMDWKXODBFXAHZWKIZXBWMN + ZXNXREXAWKXLXARXMXQWKXLXASUGUMXRXLXAIZEBFZNZEVEXSEXAWKUNYBXSEWJCUOXLWJRXT XBYAWMXLWJXAUPXLWJWKUQURUSTUTVAVBVCTVDWLWMCWKVFWLXCCWKVFVGWQXFCWRWIWRJWIW - KIZWQXFQCWKVHYCWQXEVIZWPNZXFYCWQYEYCWIWKVJMZKZYENYCYFYENZNYCYENYCWQNYCYFY - EVKYCYGYEYCYFYCYFNBWIWKVLVMVNVRVOWQYHYCWQYFYDKZWPNYHWOYIWPWIWKVPVOYFYDWPV - KVQVSVTWAXEWPWBWCTWDWEWFWG $. + KIZWQXFQCWKVHYCWQXEVQZWPNZXFYCWQYEYCWIWKVIMZKZYENYCYFYENZNYCYENYCWQNYCYFY + EVJYCYGYEYCYFYCYFNBWIWKVKVLVMVNVOWQYHYCWQYFYDKZWPNYHWOYIWPWIWKVPVOYFYDWPV + JVRVSVTWAXEWPWBWCTWDWEWFWG $. $( The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of ~ omex ). Note that our proof depends on neither the Axiom of @@ -112656,15 +112656,15 @@ values in the universe (see ~ gruiun for a more intuitive version). E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) $= ( wel cv wss wi wal wrex wa wral cdom wbr wo w3a wex wb wcel axgroth2 weq - cdif cuni sseq1 elequ1 imbi12d spv mpi reximi eluni2 sylibr adantl ralimi - ssid dfss3 ccrd cdm com cvv vex grothac eleqtrri c0 wne ne0i dominf sylan - infdif2 mp3an12i orbi1d imbi2d albidv sylan2 pm5.32i df-3an 3bitr4i exbii - mpbir ) ABFZDGCGZHDBFIDJZEGZWAHZEDFZIZEJZDBGZKZLZCWHMZWAWHHZWHWAUCWANOZCB - FZPZIZCJZQZBRVTWKWLWHWANOZWNPZIZCJZQZBRABCDEUAWRXCBVTWKLZWQLXDXBLWRXCXDWQ - XBWKVTWHWHUDZHZWQXBSWKWAXETZCWHMXFWJXGCWHWIXGWBWICDFZDWHKXGWGXHDWHWGWAWAH - ZXHWAUOWFXIXHIECECUBWDXIWEXHWCWAWAUEECDUFUGUHUIUJDWAWHUKULUMUNCWHXEUPULVT - XFLZWPXACXJWOWTWLXJWMWSWNWHUQURZTWAXKTXJUSWHNOZWMWSSWHUTXKBVAZVBVCWAUTXKC - VAVBVCVTWHVDVEXFXLWHAGVFWHXMVGVHWHWAVIVJVKVLVMVNVOVTWKWQVPVTWKXBVPVQVRVS + cdif cuni ssid elequ1 imbi12d spvv mpi reximi eluni2 sylibr adantl ralimi + sseq1 dfss3 ccrd cdm com cvv vex grothac eleqtrri wne ne0i dominf infdif2 + c0 sylan mp3an12i orbi1d imbi2d albidv sylan2 pm5.32i 3bitr4i exbii mpbir + df-3an ) ABFZDGCGZHDBFIDJZEGZWAHZEDFZIZEJZDBGZKZLZCWHMZWAWHHZWHWAUCWANOZC + BFZPZIZCJZQZBRVTWKWLWHWANOZWNPZIZCJZQZBRABCDEUAWRXCBVTWKLZWQLXDXBLWRXCXDW + QXBWKVTWHWHUDZHZWQXBSWKWAXETZCWHMXFWJXGCWHWIXGWBWICDFZDWHKXGWGXHDWHWGWAWA + HZXHWAUEWFXIXHIECECUBWDXIWEXHWCWAWAUOECDUFUGUHUIUJDWAWHUKULUMUNCWHXEUPULV + TXFLZWPXACXJWOWTWLXJWMWSWNWHUQURZTWAXKTXJUSWHNOZWMWSSWHUTXKBVAZVBVCWAUTXK + CVAVBVCVTWHVHVDXFXLWHAGVEWHXMVFVIWHWAVGVJVKVLVMVNVOVTWKWQVSVTWKXBVSVPVQVR $. $( Alternate version of the Tarski-Grothendieck Axiom. ~ ax-ac is used to @@ -112672,14 +112672,14 @@ values in the universe (see ~ gruiun for a more intuitive version). axgroth4 $p |- E. y ( x e. y /\ A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) $= ( vu wel cv wss wi wal wrex wa wral cdif w3a wex weq anbi2i 3bitr2i sseq1 - cdom wbr wo cin wcel axgroth3 elequ2 imbi2d albidv cbvrexv r19.42v elequ1 - imbi12d cbvalvw 19.26 pm4.76 elin imbi2i bitr4i albii rexbii ralbii exbii - 3anbi2i mpbi ) ABGZDHZCHZIZDBGZJZDKZFHZVIIZFDGZJZFKZDBHZLZMZCVSNZVIVSIVSV - IOVIUBUCCBGUDJCKZPZBQVGVJVHVSEHZUEUFZJZDKZEVSLZCVSNZWCPZBQABCDFUGWDWKBWBW - JVGWCWAWICVSWAVMVOFEGZJZFKZEVSLZMVMWNMZEVSLWIVTWOVMVRWNDEVSDERZVQWMFWQVPW - LVODEFUHUIUJUKSVMWNEVSULWPWHEVSWPVMVJDEGZJZDKZMVLWSMZDKWHWNWTVMWMWSFDFDRV - OVJWLWRVNVHVIUAFDEUMUNUOSVLWSDUPXAWGDXAVJVKWRMZJWGVJVKWRUQWFXBVJVHVSWEURU - SUTVATVBTVCVEVDVF $. + cdom wbr wo cin wcel axgroth3 elequ2 imbi2d albidv r19.42v elequ1 imbi12d + cbvalvw 19.26 pm4.76 elin imbi2i bitr4i albii rexbii ralbii 3anbi2i exbii + cbvrexvw mpbi ) ABGZDHZCHZIZDBGZJZDKZFHZVIIZFDGZJZFKZDBHZLZMZCVSNZVIVSIVS + VIOVIUBUCCBGUDJCKZPZBQVGVJVHVSEHZUEUFZJZDKZEVSLZCVSNZWCPZBQABCDFUGWDWKBWB + WJVGWCWAWICVSWAVMVOFEGZJZFKZEVSLZMVMWNMZEVSLWIVTWOVMVRWNDEVSDERZVQWMFWQVP + WLVODEFUHUIUJVESVMWNEVSUKWPWHEVSWPVMVJDEGZJZDKZMVLWSMZDKWHWNWTVMWMWSFDFDR + VOVJWLWRVNVHVIUAFDEULUMUNSVLWSDUOXAWGDXAVJVKWRMZJWGVJVKWRUPWFXBVJVHVSWEUQ + URUSUTTVATVBVCVDVF $. $} ${ @@ -113509,17 +113509,17 @@ divided by the argument (although we don't define full division since we ( vy va vb vm vd vz cnpi wcel ceq wbr cnq wrex wa wi wral wceq clti wn vc cxp cv weq wreu cop elxp2 wel con0 csuc pion suceloni syl vex sucid eleq2 rspcev sylancl adantl elequ2 imbi1d 2ralbidv breq2d rexbidv imbi2d elequ1 - opeq1 opeq2 imbi12d cbvral2v ralbii c2nd cfv rexnal pm4.63 ltpiord ancoms - xp2nd sylan2 adantll anbi2d syl5bb rexbidva syl5bbr w3a c1st xp1st rspccv - wb ralbidv eleq1 syl6 imp syl5 mpdi 1st2nd2 3ad2ant2 mpbird wer enqer a1i - 3imp simpr simpl ertr4d ex reximdv syl5com 3expia impcomd rexlimdva com3r - syl6bi com13 co mulcompi enqbreq anidms mpbiri opelxpi breq1 op2ndd df-nq - cmi notbid elrab2 com12 breq2 elpqn simprbi breq1d rspcva syl2an ad2antrr - rsp fveq2 ad2antlr syl2anc mpbid jca simplbi2 expcom a1dd pm2.61d2 sylbir - sylsyld ralrimivv tfis2 rexlimdv mpd syl5ibrcom rexlimivv anbi12d syl2anr - impd sylbi wo rabeq2i id ersym wor ltsopi sotric mpan notnotb syl6bbr ord - impel oveq2d syl5eq breqan12d bitrd biimpa eqtrd mulcanpi opeq12d 3eqtr4d - mt3d rgen2a vtoclg reu4 sylanbrc ) BIIUBZJZAUCZBKLZAMNZUWFCUCZBKLZOZACUDZ + opeq1 opeq2 imbi12d cbvral2vw ralbii c2nd cfv rexnal pm4.63 xp2nd ltpiord + wb ancoms sylan2 adantll anbi2d syl5bb rexbidva syl5bbr c1st xp1st rspccv + w3a ralbidv eleq1 syl6 imp syl5 mpdi 3imp 1st2nd2 3ad2ant2 mpbird wer a1i + enqer simpr simpl ertr4d ex reximdv syl5com 3expia rexlimdva com3r syl6bi + impcomd com13 cmi co mulcompi enqbreq anidms mpbiri opelxpi op2ndd notbid + breq1 df-nq elrab2 com12 breq2 elpqn fveq2 simprbi breq1d rspcva ad2antrr + rsp syl2an ad2antlr syl2anc mpbid jca simplbi2 sylsyld pm2.61d2 ralrimivv + expcom a1dd sylbir tfis2 impd rexlimdv syl5ibrcom rexlimivv sylbi anbi12d + mpd syl2anr wo rabeq2i ersym impel wor ltsopi sotric mpan notnotb syl6bbr + id ord mt3d oveq2d syl5eq breqan12d bitrd biimpa mulcanpi opeq12d 3eqtr4d + eqtrd rgen2 vtoclg reu4 sylanbrc ) BIIUBZJZAUCZBKLZAMNZUWFCUCZBKLZOZACUDZ PZCMQAMQZUWFAMUEUWDBDUCZEUCZUFZRZEINDINUWGDEBIIUGUWQUWGDEIIUWNIJZUWOIJZOZ UWGUWQUWEUWPKLZAMNZUWTECUHZCUINZUXBUWSUXDUWRUWSUWOUJZUIJZUWOUXEJZUXDUWSUW OUIJUXFUWOUKUWOULUMUWOEUNZUOUXCUXGCUXEUIUWHUXEUWOUPUQURUSUWTUXCUXBCUIUWHU @@ -113530,42 +113530,42 @@ divided by the argument (although we don't define full division since we ZUXRUXMUYIUXBGEFVFUYKUYHUXAAMUYKUYGUWPUWEKUXTUWOUWNVHVCVDVIVJVKUYFUXJDEII UYFUWPHUCZKLZUYLVLVMZUWOSLZTZPZHUWCQZUWTUXJPUWTUYRTZUYFUXJUWTUYSUYMUYNUWO JZOZHUWCNZUYFUXJPUYSUYQTZHUWCNUWTVUBUYQHUWCVNUWTVUCVUAHUWCVUCUYMUYOOUWTUY - LUWCJZOZVUAUYMUYOVOVUEUYOUYTUYMUWSVUDUYOUYTWIZUWRVUDUWSUYNIJZVUFUYLIIVRZV - UGUWSVUFUYNUWOVPVQVSVTWAWBWCWDUYFUXCVUBUXBUYFUXCVUBUXBPUYFUXCOZVUAUXBHUWC - VUIVUDOUYTUYMUXBVUIVUDUYTUYMUXBPVUIVUDUYTWEZUWEUYLKLZAMNZUYMUXBVUJVULUWEU + LUWCJZOZVUAUYMUYOVOVUEUYOUYTUYMUWSVUDUYOUYTVRZUWRVUDUWSUYNIJZVUFUYLIIVPZV + UGUWSVUFUYNUWOVQVSVTWAWBWCWDWEUYFUXCVUBUXBUYFUXCVUBUXBPUYFUXCOZVUAUXBHUWC + VUIVUDOUYTUYMUXBVUIVUDUYTUYMUXBPVUIVUDUYTWIZUWEUYLKLZAMNZUYMUXBVUJVULUWEU YLWFVMZUYNUFZKLZAMNZVUIVUDUYTVUPVUIVUDVUGUYTVUPPZVUHVUDVUMIJZVUIVUGVUQPZU YLIIWGUYFUXCVURVUSPZUYFUXCGEUHZUYCPZGIQZUAIQZVUTUYEVVDFUWOUWHFEUDZUYDVVBU AGIIVVEUXRVVAUYCFEGUTVAVBWHVVDVURVVAUWEVUMUXTUFZKLZAMNZPZGIQZVUSVVCVVJUAV UMIUXSVUMRZVVBVVIGIVVKUYCVVHVVAVVKUYBVVGAMVVKUYAVVFUWEKUXSVUMUXTVGVCVDVEW JWHVVIVUQGUYNIUXTUYNRZVVAUYTVVHVUPUXTUYNUWOWKVVLVVGVUOAMVVLVVFVUNUWEKUXTU - YNVUMVHVCVDVIWHWLWLWMWNWOXBVUDVUIVULVUPWIUYTVUDVUKVUOAMVUDUYLVUNUWEKUYLII - WPVCVDWQWRUYMVUKUXAAMUYMVUKUXAUYMVUKOZUWEUYLUWPKUWCUWCKWSZVVMWTXAUYMVUKXC - UYMVUKXDXEXFXGXHXIXJXKXFXLXMXNUYRUWTUXBUXCUWTUYRUXBUWTUWPUWPKLZUYRUWPMJZU - XBUWTVVOUWNUWOYDXOUWOUWNYDXORZUWNUWOXPUWTVVOVVQWIUWNUWOUWNUWOXQXRXSUWTUWP - UWCJZUYRVVPPUWNUWOIIXTVVPVVRUYRUWHUYLKLZUYNUWHVLVMZSLZTZPZHUWCQZUYRCUWPUW - CMUWHUWPRZVWCUYQHUWCVWEVVSUYMVWBUYPUWHUWPUYLKYAVWEVWAUYOVWEVVTUWOUYNSUWNU - WOUWHDUNUXHYBVCYEVIWJCHYCZYFUUAUMVVPVVOUXBUXAVVOAUWPMUWEUWPUWPKYAUQUUBUUF - YGUUCUUDUUGUUEXAUUHUXKDIYOUMUXJEIYOWLUUOYGUUIUUJUWQUWFUXAAMBUWPUWEKYHVDUU - KUULUUPUWEUWNKLZUWHUWNKLZOZUWKPZCMQAMQUWMDBUWCUWNBRZVWJUWLACMMVWKVWIUWJUW - KVWKVWGUWFVWHUWIUWNBUWEKYHUWNBUWHKYHUUMVAVBVWJACMVWIUWEUWHKLZUWEMJZUWHMJZ - OZUWKVWIUWEUWNUWHKUWCVVNVWIWTXAVWGVWHXDVWGVWHXCXEVWOVWLUWKVWOVWLOZUWEWFVM - ZUWEVLVMZUFZUWHWFVMZVVTUFZUWEUWHVWPVWQVWTVWRVVTVWPVWRVWQYDXOZVWRVWTYDXOZR - ZVWQVWTRZVWPVXBVWQVVTYDXOZVXCVWPVXBVWQVWRYDXOVXFVWRVWQXPVWPVWRVVTVWQYDVWP - VWRVVTRZVVTVWRSLZVWOVWLVXHTZVWNUWHUWCJZVUKUYNVWRSLZTZPZHUWCQZVWLVXIPZVWMU - WHYIZVWMUWEUWCJZVXNVWDVXNCUWEUWCMCAUDZVWCVXMHUWCVXRVVSVUKVWBVXLUWHUWEUYLK - YAVXRVWAVXKVXRVVTVWRUYNSUWHUWEVLYPVCYEVIWJVWFYFYJVXMVXOHUWHUWCHCUDZVUKVWL - VXLVXIUYLUWHUWEKYHVXSVXKVXHVXSUYNVVTVWRSUYLUWHVLYPYKYEVIYLUUNWMVWPVXGVXHV - WPVWRVVTSLZTZVXGVXHUUQZVWOUWHUWEKLZVYAVWLVWMVXQVWDVYCVYAPZVWNUWEYIZVWNVXJ - VWDVWDCMUWCVWFUURYJVWCVYDHUWEUWCHAUDZVVSVYCVWBVYAUYLUWEUWHKYHVYFVWAVXTVYF - UYNVWRVVTSUYLUWEVLYPYKYEVIYLYMVWLUWEUWHKUWCVVNVWLWTXAVWLUUSUUTUVHVWPVWRIJ - ZVVTIJZVYAVYBWIVWMVYGVWNVWLVWMVXQVYGVYEUWEIIVRZUMYNVWNVYHVWMVWLVWNVXJVYHV - XPUWHIIVRZUMYQVYGVYHOZVYAVYBTZTVYBVYKVXTVYLISUVAVYKVXTVYLWIUVBIVWRVVTSUVC - UVDYEVYBUVEUVFYRYSUVGUVRZUVIUVJVWOVWLVXFVXCRZVWMVXQVXJVWLVYNWIVWNVYEVXPVX - QVXJOVWLVWSVXAKLZVYNVXQVXJUWEVWSUWHVXAKUWEIIWPZUWHIIWPZUVKVXQVWQIJZVYGOVW - TIJZVYHOVYOVYNWIVXJVXQVYRVYGUWEIIWGZVYIYTVXJVYSVYHUWHIIWGVYJYTVWQVWRVWTVV - TXQYMUVLYMUVMUVNVWPVXQVXDVXEWIZVWMVXQVWNVWLVYEYNZVXQVYGVYRWUAVYIVYTVWRVWQ - VWTUVOYRUMYSVYMUVPVWPVXQUWEVWSRWUBVYPUMVWPVXJUWHVXARVWNVXJVWMVWLVXPYQVYQU - MUVQXFWNUVSUVTUWFUWIACMUWEUWHBKYAUWAUWB $. + YNVUMVHVCVDVIWHWLWLWMWNWOWPVUDVUIVULVUPVRUYTVUDVUKVUOAMVUDUYLVUNUWEKUYLII + WQVCVDWRWSUYMVUKUXAAMUYMVUKUXAUYMVUKOZUWEUYLUWPKUWCUWCKWTZVVMXBXAUYMVUKXC + UYMVUKXDXEXFXGXHXIXMXJXFXKXLXNUYRUWTUXBUXCUWTUYRUXBUWTUWPUWPKLZUYRUWPMJZU + XBUWTVVOUWNUWOXOXPUWOUWNXOXPRZUWNUWOXQUWTVVOVVQVRUWNUWOUWNUWOXRXSXTUWTUWP + UWCJZUYRVVPPUWNUWOIIYAVVPVVRUYRUWHUYLKLZUYNUWHVLVMZSLZTZPZHUWCQZUYRCUWPUW + CMUWHUWPRZVWCUYQHUWCVWEVVSUYMVWBUYPUWHUWPUYLKYDVWEVWAUYOVWEVVTUWOUYNSUWNU + WOUWHDUNUXHYBVCYCVIWJCHYEZYFUUAUMVVPVVOUXBUXAVVOAUWPMUWEUWPUWPKYDUQUUEUUB + YGUUFUUCUUDUUGXAUUHUXKDIYOUMUXJEIYOWLUUIYGUUJUUOUWQUWFUXAAMBUWPUWEKYHVDUU + KUULUUMUWEUWNKLZUWHUWNKLZOZUWKPZCMQAMQUWMDBUWCUWNBRZVWJUWLACMMVWKVWIUWJUW + KVWKVWGUWFVWHUWIUWNBUWEKYHUWNBUWHKYHUUNVAVBVWJACMMVWIUWEUWHKLZUWEMJZUWHMJ + ZOZUWKVWIUWEUWNUWHKUWCVVNVWIXBXAVWGVWHXDVWGVWHXCXEVWOVWLUWKVWOVWLOZUWEWFV + MZUWEVLVMZUFZUWHWFVMZVVTUFZUWEUWHVWPVWQVWTVWRVVTVWPVWRVWQXOXPZVWRVWTXOXPZ + RZVWQVWTRZVWPVXBVWQVVTXOXPZVXCVWPVXBVWQVWRXOXPVXFVWRVWQXQVWPVWRVVTVWQXOVW + PVWRVVTRZVVTVWRSLZVWOVWLVXHTZVWNUWHUWCJZVUKUYNVWRSLZTZPZHUWCQZVWLVXIPZVWM + UWHYIZVWMUWEUWCJZVXNVWDVXNCUWEUWCMCAUDZVWCVXMHUWCVXRVVSVUKVWBVXLUWHUWEUYL + KYDVXRVWAVXKVXRVVTVWRUYNSUWHUWEVLYJVCYCVIWJVWFYFYKVXMVXOHUWHUWCHCUDZVUKVW + LVXLVXIUYLUWHUWEKYHVXSVXKVXHVXSUYNVVTVWRSUYLUWHVLYJYLYCVIYMUUPWMVWPVXGVXH + VWPVWRVVTSLZTZVXGVXHUUQZVWOUWHUWEKLZVYAVWLVWMVXQVWDVYCVYAPZVWNUWEYIZVWNVX + JVWDVWDCMUWCVWFUURYKVWCVYDHUWEUWCHAUDZVVSVYCVWBVYAUYLUWEUWHKYHVYFVWAVXTVY + FUYNVWRVVTSUYLUWEVLYJYLYCVIYMYPVWLUWEUWHKUWCVVNVWLXBXAVWLUVGUUSUUTVWPVWRI + JZVVTIJZVYAVYBVRVWMVYGVWNVWLVWMVXQVYGVYEUWEIIVPZUMYNVWNVYHVWMVWLVWNVXJVYH + VXPUWHIIVPZUMYQVYGVYHOZVYAVYBTZTVYBVYKVXTVYLISUVAVYKVXTVYLVRUVBIVWRVVTSUV + CUVDYCVYBUVEUVFYRYSUVHUVIZUVJUVKVWOVWLVXFVXCRZVWMVXQVXJVWLVYNVRVWNVYEVXPV + XQVXJOVWLVWSVXAKLZVYNVXQVXJUWEVWSUWHVXAKUWEIIWQZUWHIIWQZUVLVXQVWQIJZVYGOV + WTIJZVYHOVYOVYNVRVXJVXQVYRVYGUWEIIWGZVYIYTVXJVYSVYHUWHIIWGVYJYTVWQVWRVWTV + VTXRYPUVMYPUVNUVRVWPVXQVXDVXEVRZVWMVXQVWNVWLVYEYNZVXQVYGVYRWUAVYIVYTVWRVW + QVWTUVOYRUMYSVYMUVPVWPVXQUWEVWSRWUBVYPUMVWPVXJUWHVXARVWNVXJVWMVWLVXPYQVYQ + UMUVQXFWNUVSUVTUWFUWIACMUWEUWHBKYDUWAUWB $. $} ${ @@ -113759,11 +113759,11 @@ divided by the argument (although we don't define full division since we (New usage is discouraged.) $) addpqf $p |- +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) $= ( vx vy cv c1st cfv c2nd cmi co cpli cop cnpi wcel wral cplpq xp1st xp2nd - cxp wf mulclpi syl2an syl2anr addclpi syl2anc opelxpd rgen2a df-plpq fmpo + cxp wf mulclpi syl2an syl2anr addclpi syl2anc opelxpd rgen2 df-plpq fmpo wa mpbi ) ACZDEZBCZFEZGHZULDEZUJFEZGHZIHZUPUMGHZJZKKQZLZBVAMAVAMVAVAQVANR - VBABVAUJVALZULVALZUHZURUSKKVEUNKLZUQKLZURKLVCUKKLUMKLZVFVDUJKKOULKKPZUKUM - STVDUOKLUPKLZVGVCULKKOUJKKPZUOUPSUAUNUQUBUCVCVJVHUSKLVDVKVIUPUMSTUDUEABVA - VAUTVANABUFUGUI $. + VBABVAVAUJVALZULVALZUHZURUSKKVEUNKLZUQKLZURKLVCUKKLUMKLZVFVDUJKKOULKKPZUK + UMSTVDUOKLUPKLZVGVCULKKOUJKKPZUOUPSUAUNUQUBUCVCVJVHUSKLVDVKVIUPUMSTUDUEAB + VAVAUTVANABUFUGUI $. $( Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) @@ -113778,9 +113778,9 @@ divided by the argument (although we don't define full division since we (New usage is discouraged.) $) mulpqf $p |- .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) $= ( vx vy cv c1st cfv cmi co c2nd cop cnpi cxp wcel wral cmpq wf wa mulclpi - xp1st syl2an xp2nd opelxpd rgen2a df-mpq fmpo mpbi ) ACZDEZBCZDEZFGZUFHEZ - UHHEZFGZIZJJKZLZBUOMAUOMUOUOKUONOUPABUOUFUOLZUHUOLZPUJUMJJUQUGJLUIJLUJJLU - RUFJJRUHJJRUGUIQSUQUKJLULJLUMJLURUFJJTUHJJTUKULQSUAUBABUOUOUNUONABUCUDUE + xp1st syl2an xp2nd opelxpd rgen2 df-mpq fmpo mpbi ) ACZDEZBCZDEZFGZUFHEZU + HHEZFGZIZJJKZLZBUOMAUOMUOUOKUONOUPABUOUOUFUOLZUHUOLZPUJUMJJUQUGJLUIJLUJJL + URUFJJRUHJJRUGUIQSUQUKJLULJLUMJLURUFJJTUHJJTUKULQSUAUBABUOUOUNUONABUCUDUE $. $( Closure of multiplication on positive fractions. (Contributed by NM, @@ -114599,16 +114599,16 @@ divided by the argument (although we don't define full division since we { f | E. g e. A E. h e. B f = ( g G h ) } ) $= ( cnp wcel cv wceq wrex cnq wa cab oveq1 rexeq abbidv eqeq12d rexbidv cvv co oveq2 wss wi elprnq eleq1 syl5ibrcom syl2an an4s rexlimdvva nqex ssexg - abssdv sylancl weq ovmpog mpd3an3 vtocl2ga eqeq1 2rexbidv eqeq2d cbvrex2v - syl6bb cbvabv syl6eq ) FOPGOPUAFGKUIZAQZBQZCQZLUIZRZCGSZBFSZAUBZHQZIQZJQZ - LUIZRZJGSIFSZHUBWCWDKUIZVSCWDSZBWCSZAUBZRZFWDKUIZWJBFSZAUBZRVNWBRHIFGOOWC - FRZWIWNWLWPWCFWDKUCWQWKWOAWJBWCFUDUEUFWDGRZWNVNWPWBWDGFKUJWRWOWAAWRWJVTBF - VSCWDGUDUGUEUFWCOPZWDOPZWLUHPZWMWSWTUAZWLTUKTUHPXAXBWKATXBVSVOTPZBCWCWDWS - VPWCPZWTVQWDPZVSXCULZWSXDUAVPTPZVQTPZXFWTXEUAWCVPUMWDVQUMXGXHUAXCVSVRTPNV - OVRTUNUOUPUQURVAUSWLTUHUTVBDEWCWDOOVSCEQZSZBDQZSZAUBWLKXJBWCSZAUBUHDHVCXL - XMAXJBXKWCUDUEEIVCZXMWKAXNXJWJBWCVSCXIWDUDUGUEMVDVEVFWAWHAHAHVCZWAWCVRRZC - GSBFSWHXOVSXPBCFGVOWCVRVGVHXPWGWCWDVQLUIZRBCIJFGBIVCVRXQWCVPWDVQLUCVICJVC - XQWFWCVQWEWDLUJVIVJVKVLVM $. + abssdv sylancl weq ovmpog vtocl2ga eqeq1 2rexbidv eqeq2d cbvrex2vw syl6bb + mpd3an3 cbvabv syl6eq ) FOPGOPUAFGKUIZAQZBQZCQZLUIZRZCGSZBFSZAUBZHQZIQZJQ + ZLUIZRZJGSIFSZHUBWCWDKUIZVSCWDSZBWCSZAUBZRZFWDKUIZWJBFSZAUBZRVNWBRHIFGOOW + CFRZWIWNWLWPWCFWDKUCWQWKWOAWJBWCFUDUEUFWDGRZWNVNWPWBWDGFKUJWRWOWAAWRWJVTB + FVSCWDGUDUGUEUFWCOPZWDOPZWLUHPZWMWSWTUAZWLTUKTUHPXAXBWKATXBVSVOTPZBCWCWDW + SVPWCPZWTVQWDPZVSXCULZWSXDUAVPTPZVQTPZXFWTXEUAWCVPUMWDVQUMXGXHUAXCVSVRTPN + VOVRTUNUOUPUQURVAUSWLTUHUTVBDEWCWDOOVSCEQZSZBDQZSZAUBWLKXJBWCSZAUBUHDHVCX + LXMAXJBXKWCUDUEEIVCZXMWKAXNXJWJBWCVSCXIWDUDUGUEMVDVKVEWAWHAHAHVCZWAWCVRRZ + CGSBFSWHXOVSXPBCFGVOWCVRVFVGXPWGWCWDVQLUIZRBCIJFGBIVCVRXQWCVPWDVQLUCVHCJV + CXQWFWCVQWEWDLUJVHVIVJVLVM $. $( Membership in value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario @@ -114634,11 +114634,11 @@ divided by the argument (although we don't define full division since we (New usage is discouraged.) $) genpdm $p |- dom F = ( P. X. P. ) $= ( cv co wceq wrex cvv wcel cnp wral wa cnq elprnq cab wi eleq1 syl5ibrcom - cxp wfn cdm syl2an an4s rexlimdvva abssdv nqex ssexg sylancl rgen2a fnmpo - wss fndm mp2b ) AJZBJZCJZGKZLZCEJZMBDJZMZAUAZNOZEPQDPQFPPUEZUFFUGVJLVIDEP - VFPOZVEPOZRZVHSUQSNOVIVMVGASVMVDUTSOZBCVFVEVKVAVFOZVLVBVEOZVDVNUBZVKVORVA - SOZVBSOZVQVLVPRVFVATVEVBTVRVSRVNVDVCSOIUTVCSUCUDUHUIUJUKULVHSNUMUNUODEPPV - HFNHUPVJFURUS $. + cxp wfn cdm wss syl2an an4s rexlimdvva abssdv nqex ssexg rgen2 fnmpo fndm + sylancl mp2b ) AJZBJZCJZGKZLZCEJZMBDJZMZAUAZNOZEPQDPQFPPUEZUFFUGVJLVIDEPP + VFPOZVEPOZRZVHSUHSNOVIVMVGASVMVDUTSOZBCVFVEVKVAVFOZVLVBVEOZVDVNUBZVKVORVA + SOZVBSOZVQVLVPRVFVATVEVBTVRVSRVNVDVCSOIUTVCSUCUDUIUJUKULUMVHSNUNURUODEPPV + HFNHUPVJFUQUS $. $( The result of an operation on positive reals is not empty. (Contributed by NM, 28-Feb-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) @@ -115787,21 +115787,21 @@ B C_ ( A +P. C ) ) $= ( vq vs cnp cer wcel wa cv cop cec wceq cpp co wex vf cxp cqs wal wmo wer vg vh wi enrer a1i wbr prsrlem1 addcmpblnr imp syl erthi adantrlr simprlr adantrrr simprrr 3eqtr4d expr exlimdvv impd alrimivv opeq12 eceq1d eqeq2d - ex anbi1d simpl oveq1d simpr opeq12d anbi12d anbi2d oveq2d cbvex4v anbi2i - imbi1i 2albii sylibr eqeq1 4exbidv mo4 ) FJJUBZKUCZLGWHLMZFBNZCNZOZKPZQZG - DNZENZOZKPZQZMZANZWJWORSZWKWPRSZOZKPZQZMZETDTZCTBTZWTHNZXEQZMZETDTCTBTZMZ - XAXJQZUIZHUDAUDZXIAUEWIXIFINZUANZOZKPZQZGUGNZUHNZOZKPZQZMZXJXRYCRSZXSYDRS - ZOZKPZQZMZUHTUGTZUATITZMZXOUIZHUDAUDXQWIYRAHWIXIYPXOWIXHYPXOUIZBCWIXGYSDE - WIXGYSWIXGMZYOXOIUAYTYNXOUGUHWIXGYNXOWIXGYNMMXEYLXAXJWIXGYHXEYLQZYMWIWTYH - UUAXFWIWTYHMMZXDYKKWGWGKUFUUBUJUKUUBWJJLWKJLMXRJLXSJLMMWOJLWPJLMYCJLYDJLM - MMZWJXSRSWKXRRSQWOYDRSWPYCRSQMZMXDYKKULZBCDEFGUAUGUHIUMUUCUUDUUEWJWKXRXSY - CYDWOWPUNUOUPUQURUTWIWTXFYNUSWIXGYHYMVAVBVCVDVDVJVDVDVEVFXPYRAHXNYQXOXMYP - XIXLYBWSMZXJXRWORSZXSWPRSZOZKPZQZMYNBCDEIUAUGUHWJXRQZWKXSQZMZWTUUFXKUUKUU - NWNYBWSUUNWMYAFUUNWLXTKWJWKXRXSVGVHVIVKUUNXEUUJXJUUNXDUUIKUUNXBUUGXCUUHUU - NWJXRWORUULUUMVLVMUUNWKXSWPRUULUUMVNVMVOVHVIVPWOYCQZWPYDQZMZUUFYHUUKYMUUQ - WSYGYBUUQWRYFGUUQWQYEKWOWPYCYDVGVHVIVQUUQUUJYLXJUUQUUIYKKUUQUUGYIUUHYJUUQ - WOYCXRRUUOUUPVLVRUUQWPYDXSRUUOUUPVNVRVOVHVIVPVSVTWAWBWCXIXMAHXOXGXLBCDEXO - XFXKWTXAXJXEWDVQWEWFWC $. + ex anbi1d simpl oveq1d simpr opeq12d anbi2d oveq2d cbvex4vw anbi2i imbi1i + anbi12d 2albii sylibr eqeq1 4exbidv mo4 ) FJJUBZKUCZLGWHLMZFBNZCNZOZKPZQZ + GDNZENZOZKPZQZMZANZWJWORSZWKWPRSZOZKPZQZMZETDTZCTBTZWTHNZXEQZMZETDTCTBTZM + ZXAXJQZUIZHUDAUDZXIAUEWIXIFINZUANZOZKPZQZGUGNZUHNZOZKPZQZMZXJXRYCRSZXSYDR + SZOZKPZQZMZUHTUGTZUATITZMZXOUIZHUDAUDXQWIYRAHWIXIYPXOWIXHYPXOUIZBCWIXGYSD + EWIXGYSWIXGMZYOXOIUAYTYNXOUGUHWIXGYNXOWIXGYNMMXEYLXAXJWIXGYHXEYLQZYMWIWTY + HUUAXFWIWTYHMMZXDYKKWGWGKUFUUBUJUKUUBWJJLWKJLMXRJLXSJLMMWOJLWPJLMYCJLYDJL + MMMZWJXSRSWKXRRSQWOYDRSWPYCRSQMZMXDYKKULZBCDEFGUAUGUHIUMUUCUUDUUEWJWKXRXS + YCYDWOWPUNUOUPUQURUTWIWTXFYNUSWIXGYHYMVAVBVCVDVDVJVDVDVEVFXPYRAHXNYQXOXMY + PXIXLYBWSMZXJXRWORSZXSWPRSZOZKPZQZMYNBCDEIUAUGUHWJXRQZWKXSQZMZWTUUFXKUUKU + UNWNYBWSUUNWMYAFUUNWLXTKWJWKXRXSVGVHVIVKUUNXEUUJXJUUNXDUUIKUUNXBUUGXCUUHU + UNWJXRWORUULUUMVLVMUUNWKXSWPRUULUUMVNVMVOVHVIWAWOYCQZWPYDQZMZUUFYHUUKYMUU + QWSYGYBUUQWRYFGUUQWQYEKWOWPYCYDVGVHVIVPUUQUUJYLXJUUQUUIYKKUUQUUGYIUUHYJUU + QWOYCXRRUUOUUPVLVQUUQWPYDXSRUUOUUPVNVQVOVHVIWAVRVSVTWBWCXIXMAHXOXGXLBCDEX + OXFXKWTXAXJXEWDVPWEWFWC $. $( There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) $) @@ -115813,24 +115813,24 @@ B C_ ( A +P. C ) ) $= ( vq cnp cer wcel wa cv cop cec wceq cmp co cpp wex vs vf cxp cqs wal wmo vg vh wi wer enrer a1i wbr prsrlem1 mulcmpblnr imp erthi adantrlr simprlr syl adantrrr simprrr 3eqtr4d expr exlimdvv ex impd alrimivv opeq12 eceq1d - eqeq2d anbi1d oveq1d oveq12d opeq12d anbi12d anbi2d oveq2d cbvex4v anbi2i - simpl simpr imbi1i 2albii sylibr eqeq1 4exbidv mo4 ) FIIUCZJUDZKGWJKLZFBM - ZCMZNZJOZPZGDMZEMZNZJOZPZLZAMZWLWQQRZWMWRQRZSRZWLWRQRZWMWQQRZSRZNZJOZPZLZ - ETDTZCTBTZXBHMZXKPZLZETDTCTBTZLZXCXPPZUIZHUEAUEZXOAUFWKXOFUAMZUBMZNZJOZPZ - GUGMZUHMZNZJOZPZLZXPYDYIQRZYEYJQRZSRZYDYJQRZYEYIQRZSRZNZJOZPZLZUHTUGTZUBT - UATZLZYAUIZHUEAUEYCWKUUHAHWKXOUUFYAWKXNUUFYAUIZBCWKXMUUIDEWKXMUUIWKXMLZUU - EYAUAUBUUJUUDYAUGUHWKXMUUDYAWKXMUUDLLXKUUBXCXPWKXMYNXKUUBPZUUCWKXBYNUUKXL - WKXBYNLLZXJUUAJWIWIJUJUULUKULUULWLIKWMIKLYDIKYEIKLLWQIKWRIKLYIIKYJIKLLLZW - LYESRWMYDSRPWQYJSRWRYISRPLZLXJUUAJUMZBCDEFGUBUGUHUAUNUUMUUNUUOWLWMYDYEYIY - JWQWRUOUPUTUQURVAWKXBXLUUDUSWKXMYNUUCVBVCVDVEVEVFVEVEVGVHYBUUHAHXTUUGYAXS - UUFXOXRYHXALZXPYDWQQRZYEWRQRZSRZYDWRQRZYEWQQRZSRZNZJOZPZLUUDBCDEUAUBUGUHW - LYDPZWMYEPZLZXBUUPXQUVEUVHWPYHXAUVHWOYGFUVHWNYFJWLWMYDYEVIVJVKVLUVHXKUVDX - PUVHXJUVCJUVHXFUUSXIUVBUVHXDUUQXEUURSUVHWLYDWQQUVFUVGWAZVMUVHWMYEWRQUVFUV - GWBZVMVNUVHXGUUTXHUVASUVHWLYDWRQUVIVMUVHWMYEWQQUVJVMVNVOVJVKVPWQYIPZWRYJP - ZLZUUPYNUVEUUCUVMXAYMYHUVMWTYLGUVMWSYKJWQWRYIYJVIVJVKVQUVMUVDUUBXPUVMUVCU - UAJUVMUUSYQUVBYTUVMUUQYOUURYPSUVMWQYIYDQUVKUVLWAZVRUVMWRYJYEQUVKUVLWBZVRV - NUVMUUTYRUVAYSSUVMWRYJYDQUVOVRUVMWQYIYEQUVNVRVNVOVJVKVPVSVTWCWDWEXOXSAHYA - XMXRBCDEYAXLXQXBXCXPXKWFVQWGWHWE $. + eqeq2d anbi1d simpl oveq1d oveq12d opeq12d anbi12d anbi2d oveq2d cbvex4vw + simpr anbi2i imbi1i 2albii sylibr eqeq1 4exbidv mo4 ) FIIUCZJUDZKGWJKLZFB + MZCMZNZJOZPZGDMZEMZNZJOZPZLZAMZWLWQQRZWMWRQRZSRZWLWRQRZWMWQQRZSRZNZJOZPZL + ZETDTZCTBTZXBHMZXKPZLZETDTCTBTZLZXCXPPZUIZHUEAUEZXOAUFWKXOFUAMZUBMZNZJOZP + ZGUGMZUHMZNZJOZPZLZXPYDYIQRZYEYJQRZSRZYDYJQRZYEYIQRZSRZNZJOZPZLZUHTUGTZUB + TUATZLZYAUIZHUEAUEYCWKUUHAHWKXOUUFYAWKXNUUFYAUIZBCWKXMUUIDEWKXMUUIWKXMLZU + UEYAUAUBUUJUUDYAUGUHWKXMUUDYAWKXMUUDLLXKUUBXCXPWKXMYNXKUUBPZUUCWKXBYNUUKX + LWKXBYNLLZXJUUAJWIWIJUJUULUKULUULWLIKWMIKLYDIKYEIKLLWQIKWRIKLYIIKYJIKLLLZ + WLYESRWMYDSRPWQYJSRWRYISRPLZLXJUUAJUMZBCDEFGUBUGUHUAUNUUMUUNUUOWLWMYDYEYI + YJWQWRUOUPUTUQURVAWKXBXLUUDUSWKXMYNUUCVBVCVDVEVEVFVEVEVGVHYBUUHAHXTUUGYAX + SUUFXOXRYHXALZXPYDWQQRZYEWRQRZSRZYDWRQRZYEWQQRZSRZNZJOZPZLUUDBCDEUAUBUGUH + WLYDPZWMYEPZLZXBUUPXQUVEUVHWPYHXAUVHWOYGFUVHWNYFJWLWMYDYEVIVJVKVLUVHXKUVD + XPUVHXJUVCJUVHXFUUSXIUVBUVHXDUUQXEUURSUVHWLYDWQQUVFUVGVMZVNUVHWMYEWRQUVFU + VGWAZVNVOUVHXGUUTXHUVASUVHWLYDWRQUVIVNUVHWMYEWQQUVJVNVOVPVJVKVQWQYIPZWRYJ + PZLZUUPYNUVEUUCUVMXAYMYHUVMWTYLGUVMWSYKJWQWRYIYJVIVJVKVRUVMUVDUUBXPUVMUVC + UUAJUVMUUSYQUVBYTUVMUUQYOUURYPSUVMWQYIYDQUVKUVLVMZVSUVMWRYJYEQUVKUVLWAZVS + VOUVMUUTYRUVAYSSUVMWRYJYDQUVOVSUVMWQYIYEQUVNVSVOVPVJVKVQVTWBWCWDWEXOXSAHY + AXMXRBCDEYAXLXQXBXCXPXKWFVRWGWHWE $. $} ${ @@ -116715,15 +116715,15 @@ the converse membership relation (which is not an equivalence relation) wa wf wfn wfun cdm coprab wmo moeq mosubop anass 2exbii bitri mobii mpbir 19.42vv moani funoprab df-add funeqi dmeqi dmoprabss eqsstri oveq1 eleq1d 0ncn df-c oveq2 addcnsr addclsr anim12i opelxpi eqeltrd 2optocl syl6eleqr - an4s syl oprssdm eqssi df-fn mpbir2an rgen2a ffnov ) HHIZHJUAJWBUBZAKZBKZ - JLZHMZBHNAHNWCJUCZJUDZWBOWHWDHMWEHMTZWDCKZDKZPOZWEEKZFKZPOZTGKZWKWNQLZWLW - OQLPZOZTZFRERZDRCRZTZABGUEZUCXDABGXCWJGXCGUFWMWPWTTZFRERZTZDRCRZGUFXGGCDW - DWTGEFWEGWSUGUHUHXCXIGXBXHCDXBWMXFTZFRERXHXAXJEFWMWPWTUIUJWMXFEFUNUKUJULU - MUOUPJXEABGCDEFUQZURUMWIWBWIXEUDWBJXEXKUSXCABGHHUTVAABHJVDWJWFSSIZHWQWKPZ - WLWNPZJLZXLMWDXNJLZXLMWFXLMGCDEWDWESSHVEXMWDOXOXPXLXMWDXNJVBVCXNWEOXPWFXL - XNWEWDJVFVCWQSMZWKSMZTWLSMZWNSMZTTZXOWQWLQLZWRPZXLWQWKWLWNVGYAYBSMZWRSMZT - ZYCXLMXQXSXRXTYFXQXSTYDXRXTTYEWQWLVHWKWNVHVIVNYBWRSSVJVOVKVLVEVMZVPVQJWBV - RVSWGABHYGVTABHHHJWAVS $. + an4s syl oprssdm eqssi df-fn mpbir2an rgen2 ffnov ) HHIZHJUAJWBUBZAKZBKZJ + LZHMZBHNAHNWCJUCZJUDZWBOWHWDHMWEHMTZWDCKZDKZPOZWEEKZFKZPOZTGKZWKWNQLZWLWO + QLPZOZTZFRERZDRCRZTZABGUEZUCXDABGXCWJGXCGUFWMWPWTTZFRERZTZDRCRZGUFXGGCDWD + WTGEFWEGWSUGUHUHXCXIGXBXHCDXBWMXFTZFRERXHXAXJEFWMWPWTUIUJWMXFEFUNUKUJULUM + UOUPJXEABGCDEFUQZURUMWIWBWIXEUDWBJXEXKUSXCABGHHUTVAABHJVDWJWFSSIZHWQWKPZW + LWNPZJLZXLMWDXNJLZXLMWFXLMGCDEWDWESSHVEXMWDOXOXPXLXMWDXNJVBVCXNWEOXPWFXLX + NWEWDJVFVCWQSMZWKSMZTWLSMZWNSMZTTZXOWQWLQLZWRPZXLWQWKWLWNVGYAYBSMZWRSMZTZ + YCXLMXQXSXRXTYFXQXSTYDXRXTTYEWQWLVHWKWNVHVIVNYBWRSSVJVOVKVLVEVMZVPVQJWBVR + VSWGABHHYGVTABHHHJWAVS $. $( Multiplication is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less @@ -116735,7 +116735,7 @@ the converse membership relation (which is not an equivalence relation) cm1r cxp wf wfn wral wfun cdm cplr coprab wmo moeq mosubop 2exbii 19.42vv anass bitri mobii mpbir moani funoprab df-mul funeqi dmeqi dmoprabss 0ncn eqsstri df-c oveq1 eleq1d mulcnsr m1r sylancr addclsr syl2an an4s syl2anr - oveq2 an42s opelxpd eqeltrd 2optocl syl6eleqr eqssi df-fn mpbir2an rgen2a + oveq2 an42s opelxpd eqeltrd 2optocl syl6eleqr eqssi df-fn mpbir2an rgen2 oprssdm ffnov ) HHUAZHIUBIWHUCZAJZBJZIKZHLZBHUDAHUDWIIUEZIUFZWHMWNWJHLWKH LNZWJCJZDJZOMZWKEJZFJZOMZNGJZWQWTPKZTWRXAPKPKUGKWRWTPKWQXAPKUGKOZMZNZFQEQ ZDQCQZNZABGUHZUEXJABGXIWPGXIGUIWSXBXFNZFQEQZNZDQCQZGUIXMGCDWJXFGEFWKGXEUJ @@ -116745,7 +116745,7 @@ the converse membership relation (which is not an equivalence relation) CRLZWQRLZNWRRLZWTRLZNNZYAXCWRPKZTXDPKZUGKZWQWRPKZXCWTPKZUGKZOXRXCWQWRWTVI YGYJYMRRYCYEYDYFYJRLZYCYENYHRLYIRLZYNYDYFNZXCWRSYPTRLXDRLYOVJWQWTSTXDSVKY HYIVLVMVNYCYFYDYEYMRLZYDYENYKRLYLRLYQYCYFNWQWRSXCWTSYKYLVLVOVQVRVSVTVFWAZ - WFWBIWHWCWDWMABHYRWEABHHHIWGWD $. + WFWBIWHWCWDWMABHHYRWEABHHHIWGWD $. $} $( The complex numbers form a set. This axiom is redundant in the presence @@ -118696,31 +118696,31 @@ this axiom (with the defined operation in place of ` x. ` ) follows as a dedekind $p |- ( ( A C_ RR /\ B C_ RR /\ A. x e. A A. y e. B x < y ) -> E. z e. RR A. x e. A A. y e. B ( x <_ z /\ z <_ y ) ) $= ( vw cr cv clt wbr wral cle wa wrex wi c0 wcel nfv wceq c1 wss wne w3a wn - nfra1 nf3an nfan nfra2 simpl2l sselda simplrl simprrl r19.21bi ex simprll - nltled simp2r simpr ssel2 syl2an simpl3 simp2 com12 adantl adantlr simplr - rsp ltnsym syl2an2r syld an32s ralimdva breq2 notbid cbvralv sylib ralnex - mpd rexbidv imbi12d simplrr rspcdva mtod expr anim12d expd ralrimd simp2l - breq1 ralrimi simp1l simp1r n0 sseld ralcom ralbidv rspccv sylbi 3ad2ant3 - wex jcad eximdv df-rex sylibr axsup syl3anc reximddv 3expib rzal 2ralbidv - 1re anbi12d rspcev sylancr a1d ralrimivw pm2.61iine 3impa ) DGUAZEGUAZAHZ - BHZIJZBEKZADKZYACHZLJZYFYBLJZMZBEKZADKZCGNZXSXTMZYEMZYLODEPPDPUBZEPUBZMZY - MYEYLYQYMYEUCZYFYAIJUDZADKZYAYFIJZYAFHZIJZFDNZOZAGKZMZYKCGYRYFGQZUUGMZMZY - JADYRUUIAYQYMYEAYQARYMARYDADUEUFUUHUUGAUUHARYTUUFAYSADUEUUEAGUEUGUGUGUUJY - ADQZYIBEYRUUIBYQYMYEBYQBRYMBRYCABDEUHUFUUIBRUGUUKBRUUJUUKYBEQZYIUUJUUKYGU - ULYHUUJUUKYGUUJUUKMYAYFUUJDGYAXSXTYQYEUUIUIUJYRUUHUUGUUKUKUUJYSADYRUUHYTU - UFULUMUPUNYRUUIUULYHYRUUIUULMZMZYFYBYRUUHUUGUULUOYRXTUULYBGQZUUMYQXSXTYEU - QZUUIUULURZEGYBUSUTZUUNYBYFIJZYBUUBIJZFDNZUUNUUTUDZFDKZUVAUDUUNYBYAIJZUDZ - ADKZUVCUUNYEUVFYQYMYEUUMVAYRYMUULYEUVFOUUMYQYMYEVBUUQYMUULMYDUVEADYMUUKUU - LYDUVEOYMUUKMZUULMYDYCUVEUULYDYCOUVGYDUULYCYCBEVGVCVDUVGYAGQZUULUUOYCUVEO - XSUUKUVHXTDGYAUSVEUVGEGYBXSXTUUKVFUJYAYBVHVIVJVKVLUTVRUVEUVBAFDYAUUBSUVDU - UTYAUUBYBIVMVNVOVPUUTFDVQVPUUNUUEUUSUVAOAGYBYAYBSZUUAUUSUUDUVAYAYBYFIWIUV - IUUCUUTFDYAYBUUBIWIVSVTUUMUUFYRUUHYTUUFUULWAVDUURWBWCUPWDWEWFWGWJYRXSYOUU - AADKZCGNZUUGCGNYQXSXTYEWHYOYPYMYEWKYRUUHUVJMZCWTZUVKYRYFEQZCWTZUVMYRYPUVO - YOYPYMYEWLCEWMVPYRUVNUVLCYRUVNUUHUVJYREGYFUUPWNYEYQUVNUVJOZYMYEYCADKZBEKU - VPYCABDEWOUVQUVJBYFEYBYFSYCUUAADYBYFYAIVMWPWQWRWSXAXBVRUVJCGXCXDCAFDXEXFX - GXHDPSZYLYNUVRTGQZYATLJZTYBLJZMZBEKZADKZYLXKUWCADXIYKUWDCTGYFTSZYIUWBABDE - UWEYGUVTYHUWAYFTYALVMYFTYBLWIXLXJXMZXNXOEPSZYLYNUWGUVSUWDYLXKUWGUWCADUWBB - EXIXPUWFXNXOXQXR $. + nfra1 nf3an nfan nfra2w simpl2l sselda simplrl simprrl r19.21bi nltled ex + simprll simp2r simpr ssel2 syl2an simpl3 simp2 com12 adantl simplr ltnsym + rsp adantlr syl2an2r syld an32s ralimdva mpd breq2 notbid cbvralvw ralnex + sylib breq1 rexbidv imbi12d simplrr rspcdva mtod expr anim12d expd simp2l + ralrimd ralrimi simp1l wex simp1r n0 sseld ralcom ralbidv rspccv 3ad2ant3 + sylbi jcad eximdv df-rex sylibr axsup syl3anc reximddv 3expib 1re anbi12d + rzal 2ralbidv rspcev sylancr a1d ralrimivw pm2.61iine 3impa ) DGUAZEGUAZA + HZBHZIJZBEKZADKZYACHZLJZYFYBLJZMZBEKZADKZCGNZXSXTMZYEMZYLODEPPDPUBZEPUBZM + ZYMYEYLYQYMYEUCZYFYAIJUDZADKZYAYFIJZYAFHZIJZFDNZOZAGKZMZYKCGYRYFGQZUUGMZM + ZYJADYRUUIAYQYMYEAYQARYMARYDADUEUFUUHUUGAUUHARYTUUFAYSADUEUUEAGUEUGUGUGUU + JYADQZYIBEYRUUIBYQYMYEBYQBRYMBRYCABDEUHUFUUIBRUGUUKBRUUJUUKYBEQZYIUUJUUKY + GUULYHUUJUUKYGUUJUUKMYAYFUUJDGYAXSXTYQYEUUIUIUJYRUUHUUGUUKUKUUJYSADYRUUHY + TUUFULUMUNUOYRUUIUULYHYRUUIUULMZMZYFYBYRUUHUUGUULUPYRXTUULYBGQZUUMYQXSXTY + EUQZUUIUULURZEGYBUSUTZUUNYBYFIJZYBUUBIJZFDNZUUNUUTUDZFDKZUVAUDUUNYBYAIJZU + DZADKZUVCUUNYEUVFYQYMYEUUMVAYRYMUULYEUVFOUUMYQYMYEVBUUQYMUULMYDUVEADYMUUK + UULYDUVEOYMUUKMZUULMYDYCUVEUULYDYCOUVGYDUULYCYCBEVGVCVDUVGYAGQZUULUUOYCUV + EOXSUUKUVHXTDGYAUSVHUVGEGYBXSXTUUKVEUJYAYBVFVIVJVKVLUTVMUVEUVBAFDYAUUBSUV + DUUTYAUUBYBIVNVOVPVRUUTFDVQVRUUNUUEUUSUVAOAGYBYAYBSZUUAUUSUUDUVAYAYBYFIVS + UVIUUCUUTFDYAYBUUBIVSVTWAUUMUUFYRUUHYTUUFUULWBVDUURWCWDUNWEWFWGWIWJYRXSYO + UUAADKZCGNZUUGCGNYQXSXTYEWHYOYPYMYEWKYRUUHUVJMZCWLZUVKYRYFEQZCWLZUVMYRYPU + VOYOYPYMYEWMCEWNVRYRUVNUVLCYRUVNUUHUVJYREGYFUUPWOYEYQUVNUVJOZYMYEYCADKZBE + KUVPYCABDEWPUVQUVJBYFEYBYFSYCUUAADYBYFYAIVNWQWRWTWSXAXBVMUVJCGXCXDCAFDXEX + FXGXHDPSZYLYNUVRTGQZYATLJZTYBLJZMZBEKZADKZYLXIUWCADXKYKUWDCTGYFTSZYIUWBAB + DEUWEYGUVTYHUWAYFTYALVNYFTYBLVSXJXLXMZXNXOEPSZYLYNUWGUVSUWDYLXIUWGUWCADUW + BBEXKXPUWFXNXOXQXR $. $( The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013.) $) @@ -118729,21 +118729,21 @@ this axiom (with the defined operation in place of ` x. ` ) follows as a ( vw cr wss cv cle wbr wral wa wi c0 wcel syl2an weq ssel2 nfv w3a simpr1 wrex cin wceq clt simpr2 wne simp1 simpl disjel biimpcd necon3bd ad2antll wn eleq1w simp2 simp3 simpr ltlend biimprd mpan2d ralimdvva 3exp dedekind - mpd 3imp2 syl3anc ex wex elinel1 nfra1 nf3an nfan nfra2 rsp elinel2 breq2 - n0 rspccv syl5 syl6 com23 imp32 3ad2antl3 adantr ralbidv rspccva r19.21bi - jca ralrimi expr anbi12d 2ralbidv rspcev syl2anc expcom exlimiv pm2.61ine - breq1 sylbi ) DGHZEGHZAIZBIZJKZBELZADLZUAZXDCIZJKZXJXEJKZMZBELADLZCGUCZNZ - DEUDZOXQOUEZXIXOXRXIMXBXCXDXEUFKZBELADLZXOXRXBXCXHUBXRXBXCXHUGXRXBXCXHXTX - RXBXCXHXTNXRXBXCUAZXFXSABDEYAXDDPZXEEPZMZMZXFXEXDUHZXSYEXDEPZUOZYFYAXRYBY - HYDXRXBXCUIYBYCUJZDEXDUKQYCYHYFNYAYBYCYGXEXDBARYCYGBAEUPULUMUNVFYEXSXFYFM - YEXDXEYAXBYBXDGPYDXRXBXCUQYIDGXDSQYAXCYCXEGPYDXRXBXCURYBYCUSEGXESQUTVAVBV - CVDVGABCDEVEVHVIXQOUHFIZXQPZFVJXPFXQVSYKXPFXIYKXOXIYKMZYJGPZXDYJJKZYJXEJK - ZMZBELZADLZXOXIXBYJDPZYMYKXBXCXHUIYJDEVKZDGYJSQYLYQADXIYKAXBXCXHAXBATXCAT - XGADVLVMYKATVNXIYKYBYQXIYKYBMZMZYPBEXIUUABXBXCXHBXBBTXCBTXFABDEVOVMUUABTV - NUUBYCYPUUBYCMYNYOUUBYNYCXHXBUUAYNXCXHYKYBYNXHYBYKYNXHYBXGYKYNNXGADVPYKYJ - EPXGYNYJDEVQXFYNBYJEXEYJXDJVRVTWAWBWCWDWEWFUUBYOBEXIXHYSYOBELZUUAXBXCXHUR - YKYSYBYTWFXGUUCAYJDAFRXFYOBEXDYJXEJWTWGWHQWIWJVIWKWLWKXNYRCYJGCFRZXMYPABD - EUUDXKYNXLYOXJYJXDJVRXJYJXEJWTWMWNWOWPWQWRXAWS $. + mpd 3imp2 syl3anc ex wex n0 elinel1 nfra1 nf3an nfan nfra2w elinel2 breq2 + rsp rspccv syl5 syl6 com23 imp32 3ad2antl3 breq1 ralbidv rspccva r19.21bi + adantr jca ralrimi expr anbi12d 2ralbidv rspcev syl2anc exlimiv pm2.61ine + expcom sylbi ) DGHZEGHZAIZBIZJKZBELZADLZUAZXDCIZJKZXJXEJKZMZBELADLZCGUCZN + ZDEUDZOXQOUEZXIXOXRXIMXBXCXDXEUFKZBELADLZXOXRXBXCXHUBXRXBXCXHUGXRXBXCXHXT + XRXBXCXHXTNXRXBXCUAZXFXSABDEYAXDDPZXEEPZMZMZXFXEXDUHZXSYEXDEPZUOZYFYAXRYB + YHYDXRXBXCUIYBYCUJZDEXDUKQYCYHYFNYAYBYCYGXEXDBARYCYGBAEUPULUMUNVFYEXSXFYF + MYEXDXEYAXBYBXDGPYDXRXBXCUQYIDGXDSQYAXCYCXEGPYDXRXBXCURYBYCUSEGXESQUTVAVB + VCVDVGABCDEVEVHVIXQOUHFIZXQPZFVJXPFXQVKYKXPFXIYKXOXIYKMZYJGPZXDYJJKZYJXEJ + KZMZBELZADLZXOXIXBYJDPZYMYKXBXCXHUIYJDEVLZDGYJSQYLYQADXIYKAXBXCXHAXBATXCA + TXGADVMVNYKATVOXIYKYBYQXIYKYBMZMZYPBEXIUUABXBXCXHBXBBTXCBTXFABDEVPVNUUABT + VOUUBYCYPUUBYCMYNYOUUBYNYCXHXBUUAYNXCXHYKYBYNXHYBYKYNXHYBXGYKYNNXGADVSYKY + JEPXGYNYJDEVQXFYNBYJEXEYJXDJVRVTWAWBWCWDWEWJUUBYOBEXIXHYSYOBELZUUAXBXCXHU + RYKYSYBYTWJXGUUCAYJDAFRXFYOBEXDYJXEJWFWGWHQWIWKVIWLWMWLXNYRCYJGCFRZXMYPAB + DEUUDXKYNXLYOXJYJXDJVRXJYJXEJWFWNWOWPWQWTWRXAWS $. $} @@ -119511,7 +119511,7 @@ it could represent the (meaningless) operation of 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) $) subf $p |- - : ( CC X. CC ) --> CC $= ( vy vz vx cv caddc co wceq cc crio wcel wral cxp cmin wf wa subval subcl - eqeltrrd rgen2a df-sub fmpo mpbi ) ADZBDEFCDZGBHIZHJZAHKCHKHHLHMNUFCAHUDH + eqeltrrd rgen2 df-sub fmpo mpbi ) ADZBDEFCDZGBHIZHJZAHKCHKHHLHMNUFCAHHUDH JUCHJOUDUCMFUEHBUDUCPUDUCQRSCAHHUEHMCABTUAUB $. $} @@ -122545,11 +122545,11 @@ Ordering on reals (cont.) ( CC \ { 0 } ) $= ( vx vy cc cc0 csn cdif cxp cmul wf wfn cv co wcel wss wa ffnov mp2an wne wral eldifsn cres ax-mulf mpbi simpli difss xpss12 fnssres ovres ad2ant2r - mulcl mulne0 jca syl2anb sylibr eqeltrd rgen2a mpbir2an ) CDEZFZUSGZUSHUT - UAZIVAUTJZAKZBKZVALZUSMZBUSSAUSSHCCGZJZUTVGNZVBVHVCVDHLZCMZBCSACSZVGCHIVH - VLOUBABCCCHPUCUDUSCNZVMVICURUEZVNUSCUSCUFQVGUTHUGQVFABUSVCUSMZVDUSMZOZVEV - JUSVCVDUSUSHUHVQVKVJDRZOZVJUSMVOVCCMZVCDRZOZVDCMZVDDRZOZVSVPVCCDTVDCDTWBW - EOVKVRVTWCVKWAWDVCVDUJUIVCVDUKULUMVJCDTUNUOUPABUSUSUSVAPUQ $. + mulcl mulne0 jca syl2anb sylibr eqeltrd rgen2 mpbir2an ) CDEZFZUSGZUSHUTU + AZIVAUTJZAKZBKZVALZUSMZBUSSAUSSHCCGZJZUTVGNZVBVHVCVDHLZCMZBCSACSZVGCHIVHV + LOUBABCCCHPUCUDUSCNZVMVICURUEZVNUSCUSCUFQVGUTHUGQVFABUSUSVCUSMZVDUSMZOZVE + VJUSVCVDUSUSHUHVQVKVJDRZOZVJUSMVOVCCMZVCDRZOZVDCMZVDDRZOZVSVPVCCDTVDCDTWB + WEOVKVRVTWCVKWAWDVCVDUJUIVCVDUKULUMVJCDTUNUOUPABUSUSUSVAPUQ $. $} ${ @@ -125239,12 +125239,12 @@ Ordering on reals (cont.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) $) lble $p |- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ A ) $= - ( cr wss cv cle wbr wral wrex wcel crio wa wreu lbreu nfcv nfriota1 nfral - nfbr eqid wceq nfra1 nfriota nfeq2 breq1 ralbid riotaprop syl simprd rspc - breq2 mpan9 3impa ) DEFZAGZBGZHIZBDJZADKZCDLZUSADMZCHIZUOUTNZVBUQHIZBDJZV - AVCVDVBDLZVFVDUSADOVGVFNABDPUSVFADVBVEABDADQAVBUQHUSADRAHQAUQQTSVBUAUPVBU - BURVEBDBUPVBUSBADURBDUCBDQUDZUEUPVBUQHUFUGUHUIUJVEVCBCDBVBCHVHBHQBCQTUQCV - BHULUKUMUN $. + ( cr wss cv cle wbr wral wrex wcel crio wa wreu nfcv nfriota1 nfbr nfralw + lbreu eqid wceq nfra1 nfriota nfeq2 breq1 ralbid riotaprop syl breq2 rspc + simprd mpan9 3impa ) DEFZAGZBGZHIZBDJZADKZCDLZUSADMZCHIZUOUTNZVBUQHIZBDJZ + VAVCVDVBDLZVFVDUSADOVGVFNABDTUSVFADVBVEABDADPAVBUQHUSADQAHPAUQPRSVBUAUPVB + UBURVEBDBUPVBUSBADURBDUCBDPUDZUEUPVBUQHUFUGUHUIULVEVCBCDBVBCHVHBHPBCPRUQC + VBHUJUKUMUN $. $} ${ @@ -125409,9 +125409,9 @@ of completeness axiom (it has a slightly weaker antecedent). E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) ) $= ( vw cr wss c0 wne cv cle wbr wral wrex w3a wcel wa clt csup wor ltso a1i - sup3 simp1 suplub2 breq2 cbvrexv syl6bb ) DGHZDIJZBKAKLMBDNAGOZPZEGQREDGS - TSMEFKZSMZFDOECKZSMZCDOUMABFGDESGSUAUMUBUCABFDUDUJUKULUEUFUOUQFCDUNUPESUG - UHUI $. + sup3 simp1 suplub2 breq2 cbvrexvw syl6bb ) DGHZDIJZBKAKLMBDNAGOZPZEGQREDG + STSMEFKZSMZFDOECKZSMZCDOUMABFGDESGSUAUMUBUCABFDUDUJUKULUEUFUOUQFCDUNUPESU + GUHUI $. $( An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004.) (Revised by Mario @@ -125430,10 +125430,10 @@ of completeness axiom (it has a slightly weaker antecedent). E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) ) $= ( vw cr wss c0 wne cv cle wbr wral wrex w3a wcel wa clt wn suprnub suprcl - wb lenlt sylan simpl1 sselda simplr lenltd ralbidva 3bitr4d breq1 cbvralv - csup syl6bb ) DGHZDIJZBKAKLMBDNAGOZPZEGQZRZDGSUNZELMZFKZELMZFDNZCKZELMZCD - NVAEVBSMTZEVDSMTZFDNVCVFABFDEUAUSVBGQUTVCVIUCABDUBVBEUDUEVAVEVJFDVAVDDQZR - VDEVADGVDUPUQURUTUFUGUSUTVKUHUIUJUKVEVHFCDVDVGELULUMUO $. + csup wb lenlt sylan simpl1 sselda simplr lenltd ralbidva 3bitr4d cbvralvw + breq1 syl6bb ) DGHZDIJZBKAKLMBDNAGOZPZEGQZRZDGSUCZELMZFKZELMZFDNZCKZELMZC + DNVAEVBSMTZEVDSMTZFDNVCVFABFDEUAUSVBGQUTVCVIUDABDUBVBEUEUFVAVEVJFDVAVDDQZ + RVDEVADGVDUPUQURUTUGUHUSUTVKUIUJUKULVEVHFCDVDVGELUNUMUO $. $} ${ @@ -125450,28 +125450,28 @@ of completeness axiom (it has a slightly weaker antecedent). supaddc $p |- ( ph -> ( sup ( A , RR , < ) + B ) = sup ( C , RR , < ) ) $= ( vw va cr cle wbr wcel wrex clt csup caddc co wceq wn cv vex weq oveq1 - wral eqeq2d cbvrexv eqeq1 rexbidv syl5bb elab2 wa sselda suprcld adantr - wss c0 wne 3jca suprub sylan leadd1dd breq1 syl5ibrcom rexlimdva syl5bi - w3a ralrimiv wb readdcld eleq1a syl ssrdv wex ovex isseti rgenw sylancl - wi r19.2z exbii n0 rexcom4 3bitr4i sylibr brralrspcev suprleub syl31anc - syl2anc mpbird cmin ltsubaddd biimpar resubcld suprlub adantlr ad2antrr - mpbid rspe adantl simplrr eqbrtrrd mpdan expr exlimdv mpi mtbird nrexdv - lensymd pm2.65da eqleltd mpbir2and eqcomd ) AHPUAUBZFPUAUBZGUCUDZAXTYBU - EXTYBQRZXTYBUARZUFAYCNUGZYBQRZNHUKZAYFNHYEHSZYEOUGZGUCUDZUEZOFTZAYFDUGZ - EUGZGUCUDZUEZEFTZYLDYEHNUHYQYMYJUEZOFTDNUIZYLYPYREOFEOUIYOYJYMYNYIGUCUJ - ULUMYSYRYKOFYMYEYJUNUOUPMUQZAYKYFOFAYIFSZURZYFYKYJYBQRUUBYIYAGAFPYIIUSZ - AYAPSUUAABCFIJKUTZVAAGPSZUUALVAZAFPVBZFVCVDZCUGBUGZQRCFUKBPTZVMUUAYIYAQ - RAUUGUUHUUJIJKVEBCFYIVFVGVHYEYJYBQVIVJVKVLVNZAHPVBZHVCVDZYEUUIQRNHUKBPT - ZYBPSZYCYGVOANHPYHYLAYEPSZYTAYKUUPOFUUBYJPSZYKUUPWEUUBYIGUUCUUFVPZYJPYE - VQVRVKVLVSZAYKNVTZOFTZUUMAUUHUUTOFUKUVAJUUTOFNYJYIGUCWAWBZWCUUTOFWFWDYH - NVTYLNVTUUMUVAYHYLNYTWGNHWHYKONFWIWJWKZAUUOYGUUNAYAGUUDLVPZUUKBNYEYBQPH - WLWOZUVDBNNHYBWMWNWPAYDXTGWQUDZYIUARZOFTZAYDURZUVFYAUARZUVHAUVJYDAXTGYA - ABNHUUSUVCUVEUTZLUUDWRWSAUVJUVHVOZYDAUUGUUHUUJUVFPSUVLIJKAXTGUVKLWTBCOF - UVFXAWNVAXDUVIUVGOFUVIUUAURZUVGXTYJUARUVMYJXTAUUAUUQYDUURXBAXTPSYDUUAUV - KXCZAUUAYJXTQRZYDUUBUUTUVOUVBUUBYKUVONAUUAYKUVOAUUAYKURZURZYHUVOUVPYHAU - VPYLYHYKOFXEYTWKXFUVQYHURYEYJXTQAUUAYKYHXGAYHYEXTQRZUVPAUULUUMUUNVMYHUV - RAUULUUMUUNUUSUVCUVEVEBNHYEVFVGXBXHXIXJXKXLXBXOUVMXTGYIUVNAUUEYDUUALXCA - UUAYIPSYDUUCXBWRXMXNXPAXTYBUVKUVDXQXRXS $. + eqeq2d cbvrexvw eqeq1 rexbidv syl5bb elab2 wa sselda suprcld adantr wss + wral c0 wne w3a suprub sylan leadd1dd breq1 syl5ibrcom rexlimdva syl5bi + 3jca ralrimiv wb readdcld eleq1a syl ssrdv wex ovex isseti rgenw r19.2z + wi sylancl exbii n0 rexcom4 3bitr4i sylibr brralrspcev syl2anc suprleub + syl31anc cmin ltsubaddd biimpar resubcld suprlub mpbid adantlr ad2antrr + mpbird rspe adantl simplrr eqbrtrrd mpdan exlimdv lensymd mtbird nrexdv + expr mpi pm2.65da eqleltd mpbir2and eqcomd ) AHPUAUBZFPUAUBZGUCUDZAXTYB + UEXTYBQRZXTYBUARZUFAYCNUGZYBQRZNHVBZAYFNHYEHSZYEOUGZGUCUDZUEZOFTZAYFDUG + ZEUGZGUCUDZUEZEFTZYLDYEHNUHYQYMYJUEZOFTDNUIZYLYPYREOFEOUIYOYJYMYNYIGUCU + JUKULYSYRYKOFYMYEYJUMUNUOMUPZAYKYFOFAYIFSZUQZYFYKYJYBQRUUBYIYAGAFPYIIUR + ZAYAPSUUAABCFIJKUSZUTAGPSZUUALUTZAFPVAZFVCVDZCUGBUGZQRCFVBBPTZVEUUAYIYA + QRAUUGUUHUUJIJKVMBCFYIVFVGVHYEYJYBQVIVJVKVLVNZAHPVAZHVCVDZYEUUIQRNHVBBP + TZYBPSZYCYGVOANHPYHYLAYEPSZYTAYKUUPOFUUBYJPSZYKUUPWEUUBYIGUUCUUFVPZYJPY + EVQVRVKVLVSZAYKNVTZOFTZUUMAUUHUUTOFVBUVAJUUTOFNYJYIGUCWAWBZWCUUTOFWDWFY + HNVTYLNVTUUMUVAYHYLNYTWGNHWHYKONFWIWJWKZAUUOYGUUNAYAGUUDLVPZUUKBNYEYBQP + HWLWMZUVDBNNHYBWNWOXDAYDXTGWPUDZYIUARZOFTZAYDUQZUVFYAUARZUVHAUVJYDAXTGY + AABNHUUSUVCUVEUSZLUUDWQWRAUVJUVHVOZYDAUUGUUHUUJUVFPSUVLIJKAXTGUVKLWSBCO + FUVFWTWOUTXAUVIUVGOFUVIUUAUQZUVGXTYJUARUVMYJXTAUUAUUQYDUURXBAXTPSYDUUAU + VKXCZAUUAYJXTQRZYDUUBUUTUVOUVBUUBYKUVONAUUAYKUVOAUUAYKUQZUQZYHUVOUVPYHA + UVPYLYHYKOFXEYTWKXFUVQYHUQYEYJXTQAUUAYKYHXGAYHYEXTQRZUVPAUULUUMUUNVEYHU + VRAUULUUMUUNUUSUVCUVEVMBNHYEVFVGXBXHXIXNXJXOXBXKUVMXTGYIUVNAUUEYDUUALXC + AUUAYIPSYDUUCXBWQXLXMXPAXTYBUVKUVDXQXRXS $. $} supadd.b1 $e |- ( ph -> B C_ RR ) $. supadd.b2 $e |- ( ph -> B =/= (/) ) $. @@ -125483,44 +125483,44 @@ of completeness axiom (it has a slightly weaker antecedent). sup ( C , RR , < ) ) $= ( va vw cr cle clt csup caddc wceq wbr wrex cab suprcld eqid supaddc wcel co cv wa sselda recnd adantr addcomd eqeq2d rexbidva abbidv supeq1d eqtrd - wral vex weq eqeq1 rexbidv elab wss c0 wne adantlr oveq1 cbvrexv 2rexbidv - rspe syl5bb elab2 sylibr ex sseld anim12d readdcl eleq1a rexlimdvv syl5bi - syl6 ssrdv wex ovex isseti rgenw r19.2z sylancl rexcom4 ralrimivw syl2anc - wi sylib n0 exbii bitri readdcld adantrr adantrl w3a suprub sylan le2addd - 3jca breq1 biimprcd ralrimiv brralrspcev syl3anc sylan9r wb syl rexlimdva - abssdv abn0 suprleub syl31anc mpbird eqbrtrd syl5ibrcom letri3d mpbir2and - ) AFSUAUBZGSUAUBZUCULZHSUAUBZUDYLYMTUEYMYLTUEZAYLDUMZYKQUMZUCULZUDZQFUFZD - UGZSUAUBZYMTAYLYOYPYKUCULZUDZQFUFZDUGZSUAUBUUAABCDQFYKUUEJKLABCGMNOUHZUUE - UIUJASUUEYTUAAUUDYSDAUUCYRQFAYPFUKZUNZUUBYQYOUUHYPYKUUHYPAFSYPJUOZUPUUHYK - AYKSUKZUUGUUFUQZUPURUSUTVAVBVCAUUAYMTUEZRUMZYMTUEZRYTVDZAUUNRYTUUMYTUKUUM - YQUDZQFUFZAUUNYSUUQDUUMRVEZDRVFZYRUUPQFYOUUMYQVGVHVIAUUPUUNQFUUHUUNUUPYQY - MTUEUUHYQYOYPIUMZUCULZUDZIGUFZDUGZSUAUBZYMTUUHYQYOUUTYPUCULZUDZIGUFZDUGZS - UAUBUVEUUHBCDIGYPUVIAGSVJZUUGMUQAGVKVLZUUGNUQACUMBUMZTUEZCGVDBSUFZUUGOUQU - UIUVIUIUJUUHSUVIUVDUAUUHUVHUVCDUUHUVGUVBIGUUHUUTGUKZUNZUVFUVAYOUVPUUTYPUV - PUUTAUVOUUTSUKZUUGAGSUUTMUOZVMZUPUVPYPUUHYPSUKZUVOUUIUQZUPURUSUTVAVBVCUUH - UVEYMTUEZUUNRUVDVDZUUHUUNRUVDUUMUVDUKUUMUVAUDZIGUFZUUHUUNUVCUWEDUUMUURUUS - UVBUWDIGYOUUMUVAVGZVHVIUUGUWEUUMHUKZAUUNUUGUWEUWGUUGUWEUNUWEQFUFZUWGUWEQF - VQYOEUMZUUTUCULZUDZIGUFZEFUFZUWHDUUMHUURUWMUVCQFUFUUSUWHUWLUVCEQFEQVFZUWK - UVBIGUWNUWJUVAYOUWIYPUUTUCVNUSVHVOUUSUVBUWDQIFGUWFVPVRPVSZVTWAAHSVJZHVKVL - ZUUMUVLTUEZRHVDBSUFZUWGUUNWSARHSUWGUWHAUUMSUKZUWOAUWDUWTQIFGAUUGUVOUNZUVA - SUKZUWDUWTWSAUXAUVTUVQUNUXBAUUGUVTUVOUVQAFSYPJWBAGSUUTMWBWCYPUUTWDWHUVASU - UMWEWHWFWGWIZAUWHRWJZUWQAUWERWJZQFUFZUXDAFVKVLZUXEQFVDUXFKAUXEQFAUWDRWJZI - GUFZUXEAUVKUXHIGVDUXINUXHIGRUVAYPUUTUCWKZWLWMUXHIGWNWOUWDIRGWPWTWQUXEQFWN - WRUWEQRFWPWTUWQUWGRWJUXDRHXAUWGUWHRUWOXBXCVTZAYLSUKZUUMYLTUEZRHVDZUWSAYJY - KABCFJKLUHZUUFXDZAUXMRHUWGUWHAUXMUWOAUWDUXMQIFGAUXAUVAYLTUEZUWDUXMWSAUXAU - XQAUXAUNYPUUTYJYKAUUGUVTUVOUUIXEAUVOUVQUUGUVRXFAYJSUKUXAUXOUQAUUJUXAUUFUQ - AUUGYPYJTUEZUVOAFSVJZUXGUVMCFVDBSUFZXGUUGUXRAUXSUXGUXTJKLXKBCFYPXHXIXEAUV - OUUTYKTUEZUUGAUVJUVKUVNXGUVOUYAAUVJUVKUVNMNOXKBCGUUTXHXIXFXJWAUWDUXMUXQUU - MUVAYLTXLXMWHWFWGXNZBRUUMYLTSHXOWRZUWPUWQUWSXGUWGUUNBRHUUMXHWAXPXQWGXNZUU - HUVDSVJUVDVKVLZUWRRUVDVDBSUFZYMSUKZUWBUWCXRUUHUVCDSUUHUVBYOSUKZIGUVPUXBUV - BUYHWSUVPYPUUTUWAUVSXDUVASYOWEXSXTYAAUYEUUGAUVCDWJZUYEAUVBDWJZIGUFZUYIAUV - KUYJIGVDUYKNUYJIGDUVAUXJWLWMUYJIGWNWOUVBIDGWPWTUVCDYBVTUQUUHUYGUWCUYFAUYG - UUGABRHUXCUXKUYCUHZUQZUYDBRUUMYMTSUVDXOWRUYMBRRUVDYMYCYDYEYFUUMYQYMTXLYGX - TWGXNZAYTSVJYTVKVLZUWRRYTVDBSUFZUYGUULUUOXRAYSDSAYRUYHQFUUHYQSUKYRUYHWSUU - HYKYPUUKUUIXDYQSYOWEXSXTYAAYSDWJZUYOAYRDWJZQFUFZUYQAUXGUYRQFVDUYSKUYRQFDY - QYKYPUCWKWLWMUYRQFWNWOYRQDFWPWTYSDYBVTAUYGUUOUYPUYLUYNBRUUMYMTSYTXOWRUYLB - RRYTYMYCYDYEYFAYNUXNUYBAUWPUWQUWSUXLYNUXNXRUXCUXKUYCUXPBRRHYLYCYDYEAYLYMU - XPUYLYHYI $. + wral vex weq eqeq1 rexbidv elab wss c0 wne adantlr rspe cbvrexvw 2rexbidv + oveq1 syl5bb elab2 sylibr ex anim12d readdcl syl6 eleq1a rexlimdvv syl5bi + wi sseld ssrdv wex ovex isseti rgenw r19.2z sylancl rexcom4 sylib syl2anc + ralrimivw n0 exbii bitri readdcld adantrr adantrl w3a 3jca suprub le2addd + sylan breq1 biimprcd ralrimiv brralrspcev syl3anc wb syl rexlimdva abssdv + sylan9r suprleub syl31anc mpbird eqbrtrd syl5ibrcom letri3d mpbir2and + abn0 ) AFSUAUBZGSUAUBZUCULZHSUAUBZUDYLYMTUEYMYLTUEZAYLDUMZYKQUMZUCULZUDZQ + FUFZDUGZSUAUBZYMTAYLYOYPYKUCULZUDZQFUFZDUGZSUAUBUUAABCDQFYKUUEJKLABCGMNOU + HZUUEUIUJASUUEYTUAAUUDYSDAUUCYRQFAYPFUKZUNZUUBYQYOUUHYPYKUUHYPAFSYPJUOZUP + UUHYKAYKSUKZUUGUUFUQZUPURUSUTVAVBVCAUUAYMTUEZRUMZYMTUEZRYTVDZAUUNRYTUUMYT + UKUUMYQUDZQFUFZAUUNYSUUQDUUMRVEZDRVFZYRUUPQFYOUUMYQVGVHVIAUUPUUNQFUUHUUNU + UPYQYMTUEUUHYQYOYPIUMZUCULZUDZIGUFZDUGZSUAUBZYMTUUHYQYOUUTYPUCULZUDZIGUFZ + DUGZSUAUBUVEUUHBCDIGYPUVIAGSVJZUUGMUQAGVKVLZUUGNUQACUMBUMZTUEZCGVDBSUFZUU + GOUQUUIUVIUIUJUUHSUVIUVDUAUUHUVHUVCDUUHUVGUVBIGUUHUUTGUKZUNZUVFUVAYOUVPUU + TYPUVPUUTAUVOUUTSUKZUUGAGSUUTMUOZVMZUPUVPYPUUHYPSUKZUVOUUIUQZUPURUSUTVAVB + VCUUHUVEYMTUEZUUNRUVDVDZUUHUUNRUVDUUMUVDUKUUMUVAUDZIGUFZUUHUUNUVCUWEDUUMU + URUUSUVBUWDIGYOUUMUVAVGZVHVIUUGUWEUUMHUKZAUUNUUGUWEUWGUUGUWEUNUWEQFUFZUWG + UWEQFVNYOEUMZUUTUCULZUDZIGUFZEFUFZUWHDUUMHUURUWMUVCQFUFUUSUWHUWLUVCEQFEQV + FZUWKUVBIGUWNUWJUVAYOUWIYPUUTUCVQUSVHVOUUSUVBUWDQIFGUWFVPVRPVSZVTWAAHSVJZ + HVKVLZUUMUVLTUEZRHVDBSUFZUWGUUNWHARHSUWGUWHAUUMSUKZUWOAUWDUWTQIFGAUUGUVOU + NZUVASUKZUWDUWTWHAUXAUVTUVQUNUXBAUUGUVTUVOUVQAFSYPJWIAGSUUTMWIWBYPUUTWCWD + UVASUUMWEWDWFWGWJZAUWHRWKZUWQAUWERWKZQFUFZUXDAFVKVLZUXEQFVDUXFKAUXEQFAUWD + RWKZIGUFZUXEAUVKUXHIGVDUXINUXHIGRUVAYPUUTUCWLZWMWNUXHIGWOWPUWDIRGWQWRWTUX + EQFWOWSUWEQRFWQWRUWQUWGRWKUXDRHXAUWGUWHRUWOXBXCVTZAYLSUKZUUMYLTUEZRHVDZUW + SAYJYKABCFJKLUHZUUFXDZAUXMRHUWGUWHAUXMUWOAUWDUXMQIFGAUXAUVAYLTUEZUWDUXMWH + AUXAUXQAUXAUNYPUUTYJYKAUUGUVTUVOUUIXEAUVOUVQUUGUVRXFAYJSUKUXAUXOUQAUUJUXA + UUFUQAUUGYPYJTUEZUVOAFSVJZUXGUVMCFVDBSUFZXGUUGUXRAUXSUXGUXTJKLXHBCFYPXIXK + XEAUVOUUTYKTUEZUUGAUVJUVKUVNXGUVOUYAAUVJUVKUVNMNOXHBCGUUTXIXKXFXJWAUWDUXM + UXQUUMUVAYLTXLXMWDWFWGXNZBRUUMYLTSHXOWSZUWPUWQUWSXGUWGUUNBRHUUMXIWAXPYAWG + XNZUUHUVDSVJUVDVKVLZUWRRUVDVDBSUFZYMSUKZUWBUWCXQUUHUVCDSUUHUVBYOSUKZIGUVP + UXBUVBUYHWHUVPYPUUTUWAUVSXDUVASYOWEXRXSXTAUYEUUGAUVCDWKZUYEAUVBDWKZIGUFZU + YIAUVKUYJIGVDUYKNUYJIGDUVAUXJWMWNUYJIGWOWPUVBIDGWQWRUVCDYIVTUQUUHUYGUWCUY + FAUYGUUGABRHUXCUXKUYCUHZUQZUYDBRUUMYMTSUVDXOWSUYMBRRUVDYMYBYCYDYEUUMYQYMT + XLYFXSWGXNZAYTSVJYTVKVLZUWRRYTVDBSUFZUYGUULUUOXQAYSDSAYRUYHQFUUHYQSUKYRUY + HWHUUHYKYPUUKUUIXDYQSYOWEXRXSXTAYSDWKZUYOAYRDWKZQFUFZUYQAUXGUYRQFVDUYSKUY + RQFDYQYKYPUCWLWMWNUYRQFWOWPYRQDFWQWRYSDYIVTAUYGUUOUYPUYLUYNBRUUMYMTSYTXOW + SUYLBRRYTYMYBYCYDYEAYNUXNUYBAUWPUWQUWSUXLYNUXNXQUXCUXKUYCUXPBRRHYLYBYCYDA + YLYMUXPUYLYGYH $. $} ${ @@ -125537,40 +125537,40 @@ of completeness axiom (it has a slightly weaker antecedent). supmul1 $p |- ( ph -> ( A x. sup ( B , RR , < ) ) = sup ( C , RR , < ) ) $= ( vw vb cr clt cle wbr wa wcel cc0 adantr csup cmul co wceq wral wrex vex - wn cv oveq2 eqeq2d cbvrexv eqeq1 rexbidv syl5bb elab2 wss wne simpr sylbi - c0 w3a simp1d sselda suprcl syl simpl1 simpl2 jca suprub lemul2a syl31anc - sylan breq1 syl5ibrcom rexlimdva syl5bi ralrimiv wb remulcld eleq1a ssrdv - wi wex simpr2 isseti rgenw r19.2z sylancl exbii n0 rexcom4 3bitr4i sylibr - ovex brralrspcev syl2anc 3jca mpbird cdiv 0red simpl3 breq2 rspccva letrd - suprleub exlimdv mpd imp mulge0d anim1i lelttr prodgt02 syl22anc ltdivmul - ex syl3anc syl112anc gt0ne0d redivcld suprlub mpbid adantlr ad2antrr rspe - adantl simplrr eqbrtrrd mpdan expr lensymd mtbird nrexdv pm2.65da eqleltd - mpi eqcomd ) AHMNUAZFGMNUAZUBUCZAYRYTUDYRYTOPZYRYTNPZUHZQAUUAUUCAUUAKUIZY - TOPZKHUEZAUUEKHUUDHRZUUDFLUIZUBUCZUDZLGUFZAUUEDUIZFEUIZUBUCZUDZEGUFZUUKDU - UDHKUGUUPUULUUIUDZLGUFUULUUDUDZUUKUUOUUQELGUUMUUHUDUUNUUIUULUUMUUHFUBUJUK - ULUURUUQUUJLGUULUUDUUIUMUNUOIUPZAUUJUUELGAUUHGRZQZUUEUUJUUIYTOPZUVAUUHMRZ - YSMRZFMRZSFOPZQZUUHYSOPZUVBAGMUUHAGMUQZGVAURZCUIBUIZOPCGUEBMUFZAUVEUVFSUV - KOPZBGUEZVBZUVIUVJUVLVBZQZUVPJUVOUVPUSUTZVCVDZAUVDUUTAUVPUVDUVRBCGVEVFZTZ - AUVGUUTAUVEUVFAUVQUVEJUVEUVFUVNUVPVGUTZAUVQUVFJUVEUVFUVNUVPVHUTZVITAUVPUU - TUVHUVRBCGUUHVJVMZUUHYSFVKVLUUDUUIYTOVNVOVPVQVRZAHMUQZHVAURZUUDUVKOPKHUEB - MUFZVBZYTMRZUUAUUFVSAUWFUWGUWHAKHMUUGUUKAUUDMRZUUSAUUJUWKLGUVAUUIMRZUUJUW - KWCUVAFUUHAUVEUUTUWBTZUVSVTZUUIMUUDWAVFVPVQZWBAUUJKWDZLGUFZUWGAUVJUWPLGUE - UWQAUVQUVJJUVOUVIUVJUVLWEUTZUWPLGKUUIFUUHUBWOWFZWGUWPLGWHWIUUGKWDZUUKKWDU - WGUWQUUGUUKKUUSWJKHWKZUUJLKGWLWMWNZAUWJUUFUWHAFYSUWBUVTVTZUWEBKUUDYTOMHWP - WQWRZUXCBKKHYTXFWQWSAUUBYRFWTUCZUUHNPZLGUFZAUUBQZUXEYSNPZUXGUXHUXIUUBAUUB - USUXHYRMRZUVDUVESFNPZUXIUUBVSAUXJUUBAUWIUXJUXDBKHVEVFZTZAUVDUUBUVTTZAUVEU - UBUWBTZUXHUVEUVDSYSOPZSYTNPZUXKUXOUXNAUXPUUBAUVJUXPUWRUVJUUTLWDAUXPLGWKAU - UTUXPLAUUTUXPUVASUUHYSUVAXAUVSUWAAUVNUUTSUUHOPZAUVQUVNJUVEUVFUVNUVPXBUTUV - MUXRBUUHGUVKUUHSOXCXDVMZUWDXEXPXGVQXHTUXHSYROPZUUBQZUXQAUXTUUBAUWGUXTUXBU - WGUWTAUXTUXAAUUGUXTKAUUGUXTAUUGQZSUUDYRUYBXAAUUGUWKUWOXIAUXJUUGUXLTAUUGSU - UDOPZUUGUUKAUYCUUSAUUJUYCLGUVAUYCUUJSUUIOPUVAFUUHUWMUVSAUVFUUTUWCTUXSXJUU - DUUISOXCVOVPVQXIAUWIUUGUUDYROPZUXDBKHUUDVJVMZXEXPXGVQXHXKAUYAUXQWCZUUBASM - RUXJUWJUYFAXAUXLUXCSYRYTXLXQTXHFYSXMXNZYRYSFXOXRWSUXHUVPUXEMRUXIUXGVSAUVP - UUBUVRTUXHYRFUXMUXOUXHFUYGXSXTBCLGUXEYAWQYBUXHUXFLGUXHUUTQZUXFYRUUINPZUYH - UUIYRAUUTUWLUUBUWNYCAUXJUUBUUTUXLYDZAUUTUUIYROPZUUBUVAUWPUYKUWSUVAUUJUYKK - AUUTUUJUYKAUUTUUJQZQZUUGUYKUYLUUGAUYLUUKUUGUUJLGYEUUSWNYFUYMUUGQUUDUUIYRO - AUUTUUJUUGYGAUUGUYDUYLUYEYCYHYIYJXGYPYCYKUYHUXJUVCUVEUXKUXFUYIVSUYJAUUTUV - CUUBUVSYCAUVEUUBUUTUWBYDUXHUXKUUTUYGTYRUUHFXOXRYLYMYNVIAYRYTUXLUXCYOWSYQ + wn cv oveq2 eqeq2d cbvrexvw eqeq1 rexbidv syl5bb elab2 wss c0 simpr sylbi + wne w3a simp1d sselda suprcl syl simpl1 simpl2 jca sylan lemul2a syl31anc + suprub breq1 rexlimdva syl5bi ralrimiv wb wi remulcld eleq1a ssrdv simpr2 + syl5ibrcom wex ovex isseti rgenw r19.2z sylancl n0 rexcom4 3bitr4i sylibr + exbii brralrspcev syl2anc 3jca suprleub mpbird simpl3 breq2 rspccva letrd + cdiv 0red exlimdv mpd imp mulge0d anim1i lelttr syl3anc prodgt02 syl22anc + ltdivmul syl112anc gt0ne0d redivcld suprlub mpbid adantlr ad2antrr adantl + ex rspe simplrr eqbrtrrd mpdan mpi lensymd mtbird nrexdv pm2.65da eqleltd + expr eqcomd ) AHMNUAZFGMNUAZUBUCZAYRYTUDYRYTOPZYRYTNPZUHZQAUUAUUCAUUAKUIZ + YTOPZKHUEZAUUEKHUUDHRZUUDFLUIZUBUCZUDZLGUFZAUUEDUIZFEUIZUBUCZUDZEGUFZUUKD + UUDHKUGUUPUULUUIUDZLGUFUULUUDUDZUUKUUOUUQELGUUMUUHUDUUNUUIUULUUMUUHFUBUJU + KULUURUUQUUJLGUULUUDUUIUMUNUOIUPZAUUJUUELGAUUHGRZQZUUEUUJUUIYTOPZUVAUUHMR + ZYSMRZFMRZSFOPZQZUUHYSOPZUVBAGMUUHAGMUQZGURVAZCUIBUIZOPCGUEBMUFZAUVEUVFSU + VKOPZBGUEZVBZUVIUVJUVLVBZQZUVPJUVOUVPUSUTZVCVDZAUVDUUTAUVPUVDUVRBCGVEVFZT + ZAUVGUUTAUVEUVFAUVQUVEJUVEUVFUVNUVPVGUTZAUVQUVFJUVEUVFUVNUVPVHUTZVITAUVPU + UTUVHUVRBCGUUHVMVJZUUHYSFVKVLUUDUUIYTOVNWDVOVPVQZAHMUQZHURVAZUUDUVKOPKHUE + BMUFZVBZYTMRZUUAUUFVRAUWFUWGUWHAKHMUUGUUKAUUDMRZUUSAUUJUWKLGUVAUUIMRZUUJU + WKVSUVAFUUHAUVEUUTUWBTZUVSVTZUUIMUUDWAVFVOVPZWBAUUJKWEZLGUFZUWGAUVJUWPLGU + EUWQAUVQUVJJUVOUVIUVJUVLWCUTZUWPLGKUUIFUUHUBWFWGZWHUWPLGWIWJUUGKWEZUUKKWE + UWGUWQUUGUUKKUUSWOKHWKZUUJLKGWLWMWNZAUWJUUFUWHAFYSUWBUVTVTZUWEBKUUDYTOMHW + PWQWRZUXCBKKHYTWSWQWTAUUBYRFXEUCZUUHNPZLGUFZAUUBQZUXEYSNPZUXGUXHUXIUUBAUU + BUSUXHYRMRZUVDUVESFNPZUXIUUBVRAUXJUUBAUWIUXJUXDBKHVEVFZTZAUVDUUBUVTTZAUVE + UUBUWBTZUXHUVEUVDSYSOPZSYTNPZUXKUXOUXNAUXPUUBAUVJUXPUWRUVJUUTLWEAUXPLGWKA + UUTUXPLAUUTUXPUVASUUHYSUVAXFUVSUWAAUVNUUTSUUHOPZAUVQUVNJUVEUVFUVNUVPXAUTU + VMUXRBUUHGUVKUUHSOXBXCVJZUWDXDYEXGVPXHTUXHSYROPZUUBQZUXQAUXTUUBAUWGUXTUXB + UWGUWTAUXTUXAAUUGUXTKAUUGUXTAUUGQZSUUDYRUYBXFAUUGUWKUWOXIAUXJUUGUXLTAUUGS + UUDOPZUUGUUKAUYCUUSAUUJUYCLGUVAUYCUUJSUUIOPUVAFUUHUWMUVSAUVFUUTUWCTUXSXJU + UDUUISOXBWDVOVPXIAUWIUUGUUDYROPZUXDBKHUUDVMVJZXDYEXGVPXHXKAUYAUXQVSZUUBAS + MRUXJUWJUYFAXFUXLUXCSYRYTXLXMTXHFYSXNXOZYRYSFXPXQWTUXHUVPUXEMRUXIUXGVRAUV + PUUBUVRTUXHYRFUXMUXOUXHFUYGXRXSBCLGUXEXTWQYAUXHUXFLGUXHUUTQZUXFYRUUINPZUY + HUUIYRAUUTUWLUUBUWNYBAUXJUUBUUTUXLYCZAUUTUUIYROPZUUBUVAUWPUYKUWSUVAUUJUYK + KAUUTUUJUYKAUUTUUJQZQZUUGUYKUYLUUGAUYLUUKUUGUUJLGYFUUSWNYDUYMUUGQUUDUUIYR + OAUUTUUJUUGYGAUUGUYDUYLUYEYBYHYIYPXGYJYBYKUYHUXJUVCUVEUXKUXFUYIVRUYJAUUTU + VCUUBUVSYBAUVEUUBUUTUWBYCUXHUXKUUTUYGTYRUUHFXPXQYLYMYNVIAYRYTUXLUXCYOWTYQ $. $} @@ -125585,38 +125585,38 @@ of completeness axiom (it has a slightly weaker antecedent). supmullem1 $p |- ( ph -> A. w e. C w <_ ( sup ( A , RR , < ) x. sup ( B , RR , < ) ) ) $= ( va cv cr cle wbr wcel wrex cc0 clt csup cmul wceq vex weq oveq1 rexbidv - co eqeq2d cbvrexv eqeq1 2rexbidv syl5bb elab2 wa wss wne wral w3a simp2bi - wi c0 simp1d sselda adantrr suprcl syl adantr simp3bi adantrl sylbi breq2 - simp1l rspccv simp1r suprub sylan lemul12ad breq1 biimprcd syl6 rexlimdvv - imp ex syl5bi ralrimiv ) AENZGOUAUBZHOUAUBZUCUIZPQZEIWHIRWHMNZJNZUCUIZUDZ - JHSMGSZAWLDNZFNZWNUCUIZUDZJHSZFGSZWQDWHIEUEXCWRWOUDZJHSZMGSDEUFZWQXBXEFMG - FMUFZXAXDJHXGWTWOWRWSWMWNUCUGUJUHUKXFXDWPMJGHWRWHWOULUMUNKUOAWPWLMJGHAWMG - RZWNHRZUPZWOWKPQZWPWLVBAXJXKAXJUPWMWIWNWJAXHWMORXIAGOWMAGOUQZGVCURZCNBNZP - QZCGUSBOSZATXNPQZBGUSZXQBHUSZUPZXLXMXPUTZHOUQZHVCURZXOCHUSBOSZUTZLVAZVDVE - VFAWIORZXJAYAYGYFBCGVGVHVIAXIWNORXHAHOWNAYBYCYDAXTYAYELVJZVDVEVKAWJORZXJA - YEYIYHBCHVGVHVIAXHTWMPQZXIAXHYJAXRXHYJVBAXTYAYEUTZXRLXRXSYAYEVNVLXQYJBWMG - XNWMTPVMVOVHWDVFAXITWNPQZXHAXIYLAXSXIYLVBAYKXSLXRXSYAYEVPVLXQYLBWNHXNWNTP - VMVOVHWDVKAXHWMWIPQZXIAYAXHYMYFBCGWMVQVRVFAXIWNWJPQZXHAYEXIYNYHBCHWNVQVRV - KVSWEWPWLXKWHWOWKPVTWAWBWCWFWG $. + co eqeq2d cbvrexvw eqeq1 2rexbidv syl5bb elab2 wa wi wss wne wral simp2bi + c0 w3a simp1d sselda adantrr suprcl syl adantr simp3bi simp1l sylbi breq2 + adantrl rspccv imp simp1r suprub sylan lemul12ad breq1 biimprcd rexlimdvv + ex syl6 syl5bi ralrimiv ) AENZGOUAUBZHOUAUBZUCUIZPQZEIWHIRWHMNZJNZUCUIZUD + ZJHSMGSZAWLDNZFNZWNUCUIZUDZJHSZFGSZWQDWHIEUEXCWRWOUDZJHSZMGSDEUFZWQXBXEFM + GFMUFZXAXDJHXGWTWOWRWSWMWNUCUGUJUHUKXFXDWPMJGHWRWHWOULUMUNKUOAWPWLMJGHAWM + GRZWNHRZUPZWOWKPQZWPWLUQAXJXKAXJUPWMWIWNWJAXHWMORXIAGOWMAGOURZGVBUSZCNBNZ + PQZCGUTBOSZATXNPQZBGUTZXQBHUTZUPZXLXMXPVCZHOURZHVBUSZXOCHUTBOSZVCZLVAZVDV + EVFAWIORZXJAYAYGYFBCGVGVHVIAXIWNORXHAHOWNAYBYCYDAXTYAYELVJZVDVEVNAWJORZXJ + AYEYIYHBCHVGVHVIAXHTWMPQZXIAXHYJAXRXHYJUQAXTYAYEVCZXRLXRXSYAYEVKVLXQYJBWM + GXNWMTPVMVOVHVPVFAXITWNPQZXHAXIYLAXSXIYLUQAYKXSLXRXSYAYEVQVLXQYLBWNHXNWNT + PVMVOVHVPVNAXHWMWIPQZXIAYAXHYMYFBCGWMVRVSVFAXIWNWJPQZXHAYEXIYNYHBCHWNVRVS + VNVTWDWPWLXKWHWOWKPWAWBWEWCWFWG $. $( Lemma for ~ supmul . (Contributed by Mario Carneiro, 5-Jul-2013.) $) supmullem2 $p |- ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) ) $= ( va cr cv cle wral wrex wcel cmul wss c0 wne wbr wceq vex eqeq2d rexbidv - co oveq1 cbvrexv eqeq1 2rexbidv syl5bb elab2 wa wi cc0 w3a simp2bi simp1d - sseld simp3bi anim12d remulcl syl6 eleq1a rexlimdvv syl5bi ssrdv wex ovex - simp2d isseti rgenw r19.2z sylancl rexcom4 sylib ralrimivw n0 exbii bitri - syl2anc sylibr clt csup suprcl syl remulcld supmullem1 brralrspcev 3jca ) - AINUAIUBUCZEOZBOZPUDEIQBNRZAEINWOISZWOMOZJOZTUIZUEZJHRZMGRZAWONSZDOZFOZWT - TUIZUEZJHRZFGRZXDDWOIEUFXKXFXAUEZJHRZMGRXFWOUEZXDXJXMFMGXGWSUEZXIXLJHXOXH - XAXFXGWSWTTUJUGUHUKXNXLXBMJGHXFWOXAULUMUNKUOZAXBXEMJGHAWSGSZWTHSZUPZXANSZ - XBXEUQAXSWSNSZWTNSZUPXTAXQYAXRYBAGNWSAGNUAZGUBUCZCOWPPUDZCGQBNRZAURWPPUDZ - BGQYGBHQUPZYCYDYFUSZHNUAZHUBUCZYECHQBNRZUSZLUTZVAVBAHNWTAYJYKYLAYHYIYMLVC - ZVAVBVDWSWTVEVFXANWOVGVFVHVIVJAXDEVKZWNAXCEVKZMGRZYPAYDYQMGQYRAYCYDYFYNVM - AYQMGAXBEVKZJHRZYQAYKYSJHQYTAYJYKYLYOVMYSJHEXAWSWTTVLVNVOYSJHVPVQXBJEHVRV - SVTYQMGVPWDXCMEGVRVSWNWREVKYPEIWAWRXDEXPWBWCWEAGNWFWGZHNWFWGZTUIZNSWOUUCP - UDEIQWQAUUAUUBAYIUUANSYNBCGWHWIAYMUUBNSYOBCHWHWIWJABCDEFGHIJKLWKBEWOUUCPN - IWLWDWM $. + co oveq1 cbvrexvw eqeq1 2rexbidv syl5bb elab2 wa wi cc0 w3a simp2bi sseld + simp1d simp3bi anim12d syl6 eleq1a rexlimdvv syl5bi ssrdv wex simp2d ovex + remulcl isseti rgenw r19.2z sylancl rexcom4 sylib ralrimivw syl2anc exbii + n0 bitri sylibr clt csup suprcl syl remulcld supmullem1 brralrspcev 3jca + ) AINUAIUBUCZEOZBOZPUDEIQBNRZAEINWOISZWOMOZJOZTUIZUEZJHRZMGRZAWONSZDOZFOZ + WTTUIZUEZJHRZFGRZXDDWOIEUFXKXFXAUEZJHRZMGRXFWOUEZXDXJXMFMGXGWSUEZXIXLJHXO + XHXAXFXGWSWTTUJUGUHUKXNXLXBMJGHXFWOXAULUMUNKUOZAXBXEMJGHAWSGSZWTHSZUPZXAN + SZXBXEUQAXSWSNSZWTNSZUPXTAXQYAXRYBAGNWSAGNUAZGUBUCZCOWPPUDZCGQBNRZAURWPPU + DZBGQYGBHQUPZYCYDYFUSZHNUAZHUBUCZYECHQBNRZUSZLUTZVBVAAHNWTAYJYKYLAYHYIYML + VCZVBVAVDWSWTVMVEXANWOVFVEVGVHVIAXDEVJZWNAXCEVJZMGRZYPAYDYQMGQYRAYCYDYFYN + VKAYQMGAXBEVJZJHRZYQAYKYSJHQYTAYJYKYLYOVKYSJHEXAWSWTTVLVNVOYSJHVPVQXBJEHV + RVSVTYQMGVPWAXCMEGVRVSWNWREVJYPEIWCWRXDEXPWBWDWEAGNWFWGZHNWFWGZTUIZNSWOUU + CPUDEIQWQAUUAUUBAYIUUANSYNBCGWHWIAYMUUBNSYOBCHWHWIWJABCDEFGHIJKLWKBEWOUUC + PNIWLWAWM $. $( The supremum function distributes over multiplication, in the sense that ` ( sup A ) x. ( sup B ) = sup ( A x. B ) ` , where ` A x. B ` is @@ -125631,38 +125631,38 @@ Dedekind cut construction of the reals (see ~ df-mp ). (Contributed by w3a cc0 wa simp2bi suprcl syl simp3bi cc mulcom syl2an syl2anc wex simp2d recn n0 sylib 0red simp1d sselda adantr wi simp1r sylbi rspccv imp suprub breq2 sylan letrd exlimddv simp1l eqid supmul1 syl31anc eqtrd vex rexbidv - biid eqeq1 elab rspe oveq1 eqeq2d cbvrexv 2rexbidv syl5bb elab2 sylibr ex - supmullem2 sylan9r syl5bi ralrimiv adantlr remulcld eleq1a rexlimdva ovex - wb abssdv isseti r19.2z sylancl rexcom4 cbvexvw abn0 brralrspcev suprleub - rgenw mpbird eqbrtrd breq1 syl5ibrcom supmullem1 letri3d mpbir2and ) AFNU - AUBZGNUAUBZUCUDZHNUAUBZOYHYIPQYIYHPQZAYHDUEZYGLUEZUCUDZOZLFRZDUFZNUAUBZYI - PAYHYGYFUCUDZYQAYFNSZYGNSZYHYROZAFNUGZFUHUIZCUEBUEZPQZCFTBNRZUJZYSAUKUUDP - QZBFTZUUHBGTZULZUUGGNUGZGUHUIZUUECGTBNRZUJZKUMZBCFUNUOZAUUOYTAUUKUUGUUOKU - PZBCGUNUOZYSYFUQSYGUQSZUUAYTYFVCYGVCZYFYGURUSUTAYTUKYGPQZUUIUUGYRYQOUUSAI - UEZGSZUVBIAUUMUVDIVAAUULUUMUUNUURVBZIGVDVEAUVDULZUKUVCYGUVFVFAGNUVCAUULUU - MUUNUURVGVHZAYTUVDUUSVIAUVDUKUVCPQZAUUJUVDUVHVJAUUKUUGUUOUJZUUJKUUIUUJUUG - UUOVKVLZUUHUVHBUVCGUUDUVCUKPVPVMUOVNAUUOUVDUVCYGPQUURBCGUVCVOVQVRVSAUVIUU - IKUUIUUJUUGUUOVTVLZUUPYTUVBUUIUJUUGULZBCDLYGFYPYPWAUVLWGWBWCWDAYQYIPQZMUE - ZYIPQZMYPTZAUVOMYPUVNYPSUVNYMOZLFRZAUVOYOUVRDUVNMWEZYKUVNOZYNUVQLFYKUVNYM - WHWFWIAUVQUVOLFAYLFSZULZUVOUVQYMYIPQUWBYMYLYGUCUDZYIPUWBYTYLNSZYMUWCOZAYT - UWAUUSVIZAFNYLAUUBUUCUUFUUPVGVHZYTUUTYLUQSUWEUWDUVAYLVCYGYLURUSUTUWBUWCYK - YLUVCUCUDZOZIGRZDUFZNUAUBZYIPUWBUWDUKYLPQZUUJUUOUWCUWLOUWGAUWAUWMAUUIUWAU - WMVJUVKUUHUWMBYLFUUDYLUKPVPVMUOVNAUUJUWAUVJVIAUUOUWAUURVIUWDUWMUUJUJUUOUL - ZBCDIYLGUWKUWKWAUWNWGWBWCUWBUWLYIPQZUVOMUWKTZUWBUVOMUWKUVNUWKSUVNUWHOZIGR - ZUWBUVOUWJUWRDUVNUVSUVTUWIUWQIGYKUVNUWHWHZWFZWIUWAUWRUVNHSZAUVOUWAUWRUXAU - WAUWRULUWRLFRZUXAUWRLFWJYKEUEZUVCUCUDZOZIGRZEFRZUXBDUVNHUVSUXGUWJLFRUVTUX - BUXFUWJELFUXCYLOZUXEUWIIGUXHUXDUWHYKUXCYLUVCUCWKWLWFWMUVTUWIUWQLIFGUWSWNW - OJWPWQWRAHNUGHUHUIUVNUUDPQZMHTBNRUJZUXAUVOVJABCDMEFGHIJKWSZUXJUXAUVOBMHUV - NVOWRUOWTXAXBZUWBUWKNUGUWKUHUIZUXIMUWKTBNRZYINSZUWOUWPXHUWBUWJDNUWBUWIYKN - SZIGUWBUVDULZUWHNSUWIUXPVJUXQYLUVCUWBUWDUVDUWGVIAUVDUVCNSUWAUVGXCXDUWHNYK - XEUOXFXIAUXMUWAAUWJDVAZUXMAUWRMVAZUXRAUWQMVAZIGRZUXSAUUMUXTIGTUYAUVEUXTIG - MUWHYLUVCUCXGXJXRUXTIGXKXLUWQIMGXMVEUWJUWRDMUWTXNWQUWJDXOWQVIUWBUXOUWPUXN - AUXOUWAAUXJUXOUXKBMHUNUOZVIZUXLBMUVNYIPNUWKXPUTUYCBMMUWKYIXQWCXSXTXTUVNYM - YIPYAYBXFXAXBZAYPNUGYPUHUIZUXIMYPTBNRZUXOUVMUVPXHAYODNAYNUXPLFUWBYMNSYNUX - PVJUWBYGYLUWFUWGXDYMNYKXEUOXFXIAYODVAZUYEAYNDVAZLFRZUYGAUUCUYHLFTUYIAUUBU - UCUUFUUPVBUYHLFDYMYGYLUCXGXJXRUYHLFXKXLYNLDFXMVEYODXOWQAUXOUVPUYFUYBUYDBM - UVNYIPNYPXPUTUYBBMMYPYIXQWCXSXTAYJUVNYHPQMHTZABCDMEFGHIJKYCAUXJYHNSYJUYJX - HUXKAYFYGUUQUUSXDZBMMHYHXQUTXSAYHYIUYKUYBYDYE $. + biid eqeq1 elab rspe oveq1 eqeq2d cbvrexvw syl5bb elab2 sylibr supmullem2 + 2rexbidv sylan9r syl5bi ralrimiv adantlr remulcld eleq1a rexlimdva abssdv + ex wb ovex isseti rgenw sylancl rexcom4 cbvexvw abn0 brralrspcev suprleub + r19.2z mpbird eqbrtrd breq1 syl5ibrcom supmullem1 letri3d mpbir2and ) AFN + UAUBZGNUAUBZUCUDZHNUAUBZOYHYIPQYIYHPQZAYHDUEZYGLUEZUCUDZOZLFRZDUFZNUAUBZY + IPAYHYGYFUCUDZYQAYFNSZYGNSZYHYROZAFNUGZFUHUIZCUEBUEZPQZCFTBNRZUJZYSAUKUUD + PQZBFTZUUHBGTZULZUUGGNUGZGUHUIZUUECGTBNRZUJZKUMZBCFUNUOZAUUOYTAUUKUUGUUOK + UPZBCGUNUOZYSYFUQSYGUQSZUUAYTYFVCYGVCZYFYGURUSUTAYTUKYGPQZUUIUUGYRYQOUUSA + IUEZGSZUVBIAUUMUVDIVAAUULUUMUUNUURVBZIGVDVEAUVDULZUKUVCYGUVFVFAGNUVCAUULU + UMUUNUURVGVHZAYTUVDUUSVIAUVDUKUVCPQZAUUJUVDUVHVJAUUKUUGUUOUJZUUJKUUIUUJUU + GUUOVKVLZUUHUVHBUVCGUUDUVCUKPVPVMUOVNAUUOUVDUVCYGPQUURBCGUVCVOVQVRVSAUVIU + UIKUUIUUJUUGUUOVTVLZUUPYTUVBUUIUJUUGULZBCDLYGFYPYPWAUVLWGWBWCWDAYQYIPQZMU + EZYIPQZMYPTZAUVOMYPUVNYPSUVNYMOZLFRZAUVOYOUVRDUVNMWEZYKUVNOZYNUVQLFYKUVNY + MWHWFWIAUVQUVOLFAYLFSZULZUVOUVQYMYIPQUWBYMYLYGUCUDZYIPUWBYTYLNSZYMUWCOZAY + TUWAUUSVIZAFNYLAUUBUUCUUFUUPVGVHZYTUUTYLUQSUWEUWDUVAYLVCYGYLURUSUTUWBUWCY + KYLUVCUCUDZOZIGRZDUFZNUAUBZYIPUWBUWDUKYLPQZUUJUUOUWCUWLOUWGAUWAUWMAUUIUWA + UWMVJUVKUUHUWMBYLFUUDYLUKPVPVMUOVNAUUJUWAUVJVIAUUOUWAUURVIUWDUWMUUJUJUUOU + LZBCDIYLGUWKUWKWAUWNWGWBWCUWBUWLYIPQZUVOMUWKTZUWBUVOMUWKUVNUWKSUVNUWHOZIG + RZUWBUVOUWJUWRDUVNUVSUVTUWIUWQIGYKUVNUWHWHZWFZWIUWAUWRUVNHSZAUVOUWAUWRUXA + UWAUWRULUWRLFRZUXAUWRLFWJYKEUEZUVCUCUDZOZIGRZEFRZUXBDUVNHUVSUXGUWJLFRUVTU + XBUXFUWJELFUXCYLOZUXEUWIIGUXHUXDUWHYKUXCYLUVCUCWKWLWFWMUVTUWIUWQLIFGUWSWR + WNJWOWPXGAHNUGHUHUIUVNUUDPQZMHTBNRUJZUXAUVOVJABCDMEFGHIJKWQZUXJUXAUVOBMHU + VNVOXGUOWSWTXAZUWBUWKNUGUWKUHUIZUXIMUWKTBNRZYINSZUWOUWPXHUWBUWJDNUWBUWIYK + NSZIGUWBUVDULZUWHNSUWIUXPVJUXQYLUVCUWBUWDUVDUWGVIAUVDUVCNSUWAUVGXBXCUWHNY + KXDUOXEXFAUXMUWAAUWJDVAZUXMAUWRMVAZUXRAUWQMVAZIGRZUXSAUUMUXTIGTUYAUVEUXTI + GMUWHYLUVCUCXIXJXKUXTIGXRXLUWQIMGXMVEUWJUWRDMUWTXNWPUWJDXOWPVIUWBUXOUWPUX + NAUXOUWAAUXJUXOUXKBMHUNUOZVIZUXLBMUVNYIPNUWKXPUTUYCBMMUWKYIXQWCXSXTXTUVNY + MYIPYAYBXEWTXAZAYPNUGYPUHUIZUXIMYPTBNRZUXOUVMUVPXHAYODNAYNUXPLFUWBYMNSYNU + XPVJUWBYGYLUWFUWGXCYMNYKXDUOXEXFAYODVAZUYEAYNDVAZLFRZUYGAUUCUYHLFTUYIAUUB + UUCUUFUUPVBUYHLFDYMYGYLUCXIXJXKUYHLFXRXLYNLDFXMVEYODXOWPAUXOUVPUYFUYBUYDB + MUVNYIPNYPXPUTUYBBMMYPYIXQWCXSXTAYJUVNYHPQMHTZABCDMEFGHIJKYCAUXJYHNSYJUYJ + XHUXKAYFYGUUQUUSXCZBMMHYHXQUTXSAYHYIUYKUYBYDYE $. $} ${ @@ -125735,13 +125735,13 @@ Dedekind cut construction of the reals (see ~ df-mp ). (Contributed by negiso $p |- ( F Isom < , `' < ( RR , RR ) /\ `' F = F ) $= ( vz vy cr clt ccnv wceq cv wbr cfv wb wral cneg cmpt wa wtru wcel negeq wiso wf1o simpr renegcld recn negcon2 syl2an adantl f1ocnv2d mptru simpli - ltneg negex brcnv syl6bbr fvmpt breqan12d bitr4d df-isom mpbir2an cbvmptv - cc rgen2a simpri 3eqtr4i pm3.2i ) FFGGHZBUAZBHZBIVHFFBUBZDJZEJZGKZVKBLZVL - BLZVGKZMZEFNDFNVJVIEFVLOZPZIZVJVTQRAEFFAJZOZVRBCRWAFSZQWARWCUCUDRVLFSZQVL - RWDUCUDWCWDQWAVRIVLWBIMZRWCWAVBSVLVBSWEWDWAUEVLUEWAVLUFUGUHUIUJZUKVQDEFVK - FSZWDQZVMVKOZVRVGKZVPWHVMVRWIGKWJVKVLULWIVRGVKUMZVLUMZUNUOWGWDVNWIVOVRVGA - VKWBWIFBWAVKTCWKUPAVLWBVRFBWAVLTCWLUPUQURVCDEFFGVGBUSUTVSAFWBPVIBEAFVRWBV - LWATVAVJVTWFVDCVEVF $. + cc ltneg negex brcnv syl6bbr fvmpt breqan12d bitr4d rgen2 df-isom cbvmptv + mpbir2an simpri 3eqtr4i pm3.2i ) FFGGHZBUAZBHZBIVHFFBUBZDJZEJZGKZVKBLZVLB + LZVGKZMZEFNDFNVJVIEFVLOZPZIZVJVTQRAEFFAJZOZVRBCRWAFSZQWARWCUCUDRVLFSZQVLR + WDUCUDWCWDQWAVRIVLWBIMZRWCWAULSVLULSWEWDWAUEVLUEWAVLUFUGUHUIUJZUKVQDEFFVK + FSZWDQZVMVKOZVRVGKZVPWHVMVRWIGKWJVKVLUMWIVRGVKUNZVLUNZUOUPWGWDVNWIVOVRVGA + VKWBWIFBWAVKTCWKUQAVLWBVRFBWAVLTCWLUQURUSUTDEFFGVGBVAVCVSAFWBPVIBEAFVRWBV + LWATVBVJVTWFVDCVEVF $. $} ${ @@ -126460,23 +126460,23 @@ subset of complex numbers ( ~ nnsscn ), in contrast to the more elementary (Revised by Mario Carneiro, 16-May-2014.) $) nnsub $p |- ( ( A e. NN /\ B e. NN ) -> ( A < B <-> ( B - A ) e. NN ) ) $= ( vz vx cn wcel clt wbr cmin co wi wral wceq breq2 eleq1d imbi12d ralbidv - c1 oveq1 cr vy wa cv caddc nnnlt1 pm2.21d rgen breq1 oveq2 cbvralv adantr - cc nncn ax-1cn pncan sylancl simpl eqeltrd syl5ibrcom 2a1dd rspcv wb nnre - 1re ltsubadd mp3an2 syl2anr subsub3 mp3an3 syl2an biimpd syl9r wo nn1m1nn - adantl mpjaod ralrimdva syl5bi nnind rspcva sylan2 posdif syl5ibr impbid + c1 oveq1 cr vy wa cv caddc nnnlt1 pm2.21d rgen breq1 cbvralvw nncn adantr + oveq2 cc ax-1cn pncan sylancl simpl eqeltrd syl5ibrcom 2a1dd rspcv wb 1re + nnre ltsubadd mp3an2 syl2anr subsub3 mp3an3 syl2an biimpd syl9r wo adantl + nn1m1nn mpjaod ralrimdva syl5bi nnind rspcva sylan2 posdif syl5ibr impbid cc0 nngt0 ) AEFZBEFZUBZABGHZBAIJZEFZWHWGCUCZBGHZBWMIJZEFZKZCELZWJWLKZWMDU CZGHZWTWMIJZEFZKZCELWMRGHZRWMIJZEFZKZCELWMUAUCZGHZXIWMIJZEFZKZCELZWMXIRUD JZGHZXOWMIJZEFZKZCELZWRDUABWTRMZXDXHCEYAXAXEXCXGWTRWMGNYAXBXFEWTRWMISOPQW TXIMZXDXMCEYBXAXJXCXLWTXIWMGNYBXBXKEWTXIWMISOPQWTXOMZXDXSCEYCXAXPXCXRWTXO WMGNYCXBXQEWTXOWMISOPQWTBMZXDWQCEYDXAWNXCWPWTBWMGNYDXBWOEWTBWMISOPQXHCEWM EFZXEXGWMUEUFUGXNWTXIGHZXIWTIJZEFZKZDELZXIEFZXTXMYICDEWMWTMZXJYFXLYHWMWTX - IGUHYLXKYGEWMWTXIIUIOPUJYKYJXSCEYKYEUBZWMRMZYJXSKWMRIJZEFZYMYNXRYJXPYMXRY - NXORIJZEFYMYQXIEYMXIULFZRULFZYQXIMYKYRYEXIUMZUKUNXIRUOUPYKYEUQURYNXQYQEWM - RXOIUIOUSUTYPYJYOXIGHZXIYOIJZEFZKZYMXSYIUUDDYOEWTYOMZYFUUAYHUUCWTYOXIGUHU - UEYGUUBEWTYOXIIUIOPVAYMUUDXSYMUUAXPUUCXRYEWMTFZXITFZUUAXPVBZYKWMVCXIVCUUF - RTFUUGUUHVDWMRXIVEVFVGYMUUBXQEYKYRWMULFZUUBXQMZYEYTWMUMYRUUIYSUUJUNXIWMRV - HVIVJOPVKVLYEYNYPVMYKWMVNVOVPVQVRVSWQWSCAEWMAMZWNWJWPWLWMABGUHUUKWOWKEWMA - BIUIOPVTWAWLWJWIWEWKGHZWKWFWGATFBTFWJUULVBWHAVCBVCABWBVJWCWD $. + IGUHYLXKYGEWMWTXIIULOPUIYKYJXSCEYKYEUBZWMRMZYJXSKWMRIJZEFZYMYNXRYJXPYMXRY + NXORIJZEFYMYQXIEYMXIUMFZRUMFZYQXIMYKYRYEXIUJZUKUNXIRUOUPYKYEUQURYNXQYQEWM + RXOIULOUSUTYPYJYOXIGHZXIYOIJZEFZKZYMXSYIUUDDYOEWTYOMZYFUUAYHUUCWTYOXIGUHU + UEYGUUBEWTYOXIIULOPVAYMUUDXSYMUUAXPUUCXRYEWMTFZXITFZUUAXPVBZYKWMVDXIVDUUF + RTFUUGUUHVCWMRXIVEVFVGYMUUBXQEYKYRWMUMFZUUBXQMZYEYTWMUJYRUUIYSUUJUNXIWMRV + HVIVJOPVKVLYEYNYPVMYKWMVOVNVPVQVRVSWQWSCAEWMAMZWNWJWPWLWMABGUHUUKWOWKEWMA + BIULOPVTWAWLWJWIWEWKGHZWKWFWGATFBTFWJUULVBWHAVDBVDABWBVJWCWD $. nnsub.1 $e |- A e. NN $. nnsub.2 $e |- B e. NN $. @@ -131248,10 +131248,10 @@ nonnegative integers (cont.)". $) induction step. (Contributed by NM, 4-Nov-2005.) $) uzind4s $p |- ( N e. ( ZZ>= ` M ) -> [. N / k ]. ph ) $= ( vj vm wsb wsbc cv c1 caddc co dfsbcq2 sbequ wcel wi nfim imbi12d eleq1w - cuz cfv nfv nfs1v nfsbc1v weq sbequ12 oveq1 sbceq1d chvar uzind4 ) ABGIAB - CJABHIZABHKZLMNZJZABDJGHCDABGCOAGHBPABGUOOABGDOEBKZCUBUCZQZAABUQLMNZJZRZR - UNURQZUMUPRZRBHVCVDBVCBUDUMUPBABHUEABUOUFSSBHUGZUSVCVBVDBHURUAVEAUMVAUPAB - HUHVEABUTUOUQUNLMUIUJTTFUKUL $. + cuz cfv nfv nfs1v nfsbc1v weq sbequ12 oveq1 sbceq1d chvarfv uzind4 ) ABGI + ABCJABHIZABHKZLMNZJZABDJGHCDABGCOAGHBPABGUOOABGDOEBKZCUBUCZQZAABUQLMNZJZR + ZRUNURQZUMUPRZRBHVCVDBVCBUDUMUPBABHUEABUOUFSSBHUGZUSVCVBVDBHURUAVEAUMVAUP + ABHUHVEABUTUOUQUNLMUIUJTTFUKUL $. $} ${ @@ -131308,22 +131308,22 @@ nonnegative integers (cont.)". $) sstr zleltp1 peano2re syl ltnle bitrd ancoms anbi2d sylan2 eleq1a sylbird ad2antll expd con1 com23 exp32 com34 ralimdva sylan9r pm2.43d expl sylani ex a2d uzind4i adantl sylcom adantrd pm2.61i alrimdv eq0 syl6ibr necon1ad - imp41 imp breq2 cbvralv rexbii sylib ) ADUAUDZUEZAUFUGZGBHZEHZIJZEAKZBAUH - ZXLCHZIJZCAKZBAUHXJXKXPXJXPAUFXJXPLZFHZAMZLZFUIAUFNXJXTYCFXJXTYCYAXIMZXJX - TGZYCOYDYEYAXMIJZEAKZYCYEUBHZXMIJZEAKZOYEDXMIJZEAKZOYEUCHZXMIJZEAKZOYEYMU - JUKULZXMIJZEAKZOYEYGOUBUCDYAYHDNZYJYLYEYSYIYKEAYHDXMIPQRYHYMNZYJYOYEYTYIY - NEAYHYMXMIPQRYHYPNZYJYRYEUUAYIYQEAYHYPXMIPQRYHYANZYJYGYEUUBYIYFEAYHYAXMIP - QRXJYLXTXJYKEAXJXMAMZXMXIMYKAXIXMUMDXMUNUOUPURYMXIMZYEYOYRXJUUDASUEZXTYOY - ROZXJXISUEUUEDUQAXISVJUSUUDYMSMZUUEXTGUUFODYMUTUUGUUEXTUUFUUGUUEGZXTGYOYR - XTYOYMAMZLZUUHUUFYOUUIXPUUIYOXPXOYOBYMAXLYMNXNYNEAXLYMXMIPQVAVBVCUUHUUJUU - FUUHUUJGYNYQEAUUGUUEUUJUUCYNYQOZUUGUUEUUCUUJUUKUUGUUEUUCUUJUUKOUUGUUEUUCG - ZGZYNUUJYQUUMYNYQLZUUIOUUJYQOUUMYNUUNUUIUUMYNUUNGZYMXMNZUUIUULUUGXMSMZUUP - UUOTASXMVDUUGUUQGZUUPYNXMYMIJZGZUUOUUGYMVEMZXMVEMZUUPUUTTUUQYMVFZXMVFZYMX - MVGVHUURUUSUUNYNUUQUUGUUSUUNTUUQUUGGUUSXMYPVIJZUUNXMYMVKUUQUVBYPVEMZUVEUU - NTUUGUVDUUGUVAUVFUVCYMVLVMXMYPVNVHVOVPVQVOVRUUCUUPUUIOUUGUUEXMAYMVSWAVTWB - YQUUIWCUOWDWEWFXCWGWLWHWIWJVMWKWMWNXTYGYCOXJYGYBXPYBYGXPXOYGBYAAXLYANXNYF - EAXLYAXMIPQVAVBVCWOWPYDLXJYCXTXJYBYDAXIYAUMVCWQWRWLWSFAWTXAXBXDXOXSBAXNXR - ECAXMXQXLIXEXFXGXH $. + imp41 imp breq2 cbvralvw rexbii sylib ) ADUAUDZUEZAUFUGZGBHZEHZIJZEAKZBAU + HZXLCHZIJZCAKZBAUHXJXKXPXJXPAUFXJXPLZFHZAMZLZFUIAUFNXJXTYCFXJXTYCYAXIMZXJ + XTGZYCOYDYEYAXMIJZEAKZYCYEUBHZXMIJZEAKZOYEDXMIJZEAKZOYEUCHZXMIJZEAKZOYEYM + UJUKULZXMIJZEAKZOYEYGOUBUCDYAYHDNZYJYLYEYSYIYKEAYHDXMIPQRYHYMNZYJYOYEYTYI + YNEAYHYMXMIPQRYHYPNZYJYRYEUUAYIYQEAYHYPXMIPQRYHYANZYJYGYEUUBYIYFEAYHYAXMI + PQRXJYLXTXJYKEAXJXMAMZXMXIMYKAXIXMUMDXMUNUOUPURYMXIMZYEYOYRXJUUDASUEZXTYO + YROZXJXISUEUUEDUQAXISVJUSUUDYMSMZUUEXTGUUFODYMUTUUGUUEXTUUFUUGUUEGZXTGYOY + RXTYOYMAMZLZUUHUUFYOUUIXPUUIYOXPXOYOBYMAXLYMNXNYNEAXLYMXMIPQVAVBVCUUHUUJU + UFUUHUUJGYNYQEAUUGUUEUUJUUCYNYQOZUUGUUEUUCUUJUUKUUGUUEUUCUUJUUKOUUGUUEUUC + GZGZYNUUJYQUUMYNYQLZUUIOUUJYQOUUMYNUUNUUIUUMYNUUNGZYMXMNZUUIUULUUGXMSMZUU + PUUOTASXMVDUUGUUQGZUUPYNXMYMIJZGZUUOUUGYMVEMZXMVEMZUUPUUTTUUQYMVFZXMVFZYM + XMVGVHUURUUSUUNYNUUQUUGUUSUUNTUUQUUGGUUSXMYPVIJZUUNXMYMVKUUQUVBYPVEMZUVEU + UNTUUGUVDUUGUVAUVFUVCYMVLVMXMYPVNVHVOVPVQVOVRUUCUUPUUIOUUGUUEXMAYMVSWAVTW + BYQUUIWCUOWDWEWFXCWGWLWHWIWJVMWKWMWNXTYGYCOXJYGYBXPYBYGXPXOYGBYAAXLYANXNY + FEAXLYAXMIPQVAVBVCWOWPYDLXJYCXTXJYBYDAXIYAUMVCWQWRWLWSFAWTXAXBXDXOXSBAXNX + RECAXMXQXLIXEXFXGXH $. $( Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. (Contributed by NM, 8-Oct-2005.) $) @@ -131353,10 +131353,10 @@ nonnegative integers (cont.)". $) ` A ` as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.) $) nnwof $p |- ( ( A C_ NN /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y ) $= - ( vw vv cn wss c0 wne wa cv cle wbr wral wrex nnwo nfcv nfv nfral ralbidv - weq breq1 breq2 cbvralf syl6bb cbvrexf sylib ) CHICJKLFMZGMZNOZGCPZFCQAMZ - BMZNOZBCPZACQFGCRUMUQFACFCSDULAGCDULATUAUQFTFAUCZUMUNUKNOZGCPUQURULUSGCUJ - UNUKNUDUBUSUPGBCGCSEUSBTUPGTUKUOUNNUEUFUGUHUI $. + ( vw vv cn wss c0 wne wa cv cle wbr wral wrex nnwo nfcv nfv breq1 ralbidv + nfralw weq breq2 cbvralfw syl6bb cbvrexfw sylib ) CHICJKLFMZGMZNOZGCPZFCQ + AMZBMZNOZBCPZACQFGCRUMUQFACFCSDULAGCDULATUCUQFTFAUDZUMUNUKNOZGCPUQURULUSG + CUJUNUKNUAUBUSUPGBCGCSEUSBTUPGTUKUOUNNUEUFUGUHUI $. $} ${ @@ -131532,15 +131532,15 @@ least element (schema form). (Contributed by NM, 17-Aug-2001.) $) below. (Contributed by Paul Chapman, 21-Mar-2011.) $) ublbneg $p |- ( E. x e. RR A. y e. A y <_ x -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y ) $= - ( vb va cv cle wbr wral cr wrex cneg wcel crab breq1 cbvralv wceq ralbidv - rexbii breq2 cbvrexv bitri renegcl wa wi elrabi negeq eleq1d elrab3 mpcom - biimpd rspcv adantl wb lenegcon1 sylan2 sylibrd ralrimdva rspcev rexlimiv - syl syl6an sylbir ) BGZAGZHIZBDJZAKLZEGZFGZHIZEDJZFKLZVFVEHIZBCGZMZDNZCKO - ZJZAKLZVNVEVKHIZBDJZFKLVIVMWCFKVLWBEBDVJVEVKHPQTWCVHFAKVKVFRWBVGBDVKVFVEH - UASUBUCVMWAFKVKKNZVKMZKNVMWEVEHIZBVSJZWAVKUDWDVMWFBVSWDVEVSNZUEVMVEMZVKHI - ZWFWHVMWJUFZWDWHWIDNZWKVEKNZWHWLVRCVEKUGZWMWHWLVRWLCVEKVPVERVQWIDVPVEUHUI - UJULUKVLWJEWIDVJWIVKHPUMVBUNWHWDWMWFWJUOWNVKVEUPUQURUSVTWGAWEKVFWERVOWFBV - SVFWEVEHPSUTVCVAVD $. + ( vb va cv cle wbr wral cr wrex cneg wcel crab breq1 cbvralvw rexbii wceq + ralbidv breq2 cbvrexvw bitri renegcl wa elrabi negeq eleq1d elrab3 biimpd + wi mpcom rspcv adantl wb lenegcon1 sylan2 sylibrd ralrimdva rspcev syl6an + syl rexlimiv sylbir ) BGZAGZHIZBDJZAKLZEGZFGZHIZEDJZFKLZVFVEHIZBCGZMZDNZC + KOZJZAKLZVNVEVKHIZBDJZFKLVIVMWCFKVLWBEBDVJVEVKHPQRWCVHFAKVKVFSWBVGBDVKVFV + EHUATUBUCVMWAFKVKKNZVKMZKNVMWEVEHIZBVSJZWAVKUDWDVMWFBVSWDVEVSNZUEVMVEMZVK + HIZWFWHVMWJUKZWDWHWIDNZWKVEKNZWHWLVRCVEKUFZWMWHWLVRWLCVEKVPVESVQWIDVPVEUG + UHUIUJULVLWJEWIDVJWIVKHPUMVBUNWHWDWMWFWJUOWNVKVEUPUQURUSVTWGAWEKVFWESVOWF + BVSVFWEVEHPTUTVAVCVD $. $} ${