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

Theorem ctm 6987
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 5398 . . . . . . . . . . 11 ( I ↾ 𝐴):𝐴1-1-onto𝐴
2 f1of 5360 . . . . . . . . . . 11 (( I ↾ 𝐴):𝐴1-1-onto𝐴 → ( I ↾ 𝐴):𝐴𝐴)
31, 2mp1i 10 . . . . . . . . . 10 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → ( I ↾ 𝐴):𝐴𝐴)
4 fconst6g 5316 . . . . . . . . . . 11 (𝑥𝐴 → (1o × {𝑥}):1o𝐴)
54adantr 274 . . . . . . . . . 10 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (1o × {𝑥}):1o𝐴)
63, 5casef 6966 . . . . . . . . 9 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → case(( I ↾ 𝐴), (1o × {𝑥})):(𝐴 ⊔ 1o)⟶𝐴)
7 ffun 5270 . . . . . . . . 9 (case(( I ↾ 𝐴), (1o × {𝑥})):(𝐴 ⊔ 1o)⟶𝐴 → Fun case(( I ↾ 𝐴), (1o × {𝑥})))
86, 7syl 14 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → Fun case(( I ↾ 𝐴), (1o × {𝑥})))
9 vex 2684 . . . . . . . . 9 𝑓 ∈ V
109a1i 9 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → 𝑓 ∈ V)
11 cofunexg 6002 . . . . . . . 8 ((Fun case(( I ↾ 𝐴), (1o × {𝑥})) ∧ 𝑓 ∈ V) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) ∈ V)
128, 10, 11syl2anc 408 . . . . . . 7 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) ∈ V)
13 fof 5340 . . . . . . . . . 10 (𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝑓:ω⟶(𝐴 ⊔ 1o))
1413adantl 275 . . . . . . . . 9 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → 𝑓:ω⟶(𝐴 ⊔ 1o))
15 fco 5283 . . . . . . . . 9 ((case(( I ↾ 𝐴), (1o × {𝑥})):(𝐴 ⊔ 1o)⟶𝐴𝑓:ω⟶(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω⟶𝐴)
166, 14, 15syl2anc 408 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω⟶𝐴)
17 simplr 519 . . . . . . . . . . 11 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → 𝑓:ω–onto→(𝐴 ⊔ 1o))
18 djulcl 6929 . . . . . . . . . . . 12 (𝑦𝐴 → (inl‘𝑦) ∈ (𝐴 ⊔ 1o))
1918adantl 275 . . . . . . . . . . 11 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → (inl‘𝑦) ∈ (𝐴 ⊔ 1o))
20 foelrn 5647 . . . . . . . . . . 11 ((𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ (inl‘𝑦) ∈ (𝐴 ⊔ 1o)) → ∃𝑧 ∈ ω (inl‘𝑦) = (𝑓𝑧))
2117, 19, 20syl2anc 408 . . . . . . . . . 10 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → ∃𝑧 ∈ ω (inl‘𝑦) = (𝑓𝑧))
22 fofn 5342 . . . . . . . . . . . . . . . 16 (𝑓:ω–onto→(𝐴 ⊔ 1o) → 𝑓 Fn ω)
2322ad4antlr 486 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑓 Fn ω)
24 simplr 519 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑧 ∈ ω)
25 fvco2 5483 . . . . . . . . . . . . . . 15 ((𝑓 Fn ω ∧ 𝑧 ∈ ω) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓𝑧)))
2623, 24, 25syl2anc 408 . . . . . . . . . . . . . 14 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓𝑧)))
27 simpr 109 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (inl‘𝑦) = (𝑓𝑧))
2827fveq2d 5418 . . . . . . . . . . . . . 14 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (case(( I ↾ 𝐴), (1o × {𝑥}))‘(inl‘𝑦)) = (case(( I ↾ 𝐴), (1o × {𝑥}))‘(𝑓𝑧)))
29 fnresi 5235 . . . . . . . . . . . . . . . 16 ( I ↾ 𝐴) Fn 𝐴
3029a1i 9 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → ( I ↾ 𝐴) Fn 𝐴)
31 vex 2684 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
3231fconst6 5317 . . . . . . . . . . . . . . . 16 (1o × {𝑥}):1o⟶V
33 ffun 5270 . . . . . . . . . . . . . . . 16 ((1o × {𝑥}):1o⟶V → Fun (1o × {𝑥}))
3432, 33mp1i 10 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → Fun (1o × {𝑥}))
35 simpllr 523 . . . . . . . . . . . . . . 15 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑦𝐴)
3630, 34, 35caseinl 6969 . . . . . . . . . . . . . 14 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (case(( I ↾ 𝐴), (1o × {𝑥}))‘(inl‘𝑦)) = (( I ↾ 𝐴)‘𝑦))
3726, 28, 363eqtr2d 2176 . . . . . . . . . . . . 13 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧) = (( I ↾ 𝐴)‘𝑦))
38 fvresi 5606 . . . . . . . . . . . . . 14 (𝑦𝐴 → (( I ↾ 𝐴)‘𝑦) = 𝑦)
3935, 38syl 14 . . . . . . . . . . . . 13 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → (( I ↾ 𝐴)‘𝑦) = 𝑦)
4037, 39eqtr2d 2171 . . . . . . . . . . . 12 (((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) ∧ (inl‘𝑦) = (𝑓𝑧)) → 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))
4140ex 114 . . . . . . . . . . 11 ((((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) ∧ 𝑧 ∈ ω) → ((inl‘𝑦) = (𝑓𝑧) → 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)))
4241reximdva 2532 . . . . . . . . . 10 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → (∃𝑧 ∈ ω (inl‘𝑦) = (𝑓𝑧) → ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)))
4321, 42mpd 13 . . . . . . . . 9 (((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) ∧ 𝑦𝐴) → ∃𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))
4443ralrimiva 2503 . . . . . . . 8 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → ∀𝑦𝐴𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧))
45 dffo3 5560 . . . . . . . 8 ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto𝐴 ↔ ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω⟶𝐴 ∧ ∀𝑦𝐴𝑧 ∈ ω 𝑦 = ((case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓)‘𝑧)))
4616, 44, 45sylanbrc 413 . . . . . . 7 ((𝑥𝐴𝑓:ω–onto→(𝐴 ⊔ 1o)) → (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto𝐴)
47 foeq1 5336 . . . . . . . 8 (𝑔 = (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓) → (𝑔:ω–onto𝐴 ↔ (case(( I ↾ 𝐴), (1o × {𝑥})) ∘ 𝑓):ω–onto𝐴))
4847spcegv 2769 . . . . . . 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 1577 . . . 4 (∃𝑥 𝑥𝐴 → (𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto𝐴))
5251exlimdv 1791 . . 3 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto𝐴))
53 foeq1 5336 . . . 4 (𝑓 = 𝑔 → (𝑓:ω–onto𝐴𝑔:ω–onto𝐴))
5453cbvexv 1890 . . 3 (∃𝑓 𝑓:ω–onto𝐴 ↔ ∃𝑔 𝑔:ω–onto𝐴)
5552, 54syl6ibr 161 . 2 (∃𝑥 𝑥𝐴 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑓 𝑓:ω–onto𝐴))
56 ctmlemr 6986 . 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 1331  wex 1468  wcel 1480  wral 2414  wrex 2415  Vcvv 2681  {csn 3522   I cid 4205  ωcom 4499   × cxp 4532  cres 4536  ccom 4538  Fun wfun 5112   Fn wfn 5113  wf 5114  ontowfo 5116  1-1-ontowf1o 5117  cfv 5118  1oc1o 6299  cdju 6915  inlcinl 6923  casecdjucase 6961
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-iinf 4497
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-ral 2419  df-rex 2420  df-reu 2421  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-if 3470  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-tr 4022  df-id 4210  df-iord 4283  df-on 4285  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-1st 6031  df-2nd 6032  df-1o 6306  df-dju 6916  df-inl 6925  df-inr 6926  df-case 6962
This theorem is referenced by:  ctssdc  6991  enumct  6993  omct  6995
  Copyright terms: Public domain W3C validator