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

Theorem ctm 6871
Description: Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
Assertion
Ref Expression
ctm (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto𝐴))
Distinct variable group:   𝐴,𝑓,𝑥

Proof of Theorem ctm
Dummy variables 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oi 5326 . . . . . . . . . . 11 ( I ↾ 𝐴):𝐴1-1-onto𝐴
2 f1of 5288 . . . . . . . . . . 11 (( I ↾ 𝐴):𝐴1-1-onto𝐴 → ( I ↾ 𝐴):𝐴𝐴)
31, 2mp1i 10 . . . . . . . . . 10 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → ( I ↾ 𝐴):𝐴𝐴)
4 fconst6g 5244 . . . . . . . . . . 11 (𝑥𝐴 → (1o × {𝑥}):1o𝐴)
54adantr 271 . . . . . . . . . 10 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (1o × {𝑥}):1o𝐴)
63, 5casef 6859 . . . . . . . . 9 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → case(( I ↾ 𝐴), (1o × {𝑥})):(𝐴 ⊔ 1o)⟶𝐴)
7 ffun 5198 . . . . . . . . 9 (case(( I ↾ 𝐴), (1o × {𝑥})):(𝐴 ⊔ 1o)⟶𝐴 → Fun case(( I ↾ 𝐴), (1o × {𝑥})))
86, 7syl 14 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → Fun case(( I ↾ 𝐴), (1o × {𝑥})))
9 vex 2636 . . . . . . . . 9 𝑓 ∈ V
109a1i 9 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → 𝑓 ∈ V)
11 cofunexg 5920 . . . . . . . 8 ((Fun case(( I ↾ 𝐴), (1o × {𝑥})) ∧ 𝑓 ∈ V) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) ∈ V)
128, 10, 11syl2anc 404 . . . . . . 7 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) ∈ V)
13 fof 5268 . . . . . . . . . 10 (𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝑓:ω⟶(𝐴 ⊔ 1o))
1413adantl 272 . . . . . . . . 9 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → 𝑓:ω⟶(𝐴 ⊔ 1o))
15 fco 5211 . . . . . . . . 9 ((case(( I ↾ 𝐴), (1o × {𝑥})):(𝐴 ⊔ 1o)⟶𝐴𝑓:ω⟶(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω⟶𝐴)
166, 14, 15syl2anc 404 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω⟶𝐴)
17 simplr 498 . . . . . . . . . . 11 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → 𝑓:ω–onto→(𝐴 ⊔ 1o))
18 djulcl 6823 . . . . . . . . . . . 12 (𝑦𝐴 → (inl‘𝑦) ∈ (𝐴 ⊔ 1o))
1918adantl 272 . . . . . . . . . . 11 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → (inl‘𝑦) ∈ (𝐴 ⊔ 1o))
20 foelrn 5570 . . . . . . . . . . 11 ((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ (inl‘𝑦) ∈ (𝐴 ⊔ 1o)) → ∃𝑧 ∈ ω (inl‘𝑦) = (𝑓𝑧))
2117, 19, 20syl2anc 404 . . . . . . . . . 10 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → ∃𝑧 ∈ ω (inl‘𝑦) = (𝑓𝑧))
22 fofn 5270 . . . . . . . . . . . . . . . 16 (𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝑓 Fn ω)
2322ad4antlr 480 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑓 Fn ω)
24 simplr 498 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑧 ∈ ω)
25 fvco2 5408 . . . . . . . . . . . . . . 15 ((𝑓 Fn ω ∧ 𝑧 ∈ ω) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓𝑧)))
2623, 24, 25syl2anc 404 . . . . . . . . . . . . . 14 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓𝑧)))
27 simpr 109 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (inl‘𝑦) = (𝑓𝑧))
2827fveq2d 5344 . . . . . . . . . . . . . 14 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (case(( I ↾ 𝐴), (1o × {𝑥}))‘(inl‘𝑦)) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓𝑧)))
29 fnresi 5165 . . . . . . . . . . . . . . . 16 ( I ↾ 𝐴) Fn 𝐴
3029a1i 9 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → ( I ↾ 𝐴) Fn 𝐴)
31 vex 2636 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
3231fconst6 5245 . . . . . . . . . . . . . . . 16 (1o × {𝑥}):1o⟶V
33 ffun 5198 . . . . . . . . . . . . . . . 16 ((1o × {𝑥}):1o⟶V → Fun (1o × {𝑥}))
3432, 33mp1i 10 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → Fun (1o × {𝑥}))
35 simpllr 502 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑦𝐴)
3630, 34, 35caseinl 6862 . . . . . . . . . . . . . 14 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (case(( I ↾ 𝐴), (1o × {𝑥}))‘(inl‘𝑦)) = (( I ↾ 𝐴)‘𝑦))
3726, 28, 363eqtr2d 2133 . . . . . . . . . . . . 13 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (( I ↾ 𝐴)‘𝑦))
38 fvresi 5529 . . . . . . . . . . . . . 14 (𝑦𝐴 → (( I ↾ 𝐴)‘𝑦) = 𝑦)
3935, 38syl 14 . . . . . . . . . . . . 13 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (( I ↾ 𝐴)‘𝑦) = 𝑦)
4037, 39eqtr2d 2128 . . . . . . . . . . . 12 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))
4140ex 114 . . . . . . . . . . 11 ((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) → ((inl‘𝑦) = (𝑓𝑧) → 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)))
4241reximdva 2487 . . . . . . . . . 10 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → (∃𝑧 ∈ ω (inl‘𝑦) = (𝑓𝑧) → ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)))
4321, 42mpd 13 . . . . . . . . 9 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))
4443ralrimiva 2458 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → ∀𝑦𝐴𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))
45 dffo3 5485 . . . . . . . 8 ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto𝐴 ↔ ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω⟶𝐴 ∧ ∀𝑦𝐴𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)))
4616, 44, 45sylanbrc 409 . . . . . . 7 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto𝐴)
47 foeq1 5264 . . . . . . . 8 (𝑔 = (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) → (𝑔:ω–onto𝐴 ↔ (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto𝐴))
4847spcegv 2721 . . . . . . 7 ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) ∈ V → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto𝐴 → ∃𝑔 𝑔:ω–onto𝐴))
4912, 46, 48sylc 62 . . . . . 6 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → ∃𝑔 𝑔:ω–onto𝐴)
5049ex 114 . . . . 5 (𝑥𝐴 → (𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto𝐴))
5150exlimiv 1541 . . . 4 (∃𝑥 𝑥𝐴 → (𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto𝐴))
5251exlimdv 1754 . . 3 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto𝐴))
53 foeq1 5264 . . . 4 (𝑓 = 𝑔 → (𝑓:ω–onto𝐴𝑔:ω–onto𝐴))
5453cbvexv 1850 . . 3 (∃𝑓 𝑓:ω–onto𝐴 ↔ ∃𝑔 𝑔:ω–onto𝐴)
5552, 54syl6ibr 161 . 2 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑓 𝑓:ω–onto𝐴))
56 ctmlemr 6870 . 2 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)))
5755, 56impbid 128 1 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104   = wceq 1296  wex 1433  wcel 1445  wral 2370  wrex 2371  Vcvv 2633  {csn 3466   I cid 4139  ωcom 4433   × cxp 4465  cres 4469  ccom 4471  Fun wfun 5043   Fn wfn 5044  wf 5045  ontowfo 5047  1-1-ontowf1o 5048  cfv 5049  1oc1o 6212  cdju 6810  inlcinl 6817  casecdjucase 6854
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-coll 3975  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-iinf 4431
This theorem depends on definitions:  df-bi 116  df-dc 784  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-if 3414  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-tr 3959  df-id 4144  df-iord 4217  df-on 4219  df-suc 4222  df-iom 4434  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056  df-fv 5057  df-1st 5949  df-2nd 5950  df-1o 6219  df-dju 6811  df-inl 6819  df-inr 6820  df-case 6855
This theorem is referenced by:  enumct  6873
  Copyright terms: Public domain W3C validator