Step | Hyp | Ref
| Expression |
1 | | simpll 524 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → 𝑓:𝑛–onto→𝐴) |
2 | | foeq2 5417 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → (𝑓:𝑛–onto→𝐴 ↔ 𝑓:∅–onto→𝐴)) |
3 | 2 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → (𝑓:𝑛–onto→𝐴 ↔ 𝑓:∅–onto→𝐴)) |
4 | 1, 3 | mpbid 146 |
. . . . . . . 8
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → 𝑓:∅–onto→𝐴) |
5 | | fo00 5478 |
. . . . . . . 8
⊢ (𝑓:∅–onto→𝐴 ↔ (𝑓 = ∅ ∧ 𝐴 = ∅)) |
6 | 4, 5 | sylib 121 |
. . . . . . 7
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → (𝑓 = ∅ ∧ 𝐴 = ∅)) |
7 | | 0ct 7084 |
. . . . . . . 8
⊢
∃𝑔 𝑔:ω–onto→(∅ ⊔
1o) |
8 | | djueq1 7017 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ⊔ 1o) =
(∅ ⊔ 1o)) |
9 | | foeq3 5418 |
. . . . . . . . . 10
⊢ ((𝐴 ⊔ 1o) =
(∅ ⊔ 1o) → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(∅ ⊔
1o))) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(∅ ⊔
1o))) |
11 | 10 | exbidv 1818 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(∅ ⊔
1o))) |
12 | 7, 11 | mpbiri 167 |
. . . . . . 7
⊢ (𝐴 = ∅ → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
13 | 6, 12 | simpl2im 384 |
. . . . . 6
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
14 | | omex 4577 |
. . . . . . . . 9
⊢ ω
∈ V |
15 | 14 | mptex 5722 |
. . . . . . . 8
⊢ (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) ∈ V |
16 | | simpll 524 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑓:𝑛–onto→𝐴) |
17 | | simplr 525 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑛 ∈ ω) |
18 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∅ ∈ 𝑛) |
19 | | eqid 2170 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) |
20 | 16, 17, 18, 19 | enumctlemm 7091 |
. . . . . . . 8
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))):ω–onto→𝐴) |
21 | | foeq1 5416 |
. . . . . . . . 9
⊢ (𝑔 = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) → (𝑔:ω–onto→𝐴 ↔ (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))):ω–onto→𝐴)) |
22 | 21 | spcegv 2818 |
. . . . . . . 8
⊢ ((𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) ∈ V → ((𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))):ω–onto→𝐴 → ∃𝑔 𝑔:ω–onto→𝐴)) |
23 | 15, 20, 22 | mpsyl 65 |
. . . . . . 7
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑔 𝑔:ω–onto→𝐴) |
24 | | fof 5420 |
. . . . . . . . . . 11
⊢ (𝑓:𝑛–onto→𝐴 → 𝑓:𝑛⟶𝐴) |
25 | 24 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑓:𝑛⟶𝐴) |
26 | 25, 18 | ffvelrnd 5632 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (𝑓‘∅) ∈ 𝐴) |
27 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓‘∅) → (𝑥 ∈ 𝐴 ↔ (𝑓‘∅) ∈ 𝐴)) |
28 | 27 | spcegv 2818 |
. . . . . . . . 9
⊢ ((𝑓‘∅) ∈ 𝐴 → ((𝑓‘∅) ∈ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴)) |
29 | 26, 26, 28 | sylc 62 |
. . . . . . . 8
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑥 𝑥 ∈ 𝐴) |
30 | | ctm 7086 |
. . . . . . . 8
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→𝐴)) |
31 | 29, 30 | syl 14 |
. . . . . . 7
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→𝐴)) |
32 | 23, 31 | mpbird 166 |
. . . . . 6
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
33 | | 0elnn 4603 |
. . . . . . 7
⊢ (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∅ ∈
𝑛)) |
34 | 33 | adantl 275 |
. . . . . 6
⊢ ((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑛 = ∅ ∨ ∅ ∈ 𝑛)) |
35 | 13, 32, 34 | mpjaodan 793 |
. . . . 5
⊢ ((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
36 | 35 | ex 114 |
. . . 4
⊢ (𝑓:𝑛–onto→𝐴 → (𝑛 ∈ ω → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))) |
37 | 36 | exlimiv 1591 |
. . 3
⊢
(∃𝑓 𝑓:𝑛–onto→𝐴 → (𝑛 ∈ ω → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))) |
38 | 37 | impcom 124 |
. 2
⊢ ((𝑛 ∈ ω ∧
∃𝑓 𝑓:𝑛–onto→𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
39 | 38 | rexlimiva 2582 |
1
⊢
(∃𝑛 ∈
ω ∃𝑓 𝑓:𝑛–onto→𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |