From 3dba285543c8229c90c8cf03374606a9aca4e9f5 Mon Sep 17 00:00:00 2001 From: BTernaryTau Date: Thu, 9 Jan 2025 02:21:03 -0500 Subject: [PATCH] Generalize rexdif1en and dif1en (#4543) * Revise dif1enlem * Revise rexdif1en * Use revised rexdif1en in findcard2 * Revise dif1en * Prove dif1ennn * Use dif1ennn instead of dif1enOLD * Rename dif1enALT to dif1ennnALT --- discouraged | 13 +- set.mm | 421 ++++++++++++++++++++++++++++++---------------------- 2 files changed, 257 insertions(+), 177 deletions(-) diff --git a/discouraged b/discouraged index 85a5a30dbe..869df6b569 100644 --- a/discouraged +++ b/discouraged @@ -5292,6 +5292,9 @@ "dicdmN" is used by "dicvalrelN". "dicelvalN" is used by "dicelval2N". "dicfnN" is used by "dicdmN". +"dif1enOLD" is used by "findcard2OLD". +"dif1enlemOLD" is used by "dif1enOLD". +"dif1enlemOLD" is used by "rexdif1enOLD". "dihglbcN" is used by "dihmeetcN". "dihglbcpreN" is used by "dihglbcN". "dihglblem2N" is used by "dihglblem3N". @@ -16113,7 +16116,9 @@ New usage of "dicelval2N" is discouraged (0 uses). New usage of "dicelvalN" is discouraged (1 uses). New usage of "dicfnN" is discouraged (1 uses). New usage of "dicvalrelN" is discouraged (0 uses). -New usage of "dif1enALT" is discouraged (0 uses). +New usage of "dif1enOLD" is discouraged (1 uses). +New usage of "dif1enlemOLD" is discouraged (2 uses). +New usage of "dif1ennnALT" is discouraged (0 uses). New usage of "difidALT" is discouraged (0 uses). New usage of "difopabOLD" is discouraged (0 uses). New usage of "dih0bN" is discouraged (0 uses). @@ -18824,6 +18829,7 @@ New usage of "rexbiOLD" is discouraged (0 uses). New usage of "rexbidvALT" is discouraged (0 uses). New usage of "rexbidvaALT" is discouraged (0 uses). New usage of "rexcomOLD" is discouraged (0 uses). +New usage of "rexdif1enOLD" is discouraged (0 uses). New usage of "reximdvaiOLD" is discouraged (0 uses). New usage of "reximiaOLD" is discouraged (0 uses). New usage of "rexlimddvcbv" is discouraged (0 uses). @@ -20188,7 +20194,9 @@ Proof modification of "dfvd3anir" is discouraged (19 steps). Proof modification of "dfvd3i" is discouraged (19 steps). Proof modification of "dfvd3ir" is discouraged (19 steps). Proof modification of "dfwrecsOLD" is discouraged (619 steps). -Proof modification of "dif1enALT" is discouraged (335 steps). +Proof modification of "dif1enOLD" is discouraged (313 steps). +Proof modification of "dif1enlemOLD" is discouraged (285 steps). +Proof modification of "dif1ennnALT" is discouraged (335 steps). Proof modification of "difidALT" is discouraged (14 steps). Proof modification of "difopabOLD" is discouraged (171 steps). Proof modification of "dih2dimbALTN" is discouraged (450 steps). @@ -21194,6 +21202,7 @@ Proof modification of "rexbiOLD" is discouraged (65 steps). Proof modification of "rexbidvALT" is discouraged (10 steps). Proof modification of "rexbidvaALT" is discouraged (10 steps). Proof modification of "rexcomOLD" is discouraged (67 steps). +Proof modification of "rexdif1enOLD" is discouraged (120 steps). Proof modification of "reximdvaiOLD" is discouraged (28 steps). Proof modification of "reximiaOLD" is discouraged (21 steps). Proof modification of "rexlimivOLD" is discouraged (23 steps). diff --git a/set.mm b/set.mm index 7be3ee2ac4..39bf91b21e 100644 --- a/set.mm +++ b/set.mm @@ -92389,8 +92389,29 @@ excluded middle (LEM), and in ILE the LEM is not accepted as necessarily $) $( Lemma for ~ rexdif1en and ~ dif1en . (Contributed by BTernaryTau, - 18-Aug-2024.) $) - dif1enlem $p |- ( ( F e. V /\ M e. _om /\ F : A -1-1-onto-> suc M ) -> + 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to + avoid ~ ax-un . (Revised by BTernaryTau, 5-Jan-2025.) $) + dif1enlem $p |- ( ( ( F e. V /\ A e. W /\ M e. On ) /\ + F : A -1-1-onto-> suc M ) -> ( A \ { ( `' F ` M ) } ) ~~ M ) $= + ( wcel con0 wf1o cfv csn cdif cres wa wfo adantr wceq wb mpbird c0 cvv csuc + w3a ccnv cen wbr sucidg wfun dff1o3 simprbi f1ofo wfn f1ofn fnresdm 3syl wf + foeq1 wne f1ocnvdm f1ocnvfv2 snidg adantl eqeltrd fressnfv biimp3ar syl3anc + cin disjsn con2bii sylib fnresdisj syl neqned foconst syl2anc resdif sylan2 + wn mtbid word eloni orddif f1oeq3d ancoms 3ad2antl3 difexg f1oen4g syl3anl1 + resexg syl3anl2 syldan ) BDFZAEFZCGFZUBACUAZBHZACBUCZIZJZKZCBWSLZHZWSCUDUEZ + WMWKWOXAWLWOWMXAWOWMMXAWSWNCJZKZWTHZWMWOCWNFZXECGUFWOXFMZWPUGZAWNBALZNZWRXC + BWRLZNZXEWOXHXFWOAWNBNZXHAWNBUHUIOWOXJXFWOXJXMAWNBUJWOBAUKZXIBPXJXMQAWNBULZ + ABUMAWNXIBUPUNROXGWRXCXKUOZXKSUQXLXGXNWQAFZWQBIZXCFZXPWOXNXFXOOAWNCBURZXGXR + CXCAWNCBUSXFCXCFWOCWNUTVAVBXNXQXPXSAWQXCBVCVDVEXGXKSXGAWRVFSPZXKSPZXGXQYAVQ + XTYAXQAWQVGVHVIWOYAYBQZXFWOXNYCXOAWRBVJVKOVRVLWRCXKVMVNAWRWNXCBVOVEVPWMXAXE + QWOWMCXDWSWTWMCVSCXDPCVTCWAVKWBVARWCWDWLWKWSTFZWMXAXBAWREWEWKWTTFYDWMXAXBBW + SDWHWSCWTTTGWFWGWIWJ $. + $( $j usage 'dif1enlem' avoids 'ax-pow' 'ax-un'; $) + + $( Obsolete version of ~ dif1enlem as of 5-Jan-2025. (Contributed by + BTernaryTau, 18-Aug-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + dif1enlemOLD $p |- ( ( F e. V /\ M e. _om /\ F : A -1-1-onto-> suc M ) -> ( A \ { ( `' F ` M ) } ) ~~ M ) $= ( wcel com wf1o cfv csn cdif cres wa wfo adantr wb mpbird c0 adantl syl3anc wceq csuc w3a ccnv cen wbr simp1 sucidg wfun dff1o3 simprbi f1ofo wfn f1ofn @@ -92404,50 +92425,100 @@ excluded middle (LEM), and in ILE the LEM is not accepted as necessarily WJUTRVAXJXMXLXOAWMWSBVBVCSXCXGQXCAWNVDQTZXGQTZXCXMXQVPXPXQXMAWMVFVGVHWKXQXR OZXBWKXJXSXKAWNBVIVJNVKVLWNCXGVMVNAWNWJWSBVOSVQWIWQXAOWKWICWTWOWPWICVRCWTTC VSCVTVJWARPWBWCWHWPWDEWQWRBWODWEWOCWPWDWFWGVN $. - $( $j usage 'dif1enlem' avoids 'ax-pow'; $) ${ $d A f x $. $d M f x $. - $( If a set is equinumerous to a nonzero finite ordinal, then there exists - an element in that set such that removing it leaves the set equinumerous - to the predecessor of that ordinal. (Contributed by BTernaryTau, - 26-Aug-2024.) $) - rexdif1en $p |- ( ( M e. _om /\ A ~~ suc M ) -> + $( If a set is equinumerous to a nonzero ordinal, then there exists an + element in that set such that removing it leaves the set equinumerous to + the predecessor of that ordinal. (Contributed by BTernaryTau, + 26-Aug-2024.) Generalize to all ordinals and avoid ~ ax-un . (Revised + by BTernaryTau, 5-Jan-2025.) $) + rexdif1en $p |- ( ( M e. On /\ A ~~ suc M ) -> + E. x e. A ( A \ { x } ) ~~ M ) $= + ( vf con0 wcel csuc cen wbr cv csn cdif wrex wi cvv encv simpld wa ancoms + sylan wf1o wex wb breng syl ibi cfv sucidg f1ocnvdm adantll vex dif1enlem + ccnv mp3anl1 wceq sneq difeq2d breq1d rspcev syl2anc exlimdv syl5 syldbl2 + ex ) CEFZBCGZHIZBAJZKZLZCHIZABMZVGVEVGVLNZVGBOFZVEVMVGVNVFOFZBVFPZQVGBVFD + JZUAZDUBZVNVERZVLVGVSVGVNVORVGVSUCVPBVFDOOUDUEUFVTVRVLDVTVRVLVTVRRCVQUMUG + ZBFZBWAKZLZCHIZVLVEVRWBVNVECVFFZVRWBCEUHVRWFWBBVFCVQUISTUJVQOFVNVEVRWEDUK + BVQCOOULUNVKWEAWABVHWAUOZVJWDCHWGVIWCBVHWAUPUQURUSUTVDVAVBTSVC $. + $( $j usage 'rexdif1en' avoids 'ax-pow' 'ax-un'; $) + $} + + ${ + $d A f x $. $d M f x $. + $( Obsolete version of ~ rexdif1en as of 5-Jan-2025. (Contributed by + BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) + (New usage is discouraged.) $) + rexdif1enOLD $p |- ( ( M e. _om /\ A ~~ suc M ) -> E. x e. A ( A \ { x } ) ~~ M ) $= ( vf csuc cen wbr com wcel cv wf1o wex csn cdif wrex bren 19.42v ccnv cvv - wa cfv sucidg f1ocnvdm ancoms sylan vex dif1enlem mp3an1 wceq sneq breq1d - difeq2d rspcev syl2anc exlimiv sylbir sylan2b ) BCEZFGCHIZBURDJZKZDLZBAJZ - MZNZCFGZABOZBURDPUSVBTUSVATZDLVGUSVADQVHVGDVHCUTRUAZBIZBVIMZNZCFGZVGUSCUR - IZVAVJCHUBVAVNVJBURCUTUCUDUEUTSIUSVAVMDUFBUTCSUGUHVFVMAVIBVCVIUIZVEVLCFVO - VDVKBVCVIUJULUKUMUNUOUPUQ $. - $( $j usage 'rexdif1en' avoids 'ax-pow'; $) + wa cfv sucidg f1ocnvdm ancoms sylan dif1enlemOLD mp3an1 wceq sneq difeq2d + vex breq1d rspcev syl2anc exlimiv sylbir sylan2b ) BCEZFGCHIZBURDJZKZDLZB + AJZMZNZCFGZABOZBURDPUSVBTUSVATZDLVGUSVADQVHVGDVHCUTRUAZBIZBVIMZNZCFGZVGUS + CURIZVAVJCHUBVAVNVJBURCUTUCUDUEUTSIUSVAVMDUKBUTCSUFUGVFVMAVIBVCVIUHZVEVLC + FVOVDVKBVCVIUIUJULUMUNUOUPUQ $. $} ${ $d A f $. $d M f $. $d X f $. - $( If a set ` A ` is equinumerous to the successor of a natural number - ` M ` , then ` A ` with an element removed is equinumerous to ` M ` . - For a proof with fewer symbols using ~ ax-pow , see ~ dif1enALT . + $( If a set ` A ` is equinumerous to the successor of an ordinal ` M ` , + then ` A ` with an element removed is equinumerous to ` M ` . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, - 16-Aug-2015.) Avoid ~ ax-pow . (Revised by BTernaryTau, - 26-Aug-2024.) $) - dif1en $p |- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> + 16-Aug-2015.) Avoid ~ ax-pow . (Revised by BTernaryTau, 26-Aug-2024.) + Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.) $) + dif1en $p |- ( ( M e. On /\ A ~~ suc M /\ X e. A ) -> + ( A \ { X } ) ~~ M ) $= + ( vf cen wbr wcel con0 csn cdif w3a cvv wf1o wi wa ccnv cfv cpr cop jca + csuc simp1 encv simpld 3anim1i cv wex bren cres wceq wfun sucidg f1ocnvdm + cun 3adant2 f1ofvswap syld3an3 wb f1ocnvfv2 opeq2d preq1d f1oeq1d syl3an3 + uneq2d mpbid 3adant3r1 f1ofun opex prid1 elun2 ax-mp funopfv mpi f1ocnvfv + simpr2 syl2anc mpd sneqd difeq2d simpr1 3simpc anim2i 3anass sylibr simpl + 3syl simpr3 simpr vex prex unex dif1enlem mp3anl1 sylan2 eqbrtrrd exlimiv + resex ex sylbi sylc 3comr ) ABUAZEFZCAGZBHGZACIZJZBEFZXCXDXEKXCALGZXDXEKZ + XHXCXDXEUBXCXIXDXEXCXIXBLGAXBUCUDUEXCAXBDUFZMZDUGXJXHNZAXBDUHXLXMDXLXJXHX + LXJOZABXKACBXKPQZRJZUIZCBSZXOCXKQSZRZUNZPQZIZJZXGBEXNYCXFAXNYBCXNCYAQBUJZ + YBCUJZXNAXBYAMZYAUKZYEXLXDXEYGXIXEXLXDBXBGZYGBHULXLXDYIKAXBXQCXOXKQZSZXSR + ZUNZMZYGXLXDYIXOAGZYNXLYIYOXDAXBBXKUMUOAXBXKCXOUPUQXLYIYNYGURXDXLYIOZAXBY + MYAYPYLXTXQYPYKXRXSYPYJBCAXBBXKUSUTVAVDVBUOVEVCZVFZAXBYAVGYHXRYAGZYEXRXTG + YSXRXSCBVHVIXRXTXQVJVKCBYAVLVMWFXNYGXDYEYFNYRXLXIXDXEVOAXBCBYAVNVPVQVRVSX + NXIXLXDXEKZOZXIXEOZYTOYDBEFZXNXIYTXLXIXDXEVTXNXLXDXEOZOYTXJUUDXLXIXDXEWAW + BXLXDXEWCWDTUUAUUBYTUUAXIXEXIYTWEXIXLXDXEWGTXIYTWHTYTUUBYGUUCYQYALGXIXEYG + UUCXQXTXKXPDWIWQXRXSWJWKAYABLLWLWMWNWFWOWRWPWSWTXA $. + $( $j usage 'dif1en' avoids 'ax-pow'; $) + $} + + $( If a set ` A ` is equinumerous to the successor of a natural number + ` M ` , then ` A ` with an element removed is equinumerous to ` M ` . See + also ~ dif1ennnALT . (Contributed by BTernaryTau, 6-Jan-2025.) $) + dif1ennn $p |- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> + ( A \ { X } ) ~~ M ) $= + ( com wcel con0 csuc cen wbr csn cdif nnon dif1en syl3an1 ) BDEBFEABGHICAEA + CJKBHIBLABCMN $. + $( $j usage 'dif1ennn' avoids 'ax-pow'; $) + + ${ + $d A f $. $d M f $. $d X f $. + $( Obsolete version of ~ dif1en as of 6-Jan-2025. (Contributed by Jeff + Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid + ~ ax-pow . (Revised by BTernaryTau, 26-Aug-2024.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + dif1enOLD $p |- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M ) $= ( vf cen wbr wcel com csn cdif wf1o wex w3a 3anass ccnv cfv cpr cop cun wa csuc bren 19.41v exbii 3bitr4i cres wceq sucidg wfun 3adant2 f1ofvswap cv f1ocnvdm syld3an3 wb f1ocnvfv2 opeq2d preq1d uneq2d f1oeq1d mpbid opex f1ofun prid1 elun2 ax-mp funopfv mpi 3syl wi f1ocnvfv syl2anc mpd syl3an3 - simp2 sneqd difeq2d cvv vex resex prex dif1enlem mp3an2i eqbrtrrd exlimiv - unex simp3 sylbir syl3an1b 3comr ) ABUAZEFZCAGZBHGZACIZJZBEFZWLAWKDULZKZD - LZWMWNWQAWKDUBWTWMWNMZWSWMWNMZDLZWQWSWMWNTZTZDLWTXDTXCXAWSXDDUCXBXEDWSWMW - NNUDWTWMWNNUEXBWQDXBABWRACBWROPZQJZUFZCBRZXFCWRPRZQZSZOPZIZJZWPBEXBXNWOAX - BXMCWNWSWMBWKGZXMCUGZBHUHZWSWMXPMZCXLPBUGZXQXSAWKXLKZXLUIZXTXSAWKXHCXFWRP - ZRZXJQZSZKZYAWSWMXPXFAGZYGWSXPYHWMAWKBWRUMUJAWKWRCXFUKUNWSXPYGYAUOWMWSXPT - ZAWKYFXLYIYEXKXHYIYDXIXJYIYCBCAWKBWRUPUQURUSUTUJVAZAWKXLVCYBXIXLGZXTXIXKG - YKXIXJCBVBVDXIXKXHVEVFCBXLVGVHVIXSYAWMXTXQVJYJWSWMXPVOAWKCBXLVKVLVMVNVPVQ - XLVRGXBWNYAXOBEFXHXKWRXGDVSVTXIXJWAWFWSWMWNWGWNWSWMXPYAXRYJVNAXLBVRWBWCWD - WEWHWIWJ $. - $( $j usage 'dif1en' avoids 'ax-pow'; $) + simp2 sneqd difeq2d cvv vex resex prex unex dif1enlemOLD mp3an2i eqbrtrrd + simp3 exlimiv sylbir syl3an1b 3comr ) ABUAZEFZCAGZBHGZACIZJZBEFZWLAWKDULZ + KZDLZWMWNWQAWKDUBWTWMWNMZWSWMWNMZDLZWQWSWMWNTZTZDLWTXDTXCXAWSXDDUCXBXEDWS + WMWNNUDWTWMWNNUEXBWQDXBABWRACBWROPZQJZUFZCBRZXFCWRPRZQZSZOPZIZJZWPBEXBXNW + OAXBXMCWNWSWMBWKGZXMCUGZBHUHZWSWMXPMZCXLPBUGZXQXSAWKXLKZXLUIZXTXSAWKXHCXF + WRPZRZXJQZSZKZYAWSWMXPXFAGZYGWSXPYHWMAWKBWRUMUJAWKWRCXFUKUNWSXPYGYAUOWMWS + XPTZAWKYFXLYIYEXKXHYIYDXIXJYIYCBCAWKBWRUPUQURUSUTUJVAZAWKXLVCYBXIXLGZXTXI + XKGYKXIXJCBVBVDXIXKXHVEVFCBXLVGVHVIXSYAWMXTXQVJYJWSWMXPVOAWKCBXLVKVLVMVNV + PVQXLVRGXBWNYAXOBEFXHXKWRXGDVSVTXIXJWAWBWSWMWNWFWNWSWMXPYAXRYJVNAXLBVRWCW + DWEWGWHWIWJ $. $} ${ @@ -92466,16 +92537,16 @@ excluded middle (LEM), and in ILE the LEM is not accepted as necessarily findcard $p |- ( A e. Fin -> ta ) $= ( vw wcel cen wbr com vv cfn cv wrex isfi wi wal csuc breq2 imbi1d albidv c0 wceq en0 mpbiri sylbi ax-gen w3a wa peano2 rspcev sylan sylibr 3adant2 - wral csn cdif dif1en 3expa vex difexi breq1 imbi12d syl5com ralrimdva imp - spcv an32s 3impa sylc 3exp alrimdv cbvalvw syl6ibr finds1 19.21bi vtoclga - rexlimiv ) AEFIUBMFUCZUBQWIPUCZRSZPTUDAPWIUEWKAPTWJTQWKAUFZFWLFUGWIULRSZA - UFZFUGWIUAUCZRSZAUFZFUGZWIWOUHZRSZAUFZFUGZPUAWJULUMZWLWNFXCWKWMAWJULWIRUI - UJUKWJWOUMZWLWQFXDWKWPAWJWOWIRUIUJUKWJWSUMZWLXAFXEWKWTAWJWSWIRUIUJUKWNFWM - WIULUMZAWIUNXFABNJUOUPUQWOTQZWRGUCZWSRSZDUFZGUGXBXGWRXJGXGWRXIDXGWRXIURXH - UBQZCHXHVEZDXGXIXKWRXGXIUSZXHWJRSZPTUDZXKXGWSTQXIXOWOUTXNXIPWSTWJWSXHRUIV - AVBPXHUEVCVDXGWRXIXLXGXIWRXLXMWRXLXMWRCHXHXMHUCZXHQZUSXHXPVFZVGZWORSZWRCX - GXIXQXTXHWOXPVHVIWQXTCUFFXSXHXRGVJVKWIXSUMWPXTACWIXSWORVLKVMVQVNVOVPVRVSO - VTWAWBXAXJFGWIXHUMWTXIADWIXHWSRVLLVMWCWDWEWFWHUPWG $. + wral csn cdif dif1ennn 3expa vex breq1 imbi12d spcv syl5com ralrimdva imp + difexi an32s sylc alrimdv cbvalvw syl6ibr finds1 19.21bi rexlimiv vtoclga + 3impa 3exp ) AEFIUBMFUCZUBQWIPUCZRSZPTUDAPWIUEWKAPTWJTQWKAUFZFWLFUGWIULRS + ZAUFZFUGWIUAUCZRSZAUFZFUGZWIWOUHZRSZAUFZFUGZPUAWJULUMZWLWNFXCWKWMAWJULWIR + UIUJUKWJWOUMZWLWQFXDWKWPAWJWOWIRUIUJUKWJWSUMZWLXAFXEWKWTAWJWSWIRUIUJUKWNF + WMWIULUMZAWIUNXFABNJUOUPUQWOTQZWRGUCZWSRSZDUFZGUGXBXGWRXJGXGWRXIDXGWRXIUR + XHUBQZCHXHVEZDXGXIXKWRXGXIUSZXHWJRSZPTUDZXKXGWSTQXIXOWOUTXNXIPWSTWJWSXHRU + IVAVBPXHUEVCVDXGWRXIXLXGXIWRXLXMWRXLXMWRCHXHXMHUCZXHQZUSXHXPVFZVGZWORSZWR + CXGXIXQXTXHWOXPVHVIWQXTCUFFXSXHXRGVJVQWIXSUMWPXTACWIXSWORVKKVLVMVNVOVPVRW + GOVSWHVTXAXJFGWIXHUMWTXIADWIXHWSRVKLVLWAWBWCWDWEUPWF $. $( $j usage 'findcard' avoids 'ax-pow'; $) $} @@ -92494,24 +92565,25 @@ excluded middle (LEM), and in ILE the LEM is not accepted as necessarily (Contributed by Jeff Madsen, 8-Jul-2010.) Avoid ~ ax-pow . (Revised by BTernaryTau, 26-Aug-2024.) $) findcard2 $p |- ( A e. Fin -> ta ) $= - ( vw vv cen wbr wi cfn cv wcel com wrex isfi wal csuc breq2 imbi1d albidv - c0 wceq weq en0 mpbiri sylbi ax-gen wsbc csn cdif rexdif1en wss cun snssi - wa uncom undif biimpi eqtrid vex difexi breq1 anbi2d uneq1 sbceq1d imbi2d - imbi12d spvv rspe sylibr pm2.27 adantl sylsyld syl5 snex unex sbcie vtocl - syl6ibr dfsbcq syl5ib 3syl com12 rexlimdv adantr mpd ex com23 alrimdv nfv - expd nfsbc1v nfim sbceq1a cbvalv1 finds1 19.21bi rexlimiv vtoclga ) AEFIU - AMFUBZUAUCXKPUBZRSZPUDUEAPXKUFXMAPUDXLUDUCXMATZFXNFUGXKULRSZATZFUGXKQUBZR - SZATZFUGZXKXQUHZRSZATZFUGZPQXLULUMZXNXPFYEXMXOAXLULXKRUIUJUKPQUNZXNXSFYFX - MXRAXLXQXKRUIUJUKXLYAUMZXNYCFYGXMYBAXLYAXKRUIUJUKXPFXOXKULUMZAXKUOYHABNJU - PUQURXQUDUCZXTXLYARSZAFXLUSZTZPUGYDYIXTYLPYIYJXTYKYIYJXTYKTZYIYJVFXLHUBZU - TZVAZXQRSZHXLUEZYMHXLXQVBYIYRYMTYJYIYQYMHXLYNXLUCZYIYQYMTYSYIYQYMYSYOXLVC - ZYPYOVDZXLUMZYIYQVFZYMTYNXLVEYTUUAYOYPVDZXLYPYOVGYTUUDXLUMYOXLVHVIVJUUCXT - AFUUAUSZTZUUBYMYIGUBZXQRSZVFZXTAFUUGYOVDZUSZTZTUUCUUFTGYPXLYOPVKVLUUGYPUM - ZUUIUUCUULUUFUUMUUHYQYIUUGYPXQRVMVNUUMUUKUUEXTUUMAFUUJUUAUUGYPYOVOVPVQVRU - UIXTDUUKXTUUHCTZUUIDXSUUNFGFGUNXRUUHACXKUUGXQRVMKVRVSUUIUUGUAUCZUUNCDUUIU - UHQUDUEUUOUUHQUDVTQUUGUFWAUUHUUNCTYIUUHCWBWCOWDWEADFUUJUUGYOGVKYNWFWGLWHW - JWIUUBUUEYKXTAFUUAXLWKVQWLWMXBWNWOWPWQWRWSWTYCYLFPYCPXAYJYKFYJFXAAFXLXCXD - FPUNYBYJAYKXKXLYARVMAFXLXEVRXFWJXGXHXIUQXJ $. + ( vw cen wbr wi wceq vv cfn cv wcel com wrex isfi wal breq2 imbi1d albidv + c0 csuc en0 mpbiri sylbi ax-gen wsbc wa csn cdif con0 rexdif1en sylan wss + cun snssi uncom undif biimpi eqtrid vex difexi breq1 anbi2d uneq1 sbceq1d + nnon imbi2d imbi12d spvv rspe sylibr pm2.27 adantl sylsyld syl5 snex unex + sbcie syl6ibr vtocl dfsbcq syl5ib 3syl com12 rexlimdv adantr mpd ex com23 + expd alrimdv nfsbc1v nfim sbceq1a cbvalv1 finds1 19.21bi rexlimiv vtoclga + nfv ) AEFIUBMFUCZUBUDXMPUCZQRZPUEUFAPXMUGXOAPUEXNUEUDXOASZFXPFUHXMULQRZAS + ZFUHXMUAUCZQRZASZFUHZXMXSUMZQRZASZFUHZPUAXNULTZXPXRFYGXOXQAXNULXMQUIUJUKX + NXSTZXPYAFYHXOXTAXNXSXMQUIUJUKXNYCTZXPYEFYIXOYDAXNYCXMQUIUJUKXRFXQXMULTZA + XMUNYJABNJUOUPUQXSUEUDZYBXNYCQRZAFXNURZSZPUHYFYKYBYNPYKYLYBYMYKYLYBYMSZYK + YLUSXNHUCZUTZVAZXSQRZHXNUFZYOYKXSVBUDYLYTXSVRHXNXSVCVDYKYTYOSYLYKYSYOHXNY + PXNUDZYKYSYOSUUAYKYSYOUUAYQXNVEZYRYQVFZXNTZYKYSUSZYOSYPXNVGUUBUUCYQYRVFZX + NYRYQVHUUBUUFXNTYQXNVIVJVKUUEYBAFUUCURZSZUUDYOYKGUCZXSQRZUSZYBAFUUIYQVFZU + RZSZSUUEUUHSGYRXNYQPVLVMUUIYRTZUUKUUEUUNUUHUUOUUJYSYKUUIYRXSQVNVOUUOUUMUU + GYBUUOAFUULUUCUUIYRYQVPVQVSVTUUKYBDUUMYBUUJCSZUUKDYAUUPFGXMUUITXTUUJACXMU + UIXSQVNKVTWAUUKUUIUBUDZUUPCDUUKUUJUAUEUFUUQUUJUAUEWBUAUUIUGWCUUJUUPCSYKUU + JCWDWEOWFWGADFUULUUIYQGVLYPWHWILWJWKWLUUDUUGYMYBAFUUCXNWMVSWNWOXBWPWQWRWS + WTXAXCYEYNFPYEPXLYLYMFYLFXLAFXNXDXEXMXNTYDYLAYMXMXNYCQVNAFXNXFVTXGWKXHXIX + JUPXK $. $( $j usage 'findcard2' avoids 'ax-pow'; $) $} @@ -93143,10 +93215,10 @@ proved without using the Axiom of Power Sets (unlike ~ domsdomtr ). successor minus any element of the successor. (Contributed by NM, 26-May-1998.) Avoid ~ ax-pow . (Revised by BTernaryTau, 23-Sep-2024.) $) phplem1 $p |- ( ( A e. _om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) ) $= - ( com wcel csuc wa csn cen wbr simpl peano2 enrefnn syl adantr simpr dif1en - cdif syl3anc cfn wb nnfi ensymfib 3syl mpbird ) ACDZBAEZDZFZAUFBGQZHIZUIAHI - ZUHUEUFUFHIZUGUKUEUGJZUEULUGUEUFCDULAKUFLMNUEUGOUFABPRUHUEASDUJUKTUMAUAAUIU - BUCUD $. + ( com wcel csuc wa csn cdif cen wbr simpl peano2 enrefnn syl simpr dif1ennn + adantr syl3anc cfn wb nnfi ensymfib 3syl mpbird ) ACDZBAEZDZFZAUFBGHZIJZUIA + IJZUHUEUFUFIJZUGUKUEUGKZUEULUGUEUFCDULALUFMNQUEUGOUFABPRUHUEASDUJUKTUMAUAAU + IUBUCUD $. $( $j usage 'phplem1' avoids 'ax-pow'; $) ${ @@ -94182,11 +94254,10 @@ singletons being the empty set ( ` A e/ _V ` ). (Contributed by AV, ${ $d A x $. $d X x $. $d M x $. - $( Alternate proof of ~ dif1en with fewer symbols using ~ ax-pow . - (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, - 16-Aug-2015.) (Proof modification is discouraged.) - (New usage is discouraged.) $) - dif1enALT $p |- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> + $( Alternate proof of ~ dif1ennn using ~ ax-pow . (Contributed by Jeff + Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) + (Proof modification is discouraged.) (New usage is discouraged.) $) + dif1ennnALT $p |- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M ) $= ( vx com wcel csuc cen wbr csn wrex wa cfn peano2 breq2 isfi wceq wi cin c0 w3a cdif cv rspcev sylibr sylan diffi sylib syl 3adant3 cun en2sn elvd @@ -94224,11 +94295,11 @@ singletons being the empty set ( ` A e/ _V ` ). (Contributed by AV, Carneiro, 5-Jan-2016.) $) enp1i $p |- ( A ~~ N -> E. x ps ) $= ( cen wbr cv wcel wex c0 wceq wn csuc sylib wne nsuceq0 breq1 en0 eqtr3id - ensym syl6bi necon3ad mpi con2i neq0 wi breq2i csn cdif com dif1en mp3an1 - wa syl ex sylbi sylcom eximdv mpd ) DFKLZCMZDNZCOZBCOVFDPQZRVIVJVFVJESZPU - AVFREUBVJVFVKPVJVFPFKLZVKPQDPFKUCVLVKFPHVLFPKLFPQPFUFFUDTUEUGUHUIUJCDUKTV - FVHBCVFVHABVFDVKKLZVHAULFVKDKHUMVMVHAVMVHUSDVGUNUOEKLZAEUPNVMVHVNGDEVGUQU - RIUTVAVBJVCVDVE $. + ensym syl6bi necon3ad mpi con2i neq0 wi breq2i wa csn com dif1ennn mp3an1 + cdif syl ex sylbi sylcom eximdv mpd ) DFKLZCMZDNZCOZBCOVFDPQZRVIVJVFVJESZ + PUAVFREUBVJVFVKPVJVFPFKLZVKPQDPFKUCVLVKFPHVLFPKLFPQPFUFFUDTUEUGUHUIUJCDUK + TVFVHBCVFVHABVFDVKKLZVHAULFVKDKHUMVMVHAVMVHUNDVGUOUSEKLZAEUPNVMVHVNGDEVGU + QURIUTVAVBJVCVDVE $. $} ${ @@ -94278,26 +94349,26 @@ singletons being the empty set ( ` A e/ _V ` ). (Contributed by AV, ( vw cen wbr wi c0 vv cfn wcel com wrex isfi wal csuc breq2 imbi1d albidv cv wceq weq en0 mpbiri sylbi ax-gen wne wa nsuceq0 breq1 anbi2d wb peano1 wsbc peano2 nneneq sylancr biimpa eqcomd syl6bi com12 necon3d mpi wel wex - ex n0 csn cdif dif1en 3expia wss cun snssi uncom biimpi eqtrid vex difexi - undif uneq1 sbceq1d imbi2d imbi12d spvv rspe sylibr pm2.27 adantl sylsyld - syl5 snex unex sbcie syl6ibr vtocl dfsbcq syl5ib 3syl expd adantr exlimdv - mpdd biimtrid com23 alrimdv nfsbc1v nfim sbceq1a cbvalv1 19.21bi rexlimiv - nfv finds1 vtoclga ) AEFIUBMFULZUBUCYHPULZQRZPUDUEAPYHUFYJAPUDYIUDUCYJASZ - FYKFUGYHTQRZASZFUGYHUAULZQRZASZFUGZYHYNUHZQRZASZFUGZPUAYITUMZYKYMFUUBYJYL - AYITYHQUIUJUKPUAUNZYKYPFUUCYJYOAYIYNYHQUIUJUKYIYRUMZYKYTFUUDYJYSAYIYRYHQU - IUJUKYMFYLYHTUMZAYHUOUUEABNJUPUQURYNUDUCZYQYIYRQRZAFYIVFZSZPUGUUAUUFYQUUI - PUUFUUGYQUUHUUFUUGYITUSZYQUUHSZUUFUUGUUJUUFUUGUTZYRTUSUUJYNVAUULYITYRTUUB - UULYRTUMZUUBUULUUFTYRQRZUTZUUMUUBUUGUUNUUFYITYRQVBVCUUOTYRUUFUUNTYRUMZUUF - TUDUCYRUDUCUUNUUPVDVEYNVGTYRVHVIVJVKVLVMVNVOVRUUFUUGUUJUUKSUUJHPVPZHVQUUL - UUKHYIVSUULUUQUUKHUULUUQYIHULZVTZWAZYNQRZUUKUUFUUGUUQUVAYIYNUURWBWCUUFUUQ - UVAUUKSZSUUGUUQUUFUVBUUQUUFUVAUUKUUQUUSYIWDZUUTUUSWEZYIUMZUUFUVAUTZUUKSUU - RYIWFUVCUVDUUSUUTWEZYIUUTUUSWGUVCUVGYIUMUUSYIWLWHWIUVFYQAFUVDVFZSZUVEUUKU - UFGULZYNQRZUTZYQAFUVJUUSWEZVFZSZSUVFUVISGUUTYIUUSPWJWKUVJUUTUMZUVLUVFUVOU - VIUVPUVKUVAUUFUVJUUTYNQVBVCUVPUVNUVHYQUVPAFUVMUVDUVJUUTUUSWMWNWOWPUVLYQDU - VNYQUVKCSZUVLDYPUVQFGFGUNYOUVKACYHUVJYNQVBKWPWQUVLUVJUBUCZUVQCDUVLUVKUAUD - UEUVRUVKUAUDWRUAUVJUFWSUVKUVQCSUUFUVKCWTXAOXBXCADFUVMUVJUUSGWJUURXDXELXFX - GXHUVEUVHUUHYQAFUVDYIXIWOXJXKXLVMXMXOXNXPVRXOXQXRYTUUIFPYTPYEUUGUUHFUUGFY - EAFYIXSXTFPUNYSUUGAUUHYHYIYRQVBAFYIYAWPYBXGYFYCYDUQYG $. + ex n0 csn dif1enOLD 3expia wss cun snssi uncom undif biimpi eqtrid difexi + cdif vex uneq1 sbceq1d imbi2d imbi12d spvv rspe sylibr pm2.27 adantl syl5 + sylsyld snex unex sbcie syl6ibr vtocl dfsbcq syl5ib 3syl expd adantr mpdd + exlimdv biimtrid com23 alrimdv nfv nfsbc1v sbceq1a cbvalv1 finds1 19.21bi + nfim rexlimiv vtoclga ) AEFIUBMFULZUBUCYHPULZQRZPUDUEAPYHUFYJAPUDYIUDUCYJ + ASZFYKFUGYHTQRZASZFUGYHUAULZQRZASZFUGZYHYNUHZQRZASZFUGZPUAYITUMZYKYMFUUBY + JYLAYITYHQUIUJUKPUAUNZYKYPFUUCYJYOAYIYNYHQUIUJUKYIYRUMZYKYTFUUDYJYSAYIYRY + HQUIUJUKYMFYLYHTUMZAYHUOUUEABNJUPUQURYNUDUCZYQYIYRQRZAFYIVFZSZPUGUUAUUFYQ + UUIPUUFUUGYQUUHUUFUUGYITUSZYQUUHSZUUFUUGUUJUUFUUGUTZYRTUSUUJYNVAUULYITYRT + UUBUULYRTUMZUUBUULUUFTYRQRZUTZUUMUUBUUGUUNUUFYITYRQVBVCUUOTYRUUFUUNTYRUMZ + UUFTUDUCYRUDUCUUNUUPVDVEYNVGTYRVHVIVJVKVLVMVNVOVRUUFUUGUUJUUKSUUJHPVPZHVQ + UULUUKHYIVSUULUUQUUKHUULUUQYIHULZVTZWKZYNQRZUUKUUFUUGUUQUVAYIYNUURWAWBUUF + UUQUVAUUKSZSUUGUUQUUFUVBUUQUUFUVAUUKUUQUUSYIWCZUUTUUSWDZYIUMZUUFUVAUTZUUK + SUURYIWEUVCUVDUUSUUTWDZYIUUTUUSWFUVCUVGYIUMUUSYIWGWHWIUVFYQAFUVDVFZSZUVEU + UKUUFGULZYNQRZUTZYQAFUVJUUSWDZVFZSZSUVFUVISGUUTYIUUSPWLWJUVJUUTUMZUVLUVFU + VOUVIUVPUVKUVAUUFUVJUUTYNQVBVCUVPUVNUVHYQUVPAFUVMUVDUVJUUTUUSWMWNWOWPUVLY + QDUVNYQUVKCSZUVLDYPUVQFGFGUNYOUVKACYHUVJYNQVBKWPWQUVLUVJUBUCZUVQCDUVLUVKU + AUDUEUVRUVKUAUDWRUAUVJUFWSUVKUVQCSUUFUVKCWTXAOXCXBADFUVMUVJUUSGWLUURXDXEL + XFXGXHUVEUVHUUHYQAFUVDYIXIWOXJXKXLVMXMXNXOXPVRXNXQXRYTUUIFPYTPXSUUGUUHFUU + GFXSAFYIXTYEFPUNYSUUGAUUHYHYIYRQVBAFYIYAWPYBXGYCYDYFUQYG $. $} ${ @@ -105281,12 +105352,12 @@ several of their earlier lemmas available (which would otherwise be and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.) $) en2eleq $p |- ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } ) $= ( wcel c2o cen wbr wa csn cdif cuni cpr cfn wss wceq com adantl wne syl3anc - 2onn c1o nnfi ax-mp enfi mpbiri simpl csuc 1onn simpr df-2o breqtrdi dif1en - mp3an2i en1uniel syl eldifsn sylib simpld prssd simprd necomd enpr2 syl2anc - ensym entr fisseneq eqcomd ) BACZADEFZGZBABHIZJZKZAVIALCZVLAMVLAEFZVLANVHVM - VGVHVMDLCZDOCVOSDUAUBADUCUDPVIBVKAVGVHUEZVIVKACZVKBQZVIVKVJCZVQVRGVIVJTEFZV - STOCVIATUFZEFVGVTUGVIADWAEVGVHUHUIUJVPATBUKULVJUMUNVKABUOUPZUQZURVIVLDEFZDA - EFZVNVIVGVQBVKQWDVPWCVIVKBVIVQVRWBUSUTBVKAAVARVHWEVGADVCPVLDAVDVBVLAVERVF + 2onn c1o nnfi ax-mp enfi mpbiri simpl simpr df-2o breqtrdi dif1ennn mp3an2i + csuc 1onn en1uniel syl eldifsn sylib simpld prssd simprd necomd enpr2 ensym + entr syl2anc fisseneq eqcomd ) BACZADEFZGZBABHIZJZKZAVIALCZVLAMVLAEFZVLANVH + VMVGVHVMDLCZDOCVOSDUAUBADUCUDPVIBVKAVGVHUEZVIVKACZVKBQZVIVKVJCZVQVRGVIVJTEF + ZVSTOCVIATUKZEFVGVTULVIADWAEVGVHUFUGUHVPATBUIUJVJUMUNVKABUOUPZUQZURVIVLDEFZ + DAEFZVNVIVGVQBVKQWDVPWCVIVKBVIVQVRWBUSUTBVKAAVARVHWEVGADVBPVLDAVCVDVLAVERVF $. $( Taking the other element twice in a pair gets back to the original @@ -105294,12 +105365,12 @@ several of their earlier lemmas available (which would otherwise be en2other2 $p |- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X ) $= ( wcel c2o cen wbr csn cdif cuni cpr en2eleq prcom eqtrdi difeq1d difprsnss - wa eqsstrdi wne simpl c1o com csuc 1onn simpr df-2o breqtrdi dif1en mp3an2i - en1uniel eldifsni 3syl necomd eldifsn snssd eqssd unieqd wceq unisng adantr - sylanbrc eqtrd ) BACZADEFZPZAABGZHZIZGZHZIVEIZBVDVIVEVDVIVEVDVIVGBJZVHHVEVD - AVKVHVDABVGJVKABKBVGLMNVGBOQVDBVIVDVBBVGRBVICVBVCSZVDVGBVDVFTEFZVGVFCVGBRTU - ACVDATUBZEFVBVMUCVDADVNEVBVCUDUEUFVLATBUGUHVFUIVGABUJUKULBAVGUMUTUNUOUPVBVJ - BUQVCBAURUSVA $. + wa eqsstrdi wne simpl c1o com csuc simpr breqtrdi dif1ennn mp3an2i en1uniel + 1onn df-2o eldifsni 3syl necomd eldifsn sylanbrc snssd unieqd unisng adantr + eqssd wceq eqtrd ) BACZADEFZPZAABGZHZIZGZHZIVEIZBVDVIVEVDVIVEVDVIVGBJZVHHVE + VDAVKVHVDABVGJVKABKBVGLMNVGBOQVDBVIVDVBBVGRBVICVBVCSZVDVGBVDVFTEFZVGVFCVGBR + TUACVDATUBZEFVBVMUHVDADVNEVBVCUCUIUDVLATBUEUFVFUGVGABUJUKULBAVGUMUNUOUSUPVB + VJBUTVCBAUQURVA $. ${ $d A m $. $d X m $. @@ -208140,38 +208211,38 @@ f C_ ( N ` ( g u. h ) ) /\ ( f u. h ) e. I ) -> csn wral wss animorrl mreexexlem3d wne n0 biimpi adantl wn mreexexlem2d wex simpr w3a 3anass cvv ad2antrr elfvexd simpr2 difsnb ssdifssd ssdifd sylib difun1 sseqtrrdi simpr1 uncom uneq2i unass difsnid uneq1d eqtr3id - eqsstrrd eqtrid syl fveq2d sseqtrrd simpr3 csuc wo com wi simplr dif1en - 3anan12 sylbir expcom syl2anc orim12d mpd mreexexlemd ad3antrrr difss2d - wal ssexd simprl simplr1 snssd unssd sselpwd ad3antlr cin simprrl en2sn - elpwid el2v a1i disjdifr ssdifin0 unen syl22anc eqbrtrrd eqtr2i simprrr - eqeltrrid rexlimddv breq2 uneq1 eleq1d anbi12d rspcev syl12anc sylan2br - adantlr exlimddv pm2.61dane ) AIHUKZULUMZUUKKUNZLUOZUPZHJUQZURZIUSAIUSU - TZUPBCDHIJKLNOPADOVAVBUOZUURQVCRSABUKZPUKZCUKVEUNNVBUOCUVAUUTVEUNNVBUVA - NVBVDVFBOVFPOUQVFZUURTVCAIOKVDZVGZUURUAVCAJUVCVGZUURUBVCAIJKUNZNVBZVGZU - URUCVCAIKUNLUOZUURUDVCAUURJUSUTVHVIAIUSVJZUPUHUKZIUOZUUQUHUVJUVLUHVPZAU - VJUVMUHIVKVLVMAUVLUUQUVJAUVLUPZUIUKZIUVKVEZVDZUOVNZUVQKUVOVEZUNZUNLUOZU - PZUUQUIJUVNBCDUIIJKLNOUVKPAUUSUVLQVCRSAUVBUVLTVCAUVDUVLUAVCAUVEUVLUBVCA - UVHUVLUCVCAUVIUVLUDVCAUVLVQVOUVOJUOZUWBUPUVNUWCUVRUWAVRZUUQUWCUVRUWAVSU - VNUWDUPZUVQUJUKZULUMZUWFUVTUNZLUOZUPZUUQUJJUVSVDZUQZUWEFEGHUJUVQUWKUVTL - VTMNOUWEDVAOAUUSUVLUWDQWAWBZUWEUVQUVCUVSVDZOUVTVDZUWEUVQUVQUVSVDZUWNUWE - UVRUWPUVQUTUVNUWCUVRUWAWCUVOUVQWDWGUWEUVQUVCUVSUWEIUVCUVPAUVDUVLUWDUAWA - WEWFWQOKUVSWHZWIUWEUWKUWNUWOUWEJUVCUVSAUVEUVLUWDUBWAWFUWQWIUWEIUWKUVTUN - ZNVBZUVPUWEIUVGUWSAUVHUVLUWDUCWAUWEUWRUVFNUWEUWCUWRUVFUTUVNUWCUVRUWAWJZ - UWCUWRUWKUVSKUNZUNZUVFUVTUXAUWKKUVSWKWLUWCUXBUWKUVSUNZKUNUVFUWKUVSKWMUW - CUXCJKJUVOWNWOWPWRWSWTXAWEUVNUWCUVRUWAXBUWEIMXCZULUMZJUXDULUMZXDZUVQMUL - UMZUWKMULUMZXDAUXGUVLUWDUGWAUWEUXEUXHUXFUXIUWEMXEUOZUVLUXEUXHXFAUXJUVLU - WDUEWAZAUVLUWDXGUXEUXJUVLUPZUXHUXEUXLUPUXJUXEUVLVRUXHUXJUXEUVLXIIMUVKXH - XJXKXLUWEUXJUWCUXFUXIXFUXKUWTUXFUXJUWCUPZUXIUXFUXMUPUXJUXFUWCVRUXIUXJUX - FUWCXIJMUVOXHXJXKXLXMXNAEUKZMULUMFUKZMULUMXDUXNUXOGUKZUNNVBVGUXNUXPUNLU - OVRUXNUUKULUMUUKUXPUNLUOUPHUXOUQURXFFOUXPVDUQZVFEUXQVFGXRUVLUWDUFWAXOUW - EUWFUWLUOZUWJUPZUPZUWFUVSUNZUUPUOIUYAULUMZUYAKUNZLUOZUUQUXTUYAJVTUXTJOV - TUWEOVTUOUXSUWMVCUXTJOKAUVEUVLUWDUXSUBXPXQXSUXTUWFUVSJUXTUWFJUVSUXTUWFU - WKUWEUXRUWJXTYIZXQUXTUVOJUWCUVRUWAUVNUXSYAYBYCYDUXTUVQUVPUNZIUYAULUVLUY - FIUTAUWDUXSIUVKWNYEUXTUWGUVPUVSULUMZUVQUVPYFUSUTZUWFUVSYFUSUTZUYFUYAULU - MUWEUXRUWGUWIYGUYGUXTUYGUHUIUVKUVOVTVTYHYJYKUYHUXTUVPIYLYKUXTUWFUWKVGUY - IUYEUWFJUVSYMWSUVQUWFUVPUVSYNYOYPUXTUYCUWHLUYCUWFUXAUNUWHUWFUVSKWMUXAUV - TUWFUVSKWKWLYQUWEUXRUWGUWIYRYSUUOUYBUYDUPHUYAUUPUUKUYAUTZUULUYBUUNUYDUU - KUYAIULUUAUYJUUMUYCLUUKUYAKUUBUUCUUDUUEUUFYTUUGYTUUHUUIUUJ $. + eqsstrrd eqtrid syl fveq2d sseqtrrd simpr3 csuc wo com 3anan12 dif1ennn + wi simplr sylbir expcom syl2anc orim12d mpd mreexexlemd ad3antrrr ssexd + wal difss2d simprl elpwid simplr1 snssd unssd sselpwd cin simprrl en2sn + ad3antlr el2v disjdifr ssdifin0 unen syl22anc eqbrtrrd eqtr2i eqeltrrid + a1i simprrr rexlimddv eleq1d anbi12d syl12anc sylan2br adantlr exlimddv + breq2 uneq1 rspcev pm2.61dane ) AIHUKZULUMZUUKKUNZLUOZUPZHJUQZURZIUSAIU + SUTZUPBCDHIJKLNOPADOVAVBUOZUURQVCRSABUKZPUKZCUKVEUNNVBUOCUVAUUTVEUNNVBU + VANVBVDVFBOVFPOUQVFZUURTVCAIOKVDZVGZUURUAVCAJUVCVGZUURUBVCAIJKUNZNVBZVG + ZUURUCVCAIKUNLUOZUURUDVCAUURJUSUTVHVIAIUSVJZUPUHUKZIUOZUUQUHUVJUVLUHVPZ + AUVJUVMUHIVKVLVMAUVLUUQUVJAUVLUPZUIUKZIUVKVEZVDZUOVNZUVQKUVOVEZUNZUNLUO + ZUPZUUQUIJUVNBCDUIIJKLNOUVKPAUUSUVLQVCRSAUVBUVLTVCAUVDUVLUAVCAUVEUVLUBV + CAUVHUVLUCVCAUVIUVLUDVCAUVLVQVOUVOJUOZUWBUPUVNUWCUVRUWAVRZUUQUWCUVRUWAV + SUVNUWDUPZUVQUJUKZULUMZUWFUVTUNZLUOZUPZUUQUJJUVSVDZUQZUWEFEGHUJUVQUWKUV + TLVTMNOUWEDVAOAUUSUVLUWDQWAWBZUWEUVQUVCUVSVDZOUVTVDZUWEUVQUVQUVSVDZUWNU + WEUVRUWPUVQUTUVNUWCUVRUWAWCUVOUVQWDWGUWEUVQUVCUVSUWEIUVCUVPAUVDUVLUWDUA + WAWEWFWQOKUVSWHZWIUWEUWKUWNUWOUWEJUVCUVSAUVEUVLUWDUBWAWFUWQWIUWEIUWKUVT + UNZNVBZUVPUWEIUVGUWSAUVHUVLUWDUCWAUWEUWRUVFNUWEUWCUWRUVFUTUVNUWCUVRUWAW + JZUWCUWRUWKUVSKUNZUNZUVFUVTUXAUWKKUVSWKWLUWCUXBUWKUVSUNZKUNUVFUWKUVSKWM + UWCUXCJKJUVOWNWOWPWRWSWTXAWEUVNUWCUVRUWAXBUWEIMXCZULUMZJUXDULUMZXDZUVQM + ULUMZUWKMULUMZXDAUXGUVLUWDUGWAUWEUXEUXHUXFUXIUWEMXEUOZUVLUXEUXHXHAUXJUV + LUWDUEWAZAUVLUWDXIUXEUXJUVLUPZUXHUXEUXLUPUXJUXEUVLVRUXHUXJUXEUVLXFIMUVK + XGXJXKXLUWEUXJUWCUXFUXIXHUXKUWTUXFUXJUWCUPZUXIUXFUXMUPUXJUXFUWCVRUXIUXJ + UXFUWCXFJMUVOXGXJXKXLXMXNAEUKZMULUMFUKZMULUMXDUXNUXOGUKZUNNVBVGUXNUXPUN + LUOVRUXNUUKULUMUUKUXPUNLUOUPHUXOUQURXHFOUXPVDUQZVFEUXQVFGXRUVLUWDUFWAXO + UWEUWFUWLUOZUWJUPZUPZUWFUVSUNZUUPUOIUYAULUMZUYAKUNZLUOZUUQUXTUYAJVTUXTJ + OVTUWEOVTUOUXSUWMVCUXTJOKAUVEUVLUWDUXSUBXPXSXQUXTUWFUVSJUXTUWFJUVSUXTUW + FUWKUWEUXRUWJXTYAZXSUXTUVOJUWCUVRUWAUVNUXSYBYCYDYEUXTUVQUVPUNZIUYAULUVL + UYFIUTAUWDUXSIUVKWNYIUXTUWGUVPUVSULUMZUVQUVPYFUSUTZUWFUVSYFUSUTZUYFUYAU + LUMUWEUXRUWGUWIYGUYGUXTUYGUHUIUVKUVOVTVTYHYJYRUYHUXTUVPIYKYRUXTUWFUWKVG + UYIUYEUWFJUVSYLWSUVQUWFUVPUVSYMYNYOUXTUYCUWHLUYCUWFUXAUNUWHUWFUVSKWMUXA + UVTUWFUVSKWKWLYPUWEUXRUWGUWIYSYQUUOUYBUYDUPHUYAUUPUUKUYAUTZUULUYBUUNUYD + UUKUYAIULUUGUYJUUMUYCLUUKUYAKUUHUUAUUBUUIUUCYTUUDYTUUEUUFUUJ $. $} $d q f F g h $. $d f F g h l $. $d q f g G h $. $d f g G h l $. @@ -236327,18 +236398,18 @@ operation is a permutation group (group consisting of permutations), see F = G ) $= ( vx vy wf1o wa cid cdif cdm c2o cen wbr wceq wfn f1ofn wcel c1o wb cvv ad2antrr ad2antlr cv cfv csn wmo csuc 1onn simplrr simplrl df-2o breqtrdi - com eqbrtrd simpr dif1en mp3an2i weu euen1b eumo sylbi wi f1omvdmvd eleq2 - syl ex ad2antll difeq1 eleq2d 3imtr4d imp ad4ant24 fvex pm3.2i moi mp3an1 - eleq1 syl12anc adantlr wn fnelnfp sylan bitrd necon2bbid eqtr4d pm2.61dan - wne biimpar eqfnfvd ) AABFZAACFZGZBHIJZKLMZCHIJZWMNZGZGZDABCWJBAOZWKWQAAB - PUAZWKCAOZWJWQAACPUBZWRDUCZAQZGZXCWOQZXCBUDZXCCUDZNZWRXFXIXDWRXFGZEUCZWOX - CUEZIZQZEUFZXGXMQZXHXMQZXIXJXMRLMZXORUMQXJWORUGZLMXFXRUHXJWOWMXSLWLWNWPXF - UIXJWMKXSLWLWNWPXFUJUKULUNWRXFUOWORXCUPUQXRXNEURXOEXMUSXNEUTVAVEWRXFXPWRX - CWMQZXGWMXLIZQZXFXPWJXTYBVBWKWQWJXTYBABXCVCVFUAWPXFXTSWLWNWOWMXCVDVGWPXPY - BSWLWNWPXMYAXGWOWMXLVHVIVGVJVKWKXFXQWJWQACXCVCVLXGTQZXHTQZGXOXPXQGXIYCYDX - CBVMXCCVMVNXNXPXQEXGXHTTXKXGXMVQXKXHXMVQVOVPVRVSXEXFVTZGXGXCXHXEXGXCNYEXE - XFXGXCXEXFXTXGXCWGZXEWOWMXCWLWNWPXDUIVIWRWSXDXTYFSWTABXCWAWBWCWDWHXEXHXCN - YEXEXFXHXCWRXAXDXFXHXCWGSXBACXCWAWBWDWHWEWFWI $. + com eqbrtrd simpr dif1ennn mp3an2i weu euen1b eumo sylbi syl wi f1omvdmvd + ex eleq2 ad2antll difeq1 eleq2d 3imtr4d ad4ant24 fvex pm3.2i eleq1 mp3an1 + imp moi syl12anc adantlr wn fnelnfp sylan bitrd necon2bbid biimpar eqtr4d + wne pm2.61dan eqfnfvd ) AABFZAACFZGZBHIJZKLMZCHIJZWMNZGZGZDABCWJBAOZWKWQA + ABPUAZWKCAOZWJWQAACPUBZWRDUCZAQZGZXCWOQZXCBUDZXCCUDZNZWRXFXIXDWRXFGZEUCZW + OXCUEZIZQZEUFZXGXMQZXHXMQZXIXJXMRLMZXORUMQXJWORUGZLMXFXRUHXJWOWMXSLWLWNWP + XFUIXJWMKXSLWLWNWPXFUJUKULUNWRXFUOWORXCUPUQXRXNEURXOEXMUSXNEUTVAVBWRXFXPW + RXCWMQZXGWMXLIZQZXFXPWJXTYBVCWKWQWJXTYBABXCVDVEUAWPXFXTSWLWNWOWMXCVFVGWPX + PYBSWLWNWPXMYAXGWOWMXLVHVIVGVJVPWKXFXQWJWQACXCVDVKXGTQZXHTQZGXOXPXQGXIYCY + DXCBVLXCCVLVMXNXPXQEXGXHTTXKXGXMVNXKXHXMVNVQVOVRVSXEXFVTZGXGXCXHXEXGXCNYE + XEXFXGXCXEXFXTXGXCWGZXEWOWMXCWLWNWPXDUIVIWRWSXDXTYFSWTABXCWAWBWCWDWEXEXHX + CNYEXEXFXHXCWRXAXDXFXHXCWGSXBACXCWAWBWDWEWFWHWI $. $( If exactly one of two permutations is limited to a set of points, then the composition will not be. (Contributed by Stefan O'Rear, @@ -236439,11 +236510,11 @@ operation is a permutation group (group consisting of permutations), see 16-Aug-2015.) $) pmtrf $p |- ( ( D e. V /\ P C_ D /\ P ~~ 2o ) -> ( T ` P ) : D --> D ) $= ( vz wcel wss c2o cen wbr w3a cv csn cdif cuni cif cfv wa c1o pmtrval com - simpll2 csuc 1onn simpll3 df-2o breqtrdi simpr dif1en mp3an2i eldifi 3syl - en1uniel sseldd wn simplr ifclda fmpt3d ) ADGZBAHZBIJKZLZFAFMZBGZBVDNZOZP - ZVDQABCRFABCDEUAVCVDAGZSZVEVHVDAVJVESZBAVHUTVAVBVIVEUCVKVGTJKZVHVGGVHBGTU - BGVKBTUDZJKVEVLUEVKBIVMJUTVAVBVIVEUFUGUHVJVEUIBTVDUJUKVGUNVHBVFULUMUOVCVI - VEUPUQURUS $. + simpll2 csuc 1onn simpll3 df-2o breqtrdi dif1ennn mp3an2i en1uniel eldifi + simpr 3syl sseldd wn simplr ifclda fmpt3d ) ADGZBAHZBIJKZLZFAFMZBGZBVDNZO + ZPZVDQABCRFABCDEUAVCVDAGZSZVEVHVDAVJVESZBAVHUTVAVBVIVEUCVKVGTJKZVHVGGVHBG + TUBGVKBTUDZJKVEVLUEVKBIVMJUTVAVBVIVEUFUGUHVJVEUMBTVDUIUJVGUKVHBVFULUNUOVC + VIVEUPUQURUS $. $( A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.) $) @@ -236451,14 +236522,14 @@ operation is a permutation group (group consisting of permutations), see dom ( ( T ` P ) \ _I ) = P ) $= ( vz wcel wss c2o cen wbr cfv cdif wne crab cin wceq 3syl wa c1o cv pmtrf w3a cid cdm wf wfn ffn fndifnfp csn cif pmtrfv neeq1d wb iffalse necon1ai - cuni iftrue adantl csuc 1onn simpl3 df-2o breqtrdi simpr mp3an2i en1uniel - com dif1en eldifsni eqnetrd ex impbid2 bitrd rabbidva incom dfin5 eqtr4di - adantr eqtri simp2 df-ss sylib 3eqtrd ) ADGZBAHZBIJKZUCZBCLZUDMUEZFUAZWIL - ZWKNZFAOZBAPZBWHAAWIUFWIAUGWJWNQABCDEUBAAWIUHFAWIUIRWHWNWKBGZFAOZWOWHWMWP - FAWHWKAGZSZWMWPBWKUJMZUQZWKUKZWKNZWPWSWLXBWKABCDWKEULUMWHXCWPUNWRWHXCWPWP - XBWKWPXAWKUOUPWHWPXCWHWPSZXBXAWKWPXBXAQWHWPXAWKURUSXDWTTJKZXAWTGXAWKNTVHG - XDBTUTZJKWPXEVAXDBIXFJWEWFWGWPVBVCVDWHWPVEBTWKVIVFWTVGXABWKVJRVKVLVMVSVNV - OWOABPWQBAVPFABVQVTVRWHWFWOBQWEWFWGWABAWBWCWD $. + cuni iftrue adantl csuc 1onn simpl3 df-2o breqtrdi simpr dif1ennn mp3an2i + com en1uniel eldifsni eqnetrd ex impbid2 bitrd rabbidva incom dfin5 eqtri + adantr eqtr4di simp2 df-ss sylib 3eqtrd ) ADGZBAHZBIJKZUCZBCLZUDMUEZFUAZW + ILZWKNZFAOZBAPZBWHAAWIUFWIAUGWJWNQABCDEUBAAWIUHFAWIUIRWHWNWKBGZFAOZWOWHWM + WPFAWHWKAGZSZWMWPBWKUJMZUQZWKUKZWKNZWPWSWLXBWKABCDWKEULUMWHXCWPUNWRWHXCWP + WPXBWKWPXAWKUOUPWHWPXCWHWPSZXBXAWKWPXBXAQWHWPXAWKURUSXDWTTJKZXAWTGXAWKNTV + HGXDBTUTZJKWPXEVAXDBIXFJWEWFWGWPVBVCVDWHWPVEBTWKVFVGWTVIXABWKVJRVKVLVMVSV + NVOWOABPWQBAVPFABVQVRVTWHWFWOBQWEWFWGWABAWBWCWD $. $} ${ @@ -236532,19 +236603,19 @@ operation is a permutation group (group consisting of permutations), see ( vx wcel wf wfn cdif cfv cen wbr wceq syl wa c1o sylan eqtrd cid cdm cvv ccom cres wss c2o w3a pmtrfrn simpld pmtrf simprd feq1d mpbird fco anidms eqid ffn 3syl fnresi a1i cv csn cif pmtrffv iftrue sylan9eq fveq2d simpll - cuni simp2d ad2antrr csuc 1onn simp3d df-2o breqtrdi simpr dif1en mp3an2i - com en1uniel eldifad sseldd syl2anc adantr en2other2 ancoms wn wb fnelnfp - wne ffnd necon2bbid biimpar fveq2 pm2.61dan fvresi adantl 3eqtr4d eqfnfvd - id fvco2 ) DBHZGADDUDZUAAUEZXDAADIZAAXEIZXEAJXDXGAADUAKUBZCLZIZXDAUCHZXIA - UFZXIUGMNZUHZXKXDXODXJOZAXIBCDEFXIUQZUIZUJZAXICUCEUKPXDAADXJXDXOXPXRULUMU - NZXGXHAAADDUOUPAAXEURUSXFAJXDAUTVAXDGVBZAHZQZYADLZDLZYAYAXELZYAXFLZYCYAXI - HZYEYAOZYCYHQZYEXIYAVCZKZVJZDLZYAYJYDYMDYCYHYDYHYMYAVDYMAXIBCDYAEFXQVEYHY - MYAVFVGVHYJYNYMXIHZXIYMVCKVJZYMVDZYAYJXDYMAHYNYQOXDYBYHVIYJXIAYMXDXMYBYHX - DXLXMXNXSVKVLYJYMXIYKYJYLRMNZYMYLHRWAHYJXIRVMZMNZYHYRVNXDYTYBYHXDXIUGYSMX - DXLXMXNXSVOZVPVQVLYCYHVRXIRYAVSVTYLWBPWCZWDAXIBCDYMEFXQVEWEYJYQYPYAYJYOYQ - YPOUUBYOYPYMVFPYCXNYHYPYAOZXDXNYBUUAWFYHXNUUCXIYAWGWHSTTTYCYHWIZQYDYAOZYI - YCUUEUUDYCYHYDYAXDDAJZYBYHYDYAWLWJXDAADXTWMZADYAWKSWNWOUUEYEYDYAYDYADWPUU - EXBTPWQXDUUFYBYFYEOUUGADDYAXCSYBYGYAOXDAYAWRWSWTXA $. + cuni simp2d ad2antrr com csuc 1onn simp3d df-2o breqtrdi dif1ennn mp3an2i + simpr en1uniel eldifad sseldd syl2anc adantr en2other2 ancoms wn wne ffnd + wb fnelnfp necon2bbid biimpar fveq2 pm2.61dan fvco2 fvresi adantl 3eqtr4d + id eqfnfvd ) DBHZGADDUDZUAAUEZXDAADIZAAXEIZXEAJXDXGAADUAKUBZCLZIZXDAUCHZX + IAUFZXIUGMNZUHZXKXDXODXJOZAXIBCDEFXIUQZUIZUJZAXICUCEUKPXDAADXJXDXOXPXRULU + MUNZXGXHAAADDUOUPAAXEURUSXFAJXDAUTVAXDGVBZAHZQZYADLZDLZYAYAXELZYAXFLZYCYA + XIHZYEYAOZYCYHQZYEXIYAVCZKZVJZDLZYAYJYDYMDYCYHYDYHYMYAVDYMAXIBCDYAEFXQVEY + HYMYAVFVGVHYJYNYMXIHZXIYMVCKVJZYMVDZYAYJXDYMAHYNYQOXDYBYHVIYJXIAYMXDXMYBY + HXDXLXMXNXSVKVLYJYMXIYKYJYLRMNZYMYLHRVMHYJXIRVNZMNZYHYRVOXDYTYBYHXDXIUGYS + MXDXLXMXNXSVPZVQVRVLYCYHWAXIRYAVSVTYLWBPWCZWDAXIBCDYMEFXQVEWEYJYQYPYAYJYO + YQYPOUUBYOYPYMVFPYCXNYHYPYAOZXDXNYBUUAWFYHXNUUCXIYAWGWHSTTTYCYHWIZQYDYAOZ + YIYCUUEUUDYCYHYDYAXDDAJZYBYHYDYAWJWLXDAADXTWKZADYAWMSWNWOUUEYEYDYAYDYADWP + UUEXBTPWQXDUUFYBYFYEOUUGADDYAWRSYBYGYAOXDAYAWSWTXAXC $. $( A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.) $)