Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ctssdccl Unicode version

Theorem ctssdccl 7041
 Description: A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7043 but expressed in terms of classes rather than . (Contributed by Jim Kingdon, 30-Oct-2023.)
Hypotheses
Ref Expression
ctssdccl.f
ctssdccl.s inl
ctssdccl.g inl
Assertion
Ref Expression
ctssdccl DECID
Distinct variable groups:   ,   ,,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem ctssdccl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ctssdccl.s . . . 4 inl
2 ssrab2 3209 . . . 4 inl
31, 2eqsstri 3156 . . 3
43a1i 9 . 2
5 djulf1o 6988 . . . . . . 7 inl
6 f1ocnv 5420 . . . . . . 7 inl inl
7 f1ofun 5409 . . . . . . 7 inl inl
85, 6, 7mp2b 8 . . . . . 6 inl
9 ctssdccl.f . . . . . . 7
10 fofun 5386 . . . . . . 7
119, 10syl 14 . . . . . 6
12 funco 5203 . . . . . . 7 inl inl
13 ctssdccl.g . . . . . . . 8 inl
1413funeqi 5184 . . . . . . 7 inl
1512, 14sylibr 133 . . . . . 6 inl
168, 11, 15sylancr 411 . . . . 5
17 fof 5385 . . . . . . . . . . . 12
189, 17syl 14 . . . . . . . . . . 11
1918fdmd 5319 . . . . . . . . . 10
2019eleq2d 2224 . . . . . . . . 9
2120anbi1d 461 . . . . . . . 8 inl inl
22 dmcoss 4848 . . . . . . . . . . . 12 inl
2322sseli 3120 . . . . . . . . . . 11 inl
2423pm4.71ri 390 . . . . . . . . . 10 inl inl
25 dmfco 5529 . . . . . . . . . . 11 inl inl
2625pm5.32da 448 . . . . . . . . . 10 inl inl
2724, 26syl5bb 191 . . . . . . . . 9 inl inl
2811, 27syl 14 . . . . . . . 8 inl inl
29 simpr 109 . . . . . . . . . . 11 inl inl
30 imassrn 4932 . . . . . . . . . . . . . 14 inl inl
3130sseli 3120 . . . . . . . . . . . . 13 inl inl
3231adantl 275 . . . . . . . . . . . 12 inl inl
33 df-rn 4590 . . . . . . . . . . . . 13 inl inl
3433eleq2i 2221 . . . . . . . . . . . 12 inl inl
3532, 34sylib 121 . . . . . . . . . . 11 inl inl
3629, 352thd 174 . . . . . . . . . 10 inl inl inl
37 djuin 6994 . . . . . . . . . . . . . 14 inl inr
38 disjel 3444 . . . . . . . . . . . . . 14 inl inr inl inr
3937, 38mpan 421 . . . . . . . . . . . . 13 inl inr
4039con2i 617 . . . . . . . . . . . 12 inr inl
4140adantl 275 . . . . . . . . . . 11 inr inl
42 djuin 6994 . . . . . . . . . . . . . . . 16 inl inr
43 disjel 3444 . . . . . . . . . . . . . . . 16 inl inr inl inr
4442, 43mpan 421 . . . . . . . . . . . . . . 15 inl inr
45 dfrn4 5039 . . . . . . . . . . . . . . 15 inl inl
4644, 45eleq2s 2249 . . . . . . . . . . . . . 14 inl inr
4746con2i 617 . . . . . . . . . . . . 13 inr inl
4847adantl 275 . . . . . . . . . . . 12 inr inl
4948, 34sylnib 666 . . . . . . . . . . 11 inr inl
5041, 492falsed 692 . . . . . . . . . 10 inr inl inl
5118ffvelrnda 5595 . . . . . . . . . . . 12
52 djuun 6997 . . . . . . . . . . . . 13 inl inr
5352eleq2i 2221 . . . . . . . . . . . 12 inl inr
5451, 53sylibr 133 . . . . . . . . . . 11 inl inr
55 elun 3244 . . . . . . . . . . 11 inl inr inl inr
5654, 55sylib 121 . . . . . . . . . 10 inl inr
5736, 50, 56mpjaodan 788 . . . . . . . . 9 inl inl
5857pm5.32da 448 . . . . . . . 8 inl inl
5921, 28, 583bitr4d 219 . . . . . . 7 inl inl
6013dmeqi 4780 . . . . . . . 8 inl
6160eleq2i 2221 . . . . . . 7 inl
62 fveq2 5461 . . . . . . . . 9
6362eleq1d 2223 . . . . . . . 8 inl inl
6463, 1elrab2 2867 . . . . . . 7 inl
6559, 61, 643bitr4g 222 . . . . . 6
6665eqrdv 2152 . . . . 5
67 df-fn 5166 . . . . 5
6816, 66, 67sylanbrc 414 . . . 4
6913fveq1i 5462 . . . . . . 7 inl
7018adantr 274 . . . . . . . 8
71 fveq2 5461 . . . . . . . . . . . . 13
7271eleq1d 2223 . . . . . . . . . . . 12 inl inl
7372, 1elrab2 2867 . . . . . . . . . . 11 inl
7473biimpi 119 . . . . . . . . . 10 inl
7574adantl 275 . . . . . . . . 9 inl
7675simpld 111 . . . . . . . 8
77 fvco3 5532 . . . . . . . 8 inl inl
7870, 76, 77syl2anc 409 . . . . . . 7 inl inl
7969, 78syl5eq 2199 . . . . . 6 inl
80 f1ofun 5409 . . . . . . . . . 10 inl inl
815, 80ax-mp 5 . . . . . . . . 9 inl
82 fvelima 5513 . . . . . . . . 9 inl inl inl
8381, 82mpan 421 . . . . . . . 8 inl inl
8475, 83simpl2im 384 . . . . . . 7 inl
85 simprr 522 . . . . . . . . 9 inl inl
8685fveq2d 5465 . . . . . . . 8 inl inlinl inl
87 vex 2712 . . . . . . . . . 10
88 f1ocnvfv1 5718 . . . . . . . . . 10 inl inlinl
895, 87, 88mp2an 423 . . . . . . . . 9 inlinl
90 simprl 521 . . . . . . . . 9 inl
9189, 90eqeltrid 2241 . . . . . . . 8 inl inlinl
9286, 91eqeltrrd 2232 . . . . . . 7 inl inl
9384, 92rexlimddv 2576 . . . . . 6 inl
9479, 93eqeltrd 2231 . . . . 5
9594ralrimiva 2527 . . . 4
96 ffnfv 5618 . . . 4
9768, 95, 96sylanbrc 414 . . 3
98 djulcl 6981 . . . . . . . 8 inl
99 foelrn 5694 . . . . . . . . . 10 inl inl
1009, 99sylan 281 . . . . . . . . 9 inl inl
101 df-rex 2438 . . . . . . . . 9 inl inl
102100, 101sylib 121 . . . . . . . 8 inl inl
10398, 102sylan2 284 . . . . . . 7 inl
104 fveq2 5461 . . . . . . . . . . . . 13
105104eleq1d 2223 . . . . . . . . . . . 12 inl inl
106 simprl 521 . . . . . . . . . . . 12 inl
107 simprr 522 . . . . . . . . . . . . 13 inl inl
108 vex 2712 . . . . . . . . . . . . . . . 16
109 f1odm 5411 . . . . . . . . . . . . . . . . 17 inl inl
1105, 109ax-mp 5 . . . . . . . . . . . . . . . 16 inl
111108, 110eleqtrri 2230 . . . . . . . . . . . . . . 15 inl
112 funfvima 5689 . . . . . . . . . . . . . . 15 inl inl inl inl
11381, 111, 112mp2an 423 . . . . . . . . . . . . . 14 inl inl
114113ad2antlr 481 . . . . . . . . . . . . 13 inl inl inl
115107, 114eqeltrrd 2232 . . . . . . . . . . . 12 inl inl
116105, 106, 115elrabd 2866 . . . . . . . . . . 11 inl inl
117116, 1eleqtrrdi 2248 . . . . . . . . . 10 inl
118117, 107jca 304 . . . . . . . . 9 inl inl
119118ex 114 . . . . . . . 8 inl inl
120119eximdv 1857 . . . . . . 7 inl inl
121103, 120mpd 13 . . . . . 6 inl
122 df-rex 2438 . . . . . 6 inl inl
123121, 122sylibr 133 . . . . 5 inl
124 f1ocnvfv1 5718 . . . . . . . . . 10 inl inlinl
1255, 108, 124mp2an 423 . . . . . . . . 9 inlinl
126 simpr 109 . . . . . . . . . 10 inl inl
127126fveq2d 5465 . . . . . . . . 9 inl inlinl inl
128125, 127syl5eqr 2201 . . . . . . . 8 inl inl
12913fveq1i 5462 . . . . . . . . . 10 inl
13018ad2antrr 480 . . . . . . . . . . 11
1313sseli 3120 . . . . . . . . . . . 12
132131adantl 275 . . . . . . . . . . 11
133 fvco3 5532 . . . . . . . . . . 11 inl inl
134130, 132, 133syl2anc 409 . . . . . . . . . 10 inl inl
135129, 134syl5eq 2199 . . . . . . . . 9 inl
136135adantr 274 . . . . . . . 8 inl inl
137128, 136eqtr4d 2190 . . . . . . 7 inl
138137ex 114 . . . . . 6 inl
139138reximdva 2556 . . . . 5 inl
140123, 139mpd 13 . . . 4
141140ralrimiva 2527 . . 3
142 dffo3 5607 . . 3
14397, 141, 142sylanbrc 414 . 2
14453, 55bitr3i 185 . . . . . . 7 inl inr
14551, 144sylib 121 . . . . . 6 inl inr
14640orim2i 751 . . . . . 6 inl inr inl inl
147145, 146syl 14 . . . . 5 inl inl
148 df-dc 821 . . . . 5 DECID inl inl inl
149147, 148sylibr 133 . . . 4 DECID inl
150 ibar 299 . . . . . . 7 inl inl
151150adantl 275 . . . . . 6 inl inl
152151, 64bitr4di 197 . . . . 5 inl
153152dcbid 824 . . . 4 DECID inl DECID
154149, 153mpbid 146 . . 3 DECID
155154ralrimiva 2527 . 2 DECID
1564, 143, 1553jca 1162 1 DECID
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   wo 698  DECID wdc 820   w3a 963   wceq 1332  wex 1469   wcel 2125  wral 2432  wrex 2433  crab 2436  cvv 2709   cun 3096   cin 3097   wss 3098  c0 3390  csn 3556  com 4543   cxp 4577  ccnv 4578   cdm 4579   crn 4580  cima 4582   ccom 4583   wfun 5157   wfn 5158  wf 5159  wfo 5161  wf1o 5162  cfv 5163  c1o 6346   ⊔ cdju 6967  inlcinl 6975  inrcinr 6976 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-ral 2437  df-rex 2438  df-rab 2441  df-v 2711  df-sbc 2934  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-iord 4321  df-on 4323  df-suc 4326  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-1st 6078  df-2nd 6079  df-1o 6353  df-dju 6968  df-inl 6977  df-inr 6978 This theorem is referenced by:  ctssdclemr  7042  ctiunct  12120
 Copyright terms: Public domain W3C validator