Prove ctssdclemr in terms of ctssdccl in iset.mm

Author: jkingdon

iset.mm

@@ -68342,52 +68342,15 @@ property of disjoint unions (see ~ updjud in the case of functions).
     ctssdclemr $p |- ( E. f f : _om -onto-> ( A |_| 1o )
         -> E. s ( s C_ _om /\ E. f f : s -onto-> A
         /\ A. n e. _om DECID n e. s ) ) $=
-      ( vg vt vx vy vz com c1o cv wex wcel cfv cinl wceq cvv wa adantl cdju wfo
-      wss wdc wral w3a foeq1 cbvexv cima crab ssrab2 ccnv ccom wf wrex wfn wfun
-      cdm c0 csn cxp wf1o djulf1o f1ocnv f1ofun mp2b fofun funco sylancr eleq2d
-      fof fdmd anbi1d wb dmcoss sseli pm4.71ri dmfco pm5.32da syl5bb cinr simpr
-      syl crn imassrn df-rn eleq2i sylib 2thd cin djuin disjel mpan con2i dfrn4
-      wn eleq2s sylnib 2falsed cun ffvelrnda djuun sylibr elun mpjaodan 3bitr4d
-      wo weq fveq2 eleq1d elrab eqrdv df-fn sylanbrc adantr biimpi simpld fvco3
-      syl6bbr syl2anc ax-mp fvelima simpl2im simprr fveq2d vex f1ocnvfv1 simprl
-      mp2an syl5eqel eqeltrrd rexlimddv eqeltrd ralrimiva ffnfv df-rex ex spcev
-      mpd dcbid djulcl foelrn sylan2 wi f1odm eleqtrri funfvima ad2antlr elrabd
-      jca eximdv syl5eqr ad2antrr elrabi eqtr4d reximdva cofunexg bitr3i orim2i
-      dffo3 df-dc ibar mpbid rabex sseq1 foeq2 exbidv ralbidv 3anbi123d mp3an2i
-      omex eleq2 exlimiv sylbi ) JAKUAZBLZUBZBMJUVOELZUBZEMDLZJUCZUVTAUVPUBZBMZ
-      CLZUVTNZUDZCJUEZUFZDMZUVQUVSBEJUVOUVPUVRUGUHUVSUWIEFLZUVROZPAUIZNZFJUJZJU
-      CZUVSUWNAUVPUBZBMZUWDUWNNZUDZCJUEZUWIUWMFJUKUVSUWNAPULZUVRUMZUBZUWQUVSUWN
-      AUXBUNZGLZHLZUXBOZQZHUWNUOZGAUEUXCUVSUXBUWNUPZUXEUXBOZANZGUWNUEUXDUVSUXBU
-      QZUXBURZUWNQUXJUVSUXAUQZUVRUQZUXMRUSUTRVAZPVBZUXQRUXAVBUXOVCRUXQPVDUXQRUX
-      AVEVFZJUVOUVRVGZUXAUVRVHVIUVSCUXNUWNUVSUWDUXNNZUWDJNZUWDUVROZUWLNZSZUWRUV
-      SUWDUVRURZNZUYCUXAURZNZSZUYBUYISUYAUYEUVSUYGUYBUYIUVSUYFJUWDUVSJUVOUVRJUV
-      OUVRVKZVLVJVMUVSUXPUYAUYJVNUXTUYAUYGUYASUXPUYJUYAUYGUXNUYFUWDUXAUVRVOVPVQ
-      UXPUYGUYAUYIUWDUXAUVRVRVSVTWCUVSUYBUYDUYIUVSUYBSZUYDUYDUYIVNUYCWAKUIZNZUY
-      LUYDSZUYDUYIUYLUYDWBUYOUYCPWDZNZUYIUYDUYQUYLUWLUYPUYCPAWEVPTUYPUYHUYCPWFW
-      GZWHWIUYLUYNSZUYDUYIUYNUYDWPZUYLUYDUYNUWLUYMWJUSQUYDUYNWPZAKWKUWLUYMUYCWL
-      WMWNZTUYSUYQUYIUYNUYQWPUYLUYQUYNVUAUYCPRUIZUYPVUCUYMWJUSQUYCVUCNVUARKWKVU
-      CUYMUYCWLWMPWOWQWNTUYRWRWSUYLUYCUWLUYMWTZNZUYDUYNXGZUYLUYCUVONZVUEUVSJUVO
-      UWDUVRUYKXAZVUDUVOUYCAKXBWGZXCUYCUWLUYMXDZWHXEVSXFUWMUYDFUWDJFCXHUWKUYCUW
-      LUWJUWDUVRXIXJXKZXSXLUXBUWNXMXNUVSUXLGUWNUVSUXEUWNNZSZUXKUXEUVROZUXAOZAVU
-      MJUVOUVRUNZUXEJNZUXKVUOQUVSVUPVULUYKXOVUMVUQVUNUWLNZVULVUQVURSZUVSVULVUSU
-      WMVURFUXEJFGXHUWKVUNUWLUWJUXEUVRXIXJXKXPTZXQJUVOUXEUXAUVRXRXTVUMILZPOZVUN
-      QZVUOANIAVUMVUQVURVVCIAUOZVUTPUQZVURVVDUXRVVEVCRUXQPVEYAZIVUNAPYBWMYCVUMV
-      VAANZVVCSSZVVBUXAOZVUOAVVHVVBVUNUXAVUMVVGVVCYDYEVVHVVIVVAAUXRVVARNVVIVVAQ
-      VCIYFRUXQVVAPYGYIVUMVVGVVCYHYJYKYLYMYNGUWNAUXBYOXNUVSUXIGAUVSUXEANZSZUXEP
-      OZUXFUVROZQZHUWNUOZUXIVVKUXFUWNNZVVNSZHMZVVOVVKUXFJNZVVNSZHMZVVRVVJUVSVVL
-      UVONZVWAAKUXEUUAUVSVWBSVVNHJUOVWAHJUVOVVLUVRUUBVVNHJYPWHUUCVVKVVTVVQHVVKV
-      VTVVQVVKVVTSZVVPVVNVWCUWMVVMUWLNFUXFJFHXHUWKVVMUWLUWJUXFUVRXIXJVVKVVSVVNY
-      HVWCVVLVVMUWLVVKVVSVVNYDZVVJVVLUWLNZUVSVVTVVEUXEPURZNVVJVWEUUDVVFUXERVWFG
-      YFZUXRVWFRQVCRUXQPUUEYAUUFAUXEPUUGYIUUHYKUUIVWDUUJYQUUKYSVVNHUWNYPXCVVKVV
-      NUXHHUWNVVKVVPSZVVNUXHVWHVVNSZUXEVVMUXAOZUXGVWIUXEVVLUXAOZVWJUXRUXERNVWKU
-      XEQVCVWGRUXQUXEPYGYIVWIVVLVVMUXAVWHVVNWBYEUULVWHUXGVWJQZVVNVWHVUPVVSVWLUV
-      SVUPVVJVVPUYKUUMVVPVVSVVKUWMFUXFJUUNTJUVOUXFUXAUVRXRXTXOUUOYQUUPYSYNHGUWN
-      AUXBUUTXNUWPUXCBUXBUXOUVRRNUXBRNUXSEYFUXAUVRRUUQYIUWNAUVPUXBUGYRWCUVSUWSC
-      JUYLUYDUDZUWSUYLUYDUYTXGZVWMUYLVUFVWNUYLVUGVUFVUHVUGVUEVUFVUIVUJUURWHUYNU
-      YTUYDVUBUUSWCUYDUVAXCUYLUYDUWRUYLUYDUYEUWRUYBUYDUYEVNUVSUYBUYDUVBTVUKXSYT
-      UVCYNUWHUWOUWQUWTUFDUWNUWMFJUVKUVDUVTUWNQZUWAUWOUWCUWQUWGUWTUVTUWNJUVEVWO
-      UWBUWPBUVTUWNAUVPUVFUVGVWOUWFUWSCJVWOUWEUWRUVTUWNUWDUVLYTUVHUVIYRUVJUVMUV
-      N $.
+      ( vg vt com cv wfo wex wss wcel wdc wral w3a foeq1 cinl eqid cvv wf1o c1o
+      cdju cbvexv cfv cima crab ccnv ccom id ctssdccl c0 csn cxp djulf1o f1ocnv
+      wfun f1ofun mp2b cofunexg mp2an spcev 3anim2i omex rabex wceq sseq1 foeq2
+      vex syl exbidv eleq2 dcbid ralbidv 3anbi123d exlimiv sylbi ) GAUAUBZBHZIZ
+      BJGVQEHZIZEJDHZGKZWBAVRIZBJZCHZWBLZMZCGNZOZDJZVSWABEGVQVRVTPUCWAWKEWAFHVT
+      UDQAUELZFGUFZGKZWMAVRIZBJZWFWMLZMZCGNZOZWKWAWNWMAQUGZVTUHZIZWSOWTWAFAWMCV
+      TXBWAUIWMRXBRUJXCWPWNWSWOXCBXBXAUPZVTSLXBSLSUKULSUMZQTXESXATXDUNSXEQUOXES
+      XAUQUREVHXAVTSUSUTWMAVRXBPVAVBVIWJWTDWMWLFGVCVDWBWMVEZWCWNWEWPWIWSWBWMGVF
+      XFWDWOBWBWMAVRVGVJXFWHWRCGXFWGWQWBWMWFVKVLVMVNVAVIVOVP $.
   $}
 
   ${