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

Theorem ctssdc 7011
 Description: A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 7037. (Contributed by Jim Kingdon, 15-Aug-2023.)
Assertion
Ref Expression
ctssdc (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
Distinct variable group:   𝐴,𝑓,𝑠,𝑛

Proof of Theorem ctssdc
Dummy variables 𝑔 𝑚 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 984 . . . . . . . . . . . . . . . . . 18 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) → 𝑓:𝑠onto𝐴)
2 fof 5355 . . . . . . . . . . . . . . . . . 18 (𝑓:𝑠onto𝐴𝑓:𝑠𝐴)
31, 2syl 14 . . . . . . . . . . . . . . . . 17 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) → 𝑓:𝑠𝐴)
43ad3antrrr 484 . . . . . . . . . . . . . . . 16 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) ∧ 𝑚𝑠) → 𝑓:𝑠𝐴)
5 simpr 109 . . . . . . . . . . . . . . . 16 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) ∧ 𝑚𝑠) → 𝑚𝑠)
64, 5ffvelrnd 5566 . . . . . . . . . . . . . . 15 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) ∧ 𝑚𝑠) → (𝑓𝑚) ∈ 𝐴)
73ad3antrrr 484 . . . . . . . . . . . . . . . 16 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) ∧ ¬ 𝑚𝑠) → 𝑓:𝑠𝐴)
8 simpllr 524 . . . . . . . . . . . . . . . 16 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) ∧ ¬ 𝑚𝑠) → ∅ ∈ 𝑠)
97, 8ffvelrnd 5566 . . . . . . . . . . . . . . 15 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) ∧ ¬ 𝑚𝑠) → (𝑓‘∅) ∈ 𝐴)
10 elequ1 1691 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (𝑛𝑠𝑚𝑠))
1110dcbid 824 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → (DECID 𝑛𝑠DECID 𝑚𝑠))
12 simpll2 1022 . . . . . . . . . . . . . . . 16 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) → ∀𝑛 ∈ ω DECID 𝑛𝑠)
13 simpr 109 . . . . . . . . . . . . . . . 16 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) → 𝑚 ∈ ω)
1411, 12, 13rspcdva 2799 . . . . . . . . . . . . . . 15 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) → DECID 𝑚𝑠)
156, 9, 14ifcldadc 3507 . . . . . . . . . . . . . 14 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑚 ∈ ω) → if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)) ∈ 𝐴)
1615fmpttd 5585 . . . . . . . . . . . . 13 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))):ω⟶𝐴)
1716ffnd 5283 . . . . . . . . . . . 12 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) Fn ω)
18 fvelrnb 5479 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) Fn ω → (𝑦 ∈ ran (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) ↔ ∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
1917, 18syl 14 . . . . . . . . . . . . . 14 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑦 ∈ ran (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) ↔ ∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
201ad2antrr 480 . . . . . . . . . . . . . . . . . 18 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) → 𝑓:𝑠onto𝐴)
21 foelrn 5664 . . . . . . . . . . . . . . . . . 18 ((𝑓:𝑠onto𝐴𝑦𝐴) → ∃𝑧𝑠 𝑦 = (𝑓𝑧))
2220, 21sylancom 417 . . . . . . . . . . . . . . . . 17 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) → ∃𝑧𝑠 𝑦 = (𝑓𝑧))
23 simpll1 1021 . . . . . . . . . . . . . . . . . 18 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) → 𝑠 ⊆ ω)
24 eqid 2140 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) = (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))
25 elequ1 1691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑧 → (𝑚𝑠𝑧𝑠))
26 fveq2 5431 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = 𝑧 → (𝑓𝑚) = (𝑓𝑧))
2725, 26ifbieq1d 3500 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = 𝑧 → if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)) = if(𝑧𝑠, (𝑓𝑧), (𝑓‘∅)))
2823sselda 3103 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → 𝑧 ∈ ω)
293ad4antr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) ∧ 𝑧𝑠) → 𝑓:𝑠𝐴)
30 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) ∧ 𝑧𝑠) → 𝑧𝑠)
3129, 30ffvelrnd 5566 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) ∧ 𝑧𝑠) → (𝑓𝑧) ∈ 𝐴)
323ffvelrnda 5565 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑓‘∅) ∈ 𝐴)
3332ad3antrrr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) ∧ ¬ 𝑧𝑠) → (𝑓‘∅) ∈ 𝐴)
34 elequ1 1691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑧 → (𝑛𝑠𝑧𝑠))
3534dcbid 824 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑧 → (DECID 𝑛𝑠DECID 𝑧𝑠))
36 simp2 983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑠)
3736ad3antrrr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → ∀𝑛 ∈ ω DECID 𝑛𝑠)
3835, 37, 28rspcdva 2799 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → DECID 𝑧𝑠)
3931, 33, 38ifcldadc 3507 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → if(𝑧𝑠, (𝑓𝑧), (𝑓‘∅)) ∈ 𝐴)
4024, 27, 28, 39fvmptd3 5524 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = if(𝑧𝑠, (𝑓𝑧), (𝑓‘∅)))
41 simpr 109 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → 𝑧𝑠)
4241iftrued 3487 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → if(𝑧𝑠, (𝑓𝑧), (𝑓‘∅)) = (𝑓𝑧))
4340, 42eqtrd 2173 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = (𝑓𝑧))
4443adantr 274 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) ∧ 𝑦 = (𝑓𝑧)) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = (𝑓𝑧))
45 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) ∧ 𝑦 = (𝑓𝑧)) → 𝑦 = (𝑓𝑧))
4644, 45eqtr4d 2176 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) ∧ 𝑦 = (𝑓𝑧)) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦)
4746ex 114 . . . . . . . . . . . . . . . . . . 19 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) ∧ 𝑧𝑠) → (𝑦 = (𝑓𝑧) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
4847reximdva 2538 . . . . . . . . . . . . . . . . . 18 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) → (∃𝑧𝑠 𝑦 = (𝑓𝑧) → ∃𝑧𝑠 ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
49 ssrexv 3168 . . . . . . . . . . . . . . . . . 18 (𝑠 ⊆ ω → (∃𝑧𝑠 ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦 → ∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
5023, 48, 49sylsyld 58 . . . . . . . . . . . . . . . . 17 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) → (∃𝑧𝑠 𝑦 = (𝑓𝑧) → ∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
5122, 50mpd 13 . . . . . . . . . . . . . . . 16 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑦𝐴) → ∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦)
5251ex 114 . . . . . . . . . . . . . . 15 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑦𝐴 → ∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
53 simpr 109 . . . . . . . . . . . . . . . . 17 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) ∧ ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦)
54 simpr 109 . . . . . . . . . . . . . . . . . . . 20 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) → 𝑧 ∈ ω)
553ad3antrrr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) ∧ 𝑧𝑠) → 𝑓:𝑠𝐴)
56 simpr 109 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) ∧ 𝑧𝑠) → 𝑧𝑠)
5755, 56ffvelrnd 5566 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) ∧ 𝑧𝑠) → (𝑓𝑧) ∈ 𝐴)
5832ad2antrr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) ∧ ¬ 𝑧𝑠) → (𝑓‘∅) ∈ 𝐴)
59 simpll2 1022 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) → ∀𝑛 ∈ ω DECID 𝑛𝑠)
6035, 59, 54rspcdva 2799 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) → DECID 𝑧𝑠)
6157, 58, 60ifcldadc 3507 . . . . . . . . . . . . . . . . . . . 20 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) → if(𝑧𝑠, (𝑓𝑧), (𝑓‘∅)) ∈ 𝐴)
6224, 27, 54, 61fvmptd3 5524 . . . . . . . . . . . . . . . . . . 19 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = if(𝑧𝑠, (𝑓𝑧), (𝑓‘∅)))
6362, 61eqeltrd 2217 . . . . . . . . . . . . . . . . . 18 ((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) ∈ 𝐴)
6463adantr 274 . . . . . . . . . . . . . . . . 17 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) ∧ ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦) → ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) ∈ 𝐴)
6553, 64eqeltrrd 2218 . . . . . . . . . . . . . . . 16 (((((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) ∧ 𝑧 ∈ ω) ∧ ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦) → 𝑦𝐴)
6665rexlimdva2 2556 . . . . . . . . . . . . . . 15 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦𝑦𝐴))
6752, 66impbid 128 . . . . . . . . . . . . . 14 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑦𝐴 ↔ ∃𝑧 ∈ ω ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅)))‘𝑧) = 𝑦))
6819, 67bitr4d 190 . . . . . . . . . . . . 13 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑦 ∈ ran (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) ↔ 𝑦𝐴))
6968eqrdv 2138 . . . . . . . . . . . 12 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → ran (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) = 𝐴)
70 df-fo 5139 . . . . . . . . . . . 12 ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))):ω–onto𝐴 ↔ ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) Fn ω ∧ ran (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) = 𝐴))
7117, 69, 70sylanbrc 414 . . . . . . . . . . 11 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))):ω–onto𝐴)
72 omex 4516 . . . . . . . . . . . . 13 ω ∈ V
7372mptex 5656 . . . . . . . . . . . 12 (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) ∈ V
74 foeq1 5351 . . . . . . . . . . . 12 (𝑔 = (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))) → (𝑔:ω–onto𝐴 ↔ (𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))):ω–onto𝐴))
7573, 74spcev 2785 . . . . . . . . . . 11 ((𝑚 ∈ ω ↦ if(𝑚𝑠, (𝑓𝑚), (𝑓‘∅))):ω–onto𝐴 → ∃𝑔 𝑔:ω–onto𝐴)
7671, 75syl 14 . . . . . . . . . 10 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → ∃𝑔 𝑔:ω–onto𝐴)
77 elex2 2706 . . . . . . . . . . . 12 ((𝑓‘∅) ∈ 𝐴 → ∃𝑥 𝑥𝐴)
7832, 77syl 14 . . . . . . . . . . 11 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → ∃𝑥 𝑥𝐴)
79 ctm 7007 . . . . . . . . . . 11 (∃𝑥 𝑥𝐴 → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto𝐴))
8078, 79syl 14 . . . . . . . . . 10 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto𝐴))
8176, 80mpbird 166 . . . . . . . . 9 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ∅ ∈ 𝑠) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
82 simpl1 985 . . . . . . . . . 10 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ¬ ∅ ∈ 𝑠) → 𝑠 ⊆ ω)
8336adantr 274 . . . . . . . . . 10 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ¬ ∅ ∈ 𝑠) → ∀𝑛 ∈ ω DECID 𝑛𝑠)
841adantr 274 . . . . . . . . . 10 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ¬ ∅ ∈ 𝑠) → 𝑓:𝑠onto𝐴)
85 simpr 109 . . . . . . . . . 10 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ¬ ∅ ∈ 𝑠) → ¬ ∅ ∈ 𝑠)
8682, 83, 84, 85ctssdclemn0 7008 . . . . . . . . 9 (((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) ∧ ¬ ∅ ∈ 𝑠) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
87 eleq1 2203 . . . . . . . . . . . 12 (𝑛 = ∅ → (𝑛𝑠 ↔ ∅ ∈ 𝑠))
8887dcbid 824 . . . . . . . . . . 11 (𝑛 = ∅ → (DECID 𝑛𝑠DECID ∅ ∈ 𝑠))
89 peano1 4517 . . . . . . . . . . . 12 ∅ ∈ ω
9089a1i 9 . . . . . . . . . . 11 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) → ∅ ∈ ω)
9188, 36, 90rspcdva 2799 . . . . . . . . . 10 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) → DECID ∅ ∈ 𝑠)
92 exmiddc 822 . . . . . . . . . 10 (DECID ∅ ∈ 𝑠 → (∅ ∈ 𝑠 ∨ ¬ ∅ ∈ 𝑠))
9391, 92syl 14 . . . . . . . . 9 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) → (∅ ∈ 𝑠 ∨ ¬ ∅ ∈ 𝑠))
9481, 86, 93mpjaodan 788 . . . . . . . 8 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠𝑓:𝑠onto𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
95943expia 1184 . . . . . . 7 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠) → (𝑓:𝑠onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
9695exlimdv 1792 . . . . . 6 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠) → (∃𝑓 𝑓:𝑠onto𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)))
97963impia 1179 . . . . 5 ((𝑠 ⊆ ω ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠 ∧ ∃𝑓 𝑓:𝑠onto𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
98973com23 1188 . . . 4 ((𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
9998exlimiv 1578 . . 3 (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))
100 foeq1 5351 . . . 4 (𝑔 = 𝑓 → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑓:ω–onto→(𝐴 ⊔ 1o)))
101100cbvexv 1891 . . 3 (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
10299, 101sylib 121 . 2 (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
103 ctssdclemr 7010 . 2 (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠))
104102, 103impbii 125 1 (∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠onto𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛𝑠) ↔ ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   ∨ wo 698  DECID wdc 820   ∧ w3a 963   = wceq 1332  ∃wex 1469   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418   ⊆ wss 3077  ∅c0 3369  ifcif 3480   ↦ cmpt 3998  ωcom 4513  ran crn 4550   Fn wfn 5128  ⟶wf 5129  –onto→wfo 5131  ‘cfv 5133  1oc1o 6316   ⊔ cdju 6935 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 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-iinf 4511 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 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4224  df-iord 4297  df-on 4299  df-suc 4302  df-iom 4514  df-xp 4555  df-rel 4556  df-cnv 4557  df-co 4558  df-dm 4559  df-rn 4560  df-res 4561  df-ima 4562  df-iota 5098  df-fun 5135  df-fn 5136  df-f 5137  df-f1 5138  df-fo 5139  df-f1o 5140  df-fv 5141  df-1st 6048  df-2nd 6049  df-1o 6323  df-dju 6936  df-inl 6945  df-inr 6946  df-case 6982 This theorem is referenced by:  ctiunct  12012
 Copyright terms: Public domain W3C validator