Add ctiunct to iset.mm

This states that the union of countably many countable sets is countable
(subject to a caveat described in the comment).

Includes lemmas ctiunctlemf , ctiunctlemfo , ctiunctlemu1st , ctiunctlemu2nd ,
ctiunctlemuom , and ctiunctlemudc

Author: jkingdon

iset.mm

@@ -129744,6 +129744,174 @@ then the Limited Principle of Omniscience (LPO) implies excluded middle.
       JOABECWKWM $.
   $}
 
+  ${
+    ctiunct.som $e |- ( ph -> S C_ _om ) $.
+    ctiunct.sdc $e |- ( ph -> A. n e. _om DECID n e. S ) $.
+    ctiunct.f $e |- ( ph -> F : S -onto-> A ) $.
+    ctiunct.tom $e |- ( ( ph /\ x e. A ) -> T C_ _om ) $.
+    ctiunct.tdc $e |- ( ( ph /\ x e. A ) -> A. n e. _om DECID n e. T ) $.
+    ctiunct.g $e |- ( ( ph /\ x e. A ) -> G : T -onto-> B ) $.
+    ctiunct.j $e |- ( ph -> J : _om -1-1-onto-> ( _om X. _om ) ) $.
+    ctiunct.u $e |- U = { z e. _om | ( ( 1st ` ( J ` z ) ) e. S
+      /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) } $.
+
+    ${
+      $d F z $.  $d J z $.  $d N z $.  $d S z $.  $d T z $.  $d x z $.
+      ctiunctlem.n $e |- ( ph -> N e. U ) $.
+      $( Lemma for ~ ctiunct .  (Contributed by Jim Kingdon, 28-Oct-2023.) $)
+      ctiunctlemu1st $p |- ( ph -> ( 1st ` ( J ` N ) ) e. S ) $=
+        ( cfv c1st wcel c2nd csb com wa cv 2fveq3 eleq1d fveq2d csbeq1d eleq12d
+        wceq anbi12d elrab2 sylib simprd simpld ) AMLUCZUDUCZFUEZVBUFUCZBVCJUCZ
+        GUGZUEZAMUHUEZVDVHUIZAMHUEVIVJUIUBCUJZLUCZUDUCZFUEZVLUFUCZBVMJUCZGUGZUE
+        ZUIVJCMUHHVKMUPZVNVDVRVHVSVMVCFVKMUDLUKZULVSVOVEVQVGVKMUFLUKVSBVPVFGVSV
+        MVCJVTUMUNUOUQUAURUSUTVA $.
+
+      $( Lemma for ~ ctiunct .  (Contributed by Jim Kingdon, 28-Oct-2023.) $)
+      ctiunctlemu2nd $p |- ( ph -> ( 2nd ` ( J ` N ) )
+          e. [_ ( F ` ( 1st ` ( J ` N ) ) ) / x ]_ T ) $=
+        ( cfv c1st wcel c2nd csb com wa cv 2fveq3 eleq1d fveq2d csbeq1d eleq12d
+        wceq anbi12d elrab2 sylib simprd ) AMLUCZUDUCZFUEZVAUFUCZBVBJUCZGUGZUEZ
+        AMUHUEZVCVGUIZAMHUEVHVIUIUBCUJZLUCZUDUCZFUEZVKUFUCZBVLJUCZGUGZUEZUIVICM
+        UHHVJMUPZVMVCVQVGVRVLVBFVJMUDLUKZULVRVNVDVPVFVJMUFLUKVRBVOVEGVRVLVBJVSU
+        MUNUOUQUAURUSUTUT $.
+    $}
+
+    $( Lemma for ~ ctiunct .  (Contributed by Jim Kingdon, 28-Oct-2023.) $)
+    ctiunctlemuom $p |- ( ph -> U C_ _om ) $=
+      ( com wss cv cfv c1st wcel c2nd csb wa crab ssrab2 eqsstri a1i ) HUAUBAHC
+      UCLUDZUEUDZFUFUNUGUDBUOJUDGUHUFUIZCUAUJUATUPCUAUKULUM $.
+
+    ${
+      $d A x $.  $d F n x $.  $d F x z $.  $d J n x $.  $d J x z $.  $d S n $.
+      $d S z $.  $d T n $.  $d T z $.  $d U m n $.  $d m ph x $.  $d m x z $.
+      $( Lemma for ~ ctiunct .  (Contributed by Jim Kingdon, 28-Oct-2023.) $)
+      ctiunctlemudc $p |- ( ph -> A. n e. _om DECID n e. U ) $=
+        ( vm cv wcel wdc com wral wa cfv c1st c2nd csb wn wceq eleq1 adantr cxp
+        dcbid wf1o f1of syl simpr ffvelrnd xp1st rspcdva wfo ad2antrr ralrimiva
+        wf fof nfcv nfcsb1v nfcri nfdc nfralya csbeq1a eleq2d ralbidv rspc sylc
+        xp2nd dcan wo intnanrd olcd df-dc sylibr exmiddc mpjaodan adantl 2fveq3
+        wb eleq1d fveq2d csbeq1d eleq12d anbi12d elrab2 syl6rbbr mpbird cbvralv
+        ibar sylib ) AUAUBZHUCZUDZUAUEUFIUBZHUCZUDZIUEUFAXEUAUEAXCUEUCZUGZXEXCL
+        UHZUIUHZFUCZXKUJUHZBXLJUHZGUKZUCZUGZUDZXJXMXSXMULZXJXMUGZXMUDZXQUDZXSXJ
+        YBXMXJXFFUCZUDZYBIUEXLXFXLUMYDXMXFXLFUNUQAYEIUEUFXINUOXJXKUEUEUPZUCZXLU
+        EUCXJUEYFXCLXJUEYFLURZUEYFLVHAYHXISUOUEYFLUSUTAXIVAVBZXKUEUEVCUTVDZUOYA
+        XFXPUCZUDZYCIUEXNXFXNUMYKXQXFXNXPUNUQYAXODUCXFGUCZUDZIUEUFZBDUFZYLIUEUF
+        ZYAFDXLJAFDJVHZXIXMAFDJVEYROFDJVIUTVFXJXMVAVBAYPXIXMAYOBDQVGVFYOYQBXODY
+        LBIUEBUEVJYKBBIXPBXOGVKVLVMVNBUBXOUMZYNYLIUEYSYMYKYSGXPXFBXOGVOVPUQVQVR
+        VSYAYGXNUEUCXJYGXMYIUOXKUEUEVTUTVDXMXQWAVSXJXTUGZXRXRULZWBXSYTUUAXRYTXM
+        XQXJXTVAWCWDXRWEWFXJYBXMXTWBYJXMWGUTWHXJXDXRXJXRXIXRUGZXDXIXRUUBWKAXIXR
+        XAWICUBZLUHZUIUHZFUCZUUDUJUHZBUUEJUHZGUKZUCZUGXRCXCUEHUUCXCUMZUUFXMUUJX
+        QUUKUUEXLFUUCXCUILWJZWLUUKUUGXNUUIXPUUCXCUJLWJUUKBUUHXOGUUKUUEXLJUULWMW
+        NWOWPTWQWRUQWSVGXEXHUAIUEXCXFUMXDXGXCXFHUNUQWTXB $.
+    $}
+
+    ctiunct.h $e |- H = ( n e. U |-> ( [_ ( F ` ( 1st ` ( J ` n ) ) ) / x ]_ G
+      ` ( 2nd ` ( J ` n ) ) ) ) $.
+
+    ${
+      $d A n x y $.  $d B n y $.  $d F x y $.  $d F z $.  $d G y $.
+      $d J x y $.  $d J z $.  $d S z $.  $d T z $.  $d U n $.  $d n ph x $.
+      $d x n z $.
+      $( Lemma for ~ ctiunct .  (Contributed by Jim Kingdon, 28-Oct-2023.) $)
+      ctiunctlemf $p |- ( ph -> H : U --> U_ x e. A B ) $=
+        ( vy cv cfv c2nd c1st csb ciun wcel wrex wfo adantr fof syl com wss wdc
+        wa wral adantlr cxp wf1o simpr ctiunctlemu1st ffvelrnd ralrimiva rspsbc
+        wf wsbc sylc wb sbcfg mpbid ctiunctlemu2nd csbeq1 eleq2d rspcev syl2anc
+        wceq eliun sylibr nfcv nfcsb1v csbeq1a cbviun syl6eleqr fmptd ) AIHIUDZ
+        MUEZUFUEZBWJUGUEZJUEZKUHZUEZBDEUIZLAWIHUJZUSZWOUCDBUCUDZEUHZUIZWPWRWOWT
+        UJZUCDUKZWOXAUJWRWMDUJZWOBWMEUHZUJZXCWRFDWLJWRFDJULZFDJVIAXGWQPUMZFDJUN
+        UOWRBCDEFGHIJKMWIAFUPUQWQNUMZAWIFUJURIUPUTWQOUMZXHABUDDUJZGUPUQWQQVAZAX
+        KWIGUJURIUPUTWQRVAZAXKGEKULZWQSVAZAUPUPUPVBMVCWQTUMZUAAWQVDZVEVFZWRBWMG
+        UHZXEWKWNWRGEKVIZBWMVJZXSXEWNVIZWRXDXTBDUTZYAXRAYCWQAXTBDAXKUSXNXTSGEKU
+        NUOVGUMXTBWMDVHVKWRXDYAYBVLXRBGEKDWMVMUOVNWRBCDEFGHIJKMWIXIXJXHXLXMXOXP
+        UAXQVOVFXBXFUCWMDWSWMVTWTXEWOBWSWMEVPVQVRVSUCWODWTWAWBBUCDEWTUCEWCBWSEW
+        DBWSEWEWFWGUBWH $.
+    $}
+
+    ${
+      $d A n r w x $.  $d A r u v w x $.  $d B n r w $.  $d B r u v w $.
+      $d F n r x $.  $d F r x z $.  $d G n r w $.  $d H r u v w $.  $d J n x $.
+      $d J v x $.  $d J x z $.  $d S r z $.  $d T r w z $.  $d U n r w $.
+      $d U r u v w $.  $d n ph r w x $.  $d ph r u w x $.  $d n z $.
+      ctiunct.nfh $e |- F/_ x H $.
+      ctiunct.nfu $e |- F/_ x U $.
+      $( Lemma for ~ ctiunct .  (Contributed by Jim Kingdon, 28-Oct-2023.) $)
+      ctiunctlemfo $p |- ( ph -> H : U -onto-> U_ x e. A B ) $=
+        ( vu vv vw vr ciun wf cv cfv wceq wrex wral wfo ctiunctlemf wcel wa nfv
+        nfiu1 nfcri nfan nfcv nffv nfeq2 nfrexxy simplll simplr foelrn sylancom
+        syl2anc ad4antr simpllr cop ccnv com c1st c2nd csb cxp wf1o f1ocnv f1of
+        syl ad5antr wss simprl sseldd simp-5l adantr simplrl ffvelrnd f1ocnvfv2
+        opelxpd fveq2d op1st syl6eq eqeltrd op2nd simprr eqtr4d csbeq1d 3eltr4d
+        vex csbid 2fveq3 eleq1d eleq12d anbi12d elrab2 sylanbrc fveq12d simplrr
+        jca eqeltrrd fvmptd3 3eqtr4rd fveq2 rspceeqv rexlimddv biimpi r19.29af2
+        eliun adantl ralrimiva dffo3 ) AHBDEUIZLUJUEUKZUFUKZLULZUMZUFHUNZUEYHUO
+        HYHLUPABCDEFGHIJKLMNOPQRSTUAUBUQAYMUEYHAYIYHURZUSZYIEURZYMBDAYNBABUTBUE
+        YHBDEVAVBVCYLBUFHUDBYIYKBYJLUCBYJVDVEVFVGYOBUKZDURZUSZYPUSZYIUGUKZKULZU
+        MZYMUGGYSYPGEKUPZUUCUGGUNYTAYRUUDAYNYRYPVHYOYRYPVISVLUGGEYIKVJVKYTUUAGU
+        RZUUCUSZUSZYQUHUKZJULZUMZYMUHFUUGFDJUPZYRUUJUHFUNAUUKYNYRYPUUFPVMYOYRYP
+        UUFVNZUHFDYQJVJVLUUGUUHFURZUUJUSZUSZUUHUUAVOZMVPZULZHURZYIUURLULZUMYMUU
+        OUURVQURUURMULZVRULZFURZUVAVSULZBUVBJULZGVTZURZUSZUUSUUOVQVQWAZVQUUPUUQ
+        AUVIVQUUQUJZYNYRYPUUFUUNAUVIVQUUQWBZUVJAVQUVIMWBZUVKTVQUVIMWCWEUVIVQUUQ
+        WDWEWFUUOUUHUUAVQVQUUOFVQUUHAFVQWGYNYRYPUUFUUNNWFUUGUUMUUJWHZWIUUOGVQUU
+        AUUOAYRGVQWGAYNYRYPUUFUUNWJZUUGYRUUNUULWKQVLYTUUEUUCUUNWLZWIWOZWMUUOUVC
+        UVGUUOUVBUUHFUUOUVBUUPVRULUUHUUOUVAUUPVRUUOUVLUUPUVIURUVAUUPUMUUOAUVLUV
+        NTWEUVPVQUVIUUPMWNVLZWPUUHUUAUHXEZUGXEZWQWRZUVMWSUUOUUAGUVDUVFUVOUUOUVD
+        UUPVSULUUAUUOUVAUUPVSUVQWPUUHUUAUVRUVSWTWRZUUOUVFBYQGVTGUUOBUVEYQGUUOUV
+        EUUIYQUUOUVBUUHJUVTWPUUGUUMUUJXAXBZXCBGXFWRXDXOCUKZMULZVRULZFURZUWDVSUL
+        ZBUWEJULZGVTZURZUSUVHCUURVQHUWCUURUMZUWFUVCUWJUVGUWKUWEUVBFUWCUURVRMXGZ
+        XHUWKUWGUVDUWIUVFUWCUURVSMXGUWKBUWHUVEGUWKUWEUVBJUWLWPXCXIXJUAXKXLZUUOU
+        VDBUVEKVTZULZUUBUUTYIUUOUVDUUAUWNKUUOUWNBYQKVTKUUOBUVEYQKUWBXCBKXFWRUWA
+        XMZUUOIUURIUKZMULZVSULZBUWRVRULZJULZKVTZULUWOHLEUBUWQUURUMZUWSUVDUXBUWN
+        UXCBUXAUVEKUXCUWTUVBJUWQUURVRMXGWPXCUWQUURVSMXGXMUWMUUOYIUWOEUUOYIUUBUW
+        OYTUUEUUCUUNXNZUWPXBYSYPUUFUUNVNXPXQUXDXRUFUURHYKUUTYIYJUURLXSXTVLYAYAY
+        NYPBDUNZAYNUXEBYIDEYDYBYEYCYFUFUEHYHLYGXL $.
+    $}
+  $}
+
+  ${
+    $d A h j k x $.  $d A j k n u x z $.  $d A k n u w x z $.  $d B h j k $.
+    $d B j k n u z $.  $d B k n u w z $.  $d F k n u w x z $.
+    $d G k n u w z $.  $d j n ph x $.
+    ctiunct.a $e |- ( ph -> F : _om -onto-> ( A |_| 1o ) ) $.
+    ctiunct.b $e |- ( ( ph /\ x e. A )
+      -> G : _om -onto-> ( B |_| 1o ) ) $.
+    $( The union of countably many countable sets is countable.  The
+       construction here is constructive in the sense that the hypothesis
+       provides a specific class for ` G ` in terms of ` x ` , as opposed to a
+       construction of the form ` A. x e. A E. g ` .  Countable choice would be
+       needed to turn the latter into the former.
+
+       The proof proceeds by mapping a natural number to a pair of natural
+       numbers (by ~ xpomen ) and using the first number to map to an element
+       ` x ` of ` A ` and the second number to map to an element of B(x) .  In
+       this way we are able to map to every element of ` U_ x e. A B ` .
+       Although it would be possible to work directly with countability
+       expressed as ` F : _om -onto-> ( A |_| 1o ) ` , we instead use functions
+       from subsets of the natural numbers via ~ ctssdccl and ~ ctssdc .
+
+       (Contributed by Jim Kingdon, 31-Oct-2023.) $)
+    ctiunct $p |- ( ph -> E. h h : _om -onto-> ( U_ x e. A B |_| 1o ) ) $=
+      ( vk vn vz vw com cv wfo wex wcel cfv eqid cxp wf1o ciun c1o cdju cen wbr
+      vj vu xpomen ensymi bren mpbi a1i wa wss wdc wral w3a c1st cinl cima crab
+      c2nd ccnv ccom ctssdccl simp1d adantr simp3d simp2d adantlr ctiunctlemuom
+      csb simpr cmpt nfv nfcsb1v nfel2 nfan nfcv nfrabxy nffv ctiunctlemfo omex
+      nfmpt rabex mptex foeq1 spcev ctiunctlemudc wceq sseq1 foeq2 exbidv eleq2
+      syl dcbid ralbidv 3anbi123d syl3anc ctssdc cbvexv bitri sylib exlimddv )
+      ANNNUAZUHOZUBZNBCDUCZUDUEZEOZPZEQZUHXIUHQZANXGUFUGXOXGNUJUKNXGUHULUMUNAXI
+      UOZUIOZNUPZXQXJJOZPZJQZKOZXQRZUQZKNURZUSZUIQZXNXPLOXHSZUTSZMOZFSVACVBRMNV
+      CZRZYHVDSZBYIVAVEZFVFZSZYJGSVADVBRMNVCZVNZRZUOZLNVCZNUPZUUAXJXSPZJQZYBUUA
+      RZUQZKNURZYGXPBLCDYKYQUUAKYOYNGVFZXHAYKNUPZXIAUUIYKCYOPZYBYKRUQKNURZAMCYK
+      KFYOHYKTYOTVGZVHVIZAUUKXIAUUIUUJUUKUULVJVIZAUUJXIAUUIUUJUUKUULVKVIZABOCRZ
+      YQNUPZXIAUUPUOZUUQYQDUUHPZYBYQRUQKNURZUURMDYQKGUUHIYQTUUHTVGZVHVLZAUUPUUT
+      XIUURUUQUUSUUTUVAVJVLZAUUPUUSXIUURUUQUUSUUTUVAVKVLZAXIVOZUUATZVMXPUUAXJKU
+      UAYBXHSZVDSZBUVGUTSYOSZUUHVNZSZVPZPZUUDXPBLCDYKYQUUAKYOUUHUVLXHUUMUUNUUOU
+      VBUVCUVDUVEUVFUVLTBKUUAUVKYTBLNYLYSBYLBVQBYMYRBYPYQVRVSVTBNWAWBZBUVHUVJBU
+      VIUUHVRBUVHWAWCWFUVNWDUUCUVMJUVLKUUAUVKYTLNWEWGZWHUUAXJXSUVLWIWJWQXPBLCDY
+      KYQUUAKYOUUHXHUUMUUNUUOUVBUVCUVDUVEUVFWKYFUUBUUDUUGUSUIUUAUVOXQUUAWLZXRUU
+      BYAUUDYEUUGXQUUANWMUVPXTUUCJXQUUAXJXSWNWOUVPYDUUFKNUVPYCUUEXQUUAYBWPWRWSW
+      TWJXAYGNXKXSPZJQXNXJJKUIXBUVQXMJENXKXSXLWIXCXDXEXF $.
+  $}
+
 
 $(
 ###############################################################################