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

Theorem enumct 7000
 Description: A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as ∃𝑛 ∈ ω∃𝑓𝑓:𝑛–onto→𝐴 per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as ∃𝑔𝑔:ω–onto→(𝐴 ⊔ 1o) per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
Assertion
Ref Expression
enumct (∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
Distinct variable group:   𝐴,𝑓,𝑔,𝑛

Proof of Theorem enumct
Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 518 . . . . . . . . 9 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ 𝑛 = ∅) → 𝑓:𝑛onto𝐴)
2 foeq2 5342 . . . . . . . . . 10 (𝑛 = ∅ → (𝑓:𝑛onto𝐴𝑓:∅–onto𝐴))
32adantl 275 . . . . . . . . 9 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ 𝑛 = ∅) → (𝑓:𝑛onto𝐴𝑓:∅–onto𝐴))
41, 3mpbid 146 . . . . . . . 8 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ 𝑛 = ∅) → 𝑓:∅–onto𝐴)
5 fo00 5403 . . . . . . . 8 (𝑓:∅–onto𝐴 ↔ (𝑓 = ∅ ∧ 𝐴 = ∅))
64, 5sylib 121 . . . . . . 7 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ 𝑛 = ∅) → (𝑓 = ∅ ∧ 𝐴 = ∅))
7 0ct 6992 . . . . . . . 8 𝑔 𝑔:ω–onto→(∅ ⊔ 1o)
8 djueq1 6925 . . . . . . . . . 10 (𝐴 = ∅ → (𝐴 ⊔ 1o) = (∅ ⊔ 1o))
9 foeq3 5343 . . . . . . . . . 10 ((𝐴 ⊔ 1o) = (∅ ⊔ 1o) → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(∅ ⊔ 1o)))
108, 9syl 14 . . . . . . . . 9 (𝐴 = ∅ → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(∅ ⊔ 1o)))
1110exbidv 1797 . . . . . . . 8 (𝐴 = ∅ → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(∅ ⊔ 1o)))
127, 11mpbiri 167 . . . . . . 7 (𝐴 = ∅ → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
136, 12simpl2im 383 . . . . . 6 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ 𝑛 = ∅) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
14 omex 4507 . . . . . . . . 9 ω ∈ V
1514mptex 5646 . . . . . . . 8 (𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅))) ∈ V
16 simpll 518 . . . . . . . . 9 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑓:𝑛onto𝐴)
17 simplr 519 . . . . . . . . 9 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑛 ∈ ω)
18 simpr 109 . . . . . . . . 9 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∅ ∈ 𝑛)
19 eqid 2139 . . . . . . . . 9 (𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅))) = (𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅)))
2016, 17, 18, 19enumctlemm 6999 . . . . . . . 8 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅))):ω–onto𝐴)
21 foeq1 5341 . . . . . . . . 9 (𝑔 = (𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅))) → (𝑔:ω–onto𝐴 ↔ (𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅))):ω–onto𝐴))
2221spcegv 2774 . . . . . . . 8 ((𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅))) ∈ V → ((𝑘 ∈ ω ↦ if(𝑘𝑛, (𝑓𝑘), (𝑓‘∅))):ω–onto𝐴 → ∃𝑔 𝑔:ω–onto𝐴))
2315, 20, 22mpsyl 65 . . . . . . 7 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑔 𝑔:ω–onto𝐴)
24 fof 5345 . . . . . . . . . . 11 (𝑓:𝑛onto𝐴𝑓:𝑛𝐴)
2524ad2antrr 479 . . . . . . . . . 10 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑓:𝑛𝐴)
2625, 18ffvelrnd 5556 . . . . . . . . 9 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (𝑓‘∅) ∈ 𝐴)
27 eleq1 2202 . . . . . . . . . 10 (𝑥 = (𝑓‘∅) → (𝑥𝐴 ↔ (𝑓‘∅) ∈ 𝐴))
2827spcegv 2774 . . . . . . . . 9 ((𝑓‘∅) ∈ 𝐴 → ((𝑓‘∅) ∈ 𝐴 → ∃𝑥 𝑥𝐴))
2926, 26, 28sylc 62 . . . . . . . 8 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑥 𝑥𝐴)
30 ctm 6994 . . . . . . . 8 (∃𝑥 𝑥𝐴 → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto𝐴))
3129, 30syl 14 . . . . . . 7 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto𝐴))
3223, 31mpbird 166 . . . . . 6 (((𝑓:𝑛onto𝐴𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
33 0elnn 4532 . . . . . . 7 (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∅ ∈ 𝑛))
3433adantl 275 . . . . . 6 ((𝑓:𝑛onto𝐴𝑛 ∈ ω) → (𝑛 = ∅ ∨ ∅ ∈ 𝑛))
3513, 32, 34mpjaodan 787 . . . . 5 ((𝑓:𝑛onto𝐴𝑛 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
3635ex 114 . . . 4 (𝑓:𝑛onto𝐴 → (𝑛 ∈ ω → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
3736exlimiv 1577 . . 3 (∃𝑓 𝑓:𝑛onto𝐴 → (𝑛 ∈ ω → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
3837impcom 124 . 2 ((𝑛 ∈ ω ∧ ∃𝑓 𝑓:𝑛onto𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
3938rexlimiva 2544 1 (∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∃wrex 2417  Vcvv 2686  ∅c0 3363  ifcif 3474   ↦ cmpt 3989  ωcom 4504  ⟶wf 5119  –onto→wfo 5121  ‘cfv 5123  1oc1o 6306   ⊔ cdju 6922 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 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-1st 6038  df-2nd 6039  df-1o 6313  df-dju 6923  df-inl 6932  df-inr 6933  df-case 6969 This theorem is referenced by:  finct  7001
 Copyright terms: Public domain W3C validator