Add ctssdccl to iset.mm

This is ctssdclemr but expressed in terms of class variables not
there-exists

Author: jkingdon

iset.mm

@@ -68279,6 +68279,61 @@ property of disjoint unions (see ~ updjud in the case of functions).
       EUUHWTZAYTUVPUBBNYDXAXBXCXFXDLUAMXMXTXGXHYCYADXTKMXSXIXJMXMYBXTXKXLUO $.
   $}
 
+  ${
+    $d A m x y z $.  $d F m n x y z $.  $d G m n y $.  $d S m n y z $.
+    $d ph m n y z $.
+    ctssdccl.f $e |- ( ph -> F : _om -onto-> ( A |_| 1o ) ) $.
+    ctssdccl.s $e |- S = { x e. _om | ( F ` x ) e. ( inl " A ) } $.
+    ctssdccl.g $e |- G = ( `' inl o. F ) $.
+    $( A mapping from a decidable subset of the natural numbers onto a
+       countable set.  This is similar to one direction of ~ ctssdc but
+       expressed in terms of classes rather than ` E. ` .  (Contributed by Jim
+       Kingdon, 30-Oct-2023.) $)
+    ctssdccl $p |- ( ph -> ( S C_ _om /\ G : S -onto-> A
+        /\ A. n e. _om DECID n e. S ) ) $=
+      ( vm vy com wcel cfv cinl wceq cvv c1o wa vz wss wfo wdc wral cima ssrab2
+      cv crab eqsstri a1i wf wrex wfn wfun cdm ccnv csn cxp wf1o djulf1o f1ocnv
+      c0 f1ofun mp2b cdju fofun syl ccom funco funeqi sylibr sylancr fof eleq2d
+      fdmd anbi1d wb dmcoss sseli pm4.71ri dmfco pm5.32da syl5bb cinr simpr crn
+      imassrn adantl df-rn eleq2i sylib 2thd cin djuin disjel mpan con2i eleq2s
+      wn dfrn4 sylnib 2falsed cun wo ffvelrnda djuun mpjaodan 3bitr4d dmeqi weq
+      elun fveq2 eleq1d elrab2 eqrdv df-fn sylanbrc fveq1i adantr biimpi simpld
+      3bitr4g fvco3 syl2anc syl5eq ax-mp fvelima simprr fveq2d f1ocnvfv1 simprl
+      vex mp2an eqeltrrd ralrimiva wex df-rex ex mpd simpl2im rexlimddv eqeltrd
+      syl5eqel ffnfv djulcl sylan wi f1odm eleqtrri funfvima ad2antlr syl6eleqr
+      foelrn sylan2 elrabd eximdv syl5eqr ad2antrr eqtr4d reximdva dffo3 bitr3i
+      jca orim2i df-dc ibar syl6bbr dcbid mpbid 3jca ) ADMUBZDCGUCZEUHZDNZUDZEM
+      UEUVLADBUHZFOZPCUFZNZBMUIZMIUVTBMUGUJZUKADCGULZKUHZLUHZGOZQZLDUMZKCUEUVMA
+      GDUNZUWDGOZCNZKDUEUWCAGUOZGUPZDQUWIAPUQZUOZFUOZUWLRVCURRUSZPUTZUWQRUWNUTU
+      WOVARUWQPVBUWQRUWNVDVEAMCSVFZFUCZUWPHMUWSFVGVHZUWOUWPTUWNFVIZUOUWLUWNFVJG
+      UXBJVKVLVMAEUWMDAUVNUXBUPZNZUVNMNZUVNFOZUVSNZTZUVNUWMNUVOAUVNFUPZNZUXFUWN
+      UPZNZTZUXEUXLTUXDUXHAUXJUXEUXLAUXIMUVNAMUWSFAUWTMUWSFULZHMUWSFVNVHZVPVOVQ
+      AUWPUXDUXMVRUXAUXDUXJUXDTUWPUXMUXDUXJUXCUXIUVNUWNFVSVTWAUWPUXJUXDUXLUVNUW
+      NFWBWCWDVHAUXEUXGUXLAUXETZUXGUXGUXLVRUXFWESUFZNZUXPUXGTZUXGUXLUXPUXGWFUXS
+      UXFPWGZNZUXLUXGUYAUXPUVSUXTUXFPCWHVTWIUXTUXKUXFPWJWKZWLWMUXPUXRTZUXGUXLUX
+      RUXGWTZUXPUXGUXRUVSUXQWNVCQUXGUXRWTZCSWOUVSUXQUXFWPWQWRZWIUYCUYAUXLUXRUYA
+      WTUXPUYAUXRUYEUXFPRUFZUXTUYGUXQWNVCQUXFUYGNUYERSWOUYGUXQUXFWPWQPXAWSWRWIU
+      YBXBXCUXPUXFUVSUXQXDZNZUXGUXRXEZUXPUXFUWSNZUYIAMUWSUVNFUXOXFZUYHUWSUXFCSX
+      GWKZVLUXFUVSUXQXLZWLXHWCXIUWMUXCUVNGUXBJXJWKUVTUXGBUVNMDBEXKUVRUXFUVSUVQU
+      VNFXMXNIXOZYCXPGDXQXRAUWKKDAUWDDNZTZUWJUWDFOZUWNOZCUYQUWJUWDUXBOZUYSUWDGU
+      XBJXSUYQUXNUWDMNZUYTUYSQAUXNUYPUXOXTUYQVUAUYRUVSNZUYPVUAVUBTZAUYPVUCUVTVU
+      BBUWDMDBKXKUVRUYRUVSUVQUWDFXMXNIXOYAWIZYBMUWSUWDUWNFYDYEYFUYQUAUHZPOZUYRQ
+      ZUYSCNUACUYQVUAVUBVUGUACUMZVUDPUOZVUBVUHUWRVUIVARUWQPVDYGZUAUYRCPYHWQUUAU
+      YQVUECNZVUGTTZVUFUWNOZUYSCVULVUFUYRUWNUYQVUKVUGYIYJVULVUMVUECUWRVUERNVUMV
+      UEQVAUAYMRUWQVUEPYKYNUYQVUKVUGYLUUDYOUUBUUCYPKDCGUUEXRAUWHKCAUWDCNZTZUWDP
+      OZUWEFOZQZLDUMZUWHVUOUWEDNZVURTZLYQZVUSVUOUWEMNZVURTZLYQZVVBVUNAVUPUWSNZV
+      VECSUWDUUFAVVFTVURLMUMZVVEAUWTVVFVVGHLMUWSVUPFUUNUUGVURLMYRWLUUOVUOVVDVVA
+      LVUOVVDVVAVUOVVDTZVUTVURVVHUWEUWADVVHUVTVUQUVSNBUWEMBLXKUVRVUQUVSUVQUWEFX
+      MXNVUOVVCVURYLVVHVUPVUQUVSVUOVVCVURYIZVUNVUPUVSNZAVVDVUIUWDPUPZNVUNVVJUUH
+      VUJUWDRVVKKYMZUWRVVKRQVARUWQPUUIYGUUJCUWDPUUKYNUULYOUUPIUUMVVIUVDYSUUQYTV
+      URLDYRVLVUOVURUWGLDVUOVUTTZVURUWGVVMVURTZUWDVUQUWNOZUWFVVNUWDVUPUWNOZVVOU
+      WRUWDRNVVPUWDQVAVVLRUWQUWDPYKYNVVNVUPVUQUWNVVMVURWFYJUURVVMUWFVVOQVURVVMU
+      WFUWEUXBOZVVOUWEGUXBJXSVVMUXNVVCVVQVVOQAUXNVUNVUTUXOUUSVUTVVCVUODMUWEUWBV
+      TWIMUWSUWEUWNFYDYEYFXTUUTYSUVAYTYPLKDCGUVBXRAUVPEMUXPUXGUDZUVPUXPUXGUYDXE
+      ZVVRUXPUYJVVSUXPUYKUYJUYLUYKUYIUYJUYMUYNUVCWLUXRUYDUXGUYFUVEVHUXGUVFVLUXP
+      UXGUVOUXPUXGUXHUVOUXEUXGUXHVRAUXEUXGUVGWIUYOUVHUVIUVJYPUVK $.
+  $}
+
   ${
     $d A f g s t $.  $d A g n s t x y z $.
     $( Lemma for ~ ctssdc .  Showing that our usual definition of countable