Step | Hyp | Ref
| Expression |
1 | | simpll 519 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → 𝑓:𝑛–onto→𝐴) |
2 | | foeq2 5390 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → (𝑓:𝑛–onto→𝐴 ↔ 𝑓:∅–onto→𝐴)) |
3 | 2 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → (𝑓:𝑛–onto→𝐴 ↔ 𝑓:∅–onto→𝐴)) |
4 | 1, 3 | mpbid 146 |
. . . . . . . 8
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → 𝑓:∅–onto→𝐴) |
5 | | fo00 5451 |
. . . . . . . 8
⊢ (𝑓:∅–onto→𝐴 ↔ (𝑓 = ∅ ∧ 𝐴 = ∅)) |
6 | 4, 5 | sylib 121 |
. . . . . . 7
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → (𝑓 = ∅ ∧ 𝐴 = ∅)) |
7 | | 0ct 7052 |
. . . . . . . 8
⊢
∃𝑔 𝑔:ω–onto→(∅ ⊔
1o) |
8 | | djueq1 6985 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐴 ⊔ 1o) =
(∅ ⊔ 1o)) |
9 | | foeq3 5391 |
. . . . . . . . . 10
⊢ ((𝐴 ⊔ 1o) =
(∅ ⊔ 1o) → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(∅ ⊔
1o))) |
10 | 8, 9 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ 𝑔:ω–onto→(∅ ⊔
1o))) |
11 | 10 | exbidv 1805 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(∅ ⊔
1o))) |
12 | 7, 11 | mpbiri 167 |
. . . . . . 7
⊢ (𝐴 = ∅ → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
13 | 6, 12 | simpl2im 384 |
. . . . . 6
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ 𝑛 = ∅) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
14 | | omex 4553 |
. . . . . . . . 9
⊢ ω
∈ V |
15 | 14 | mptex 5694 |
. . . . . . . 8
⊢ (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) ∈ V |
16 | | simpll 519 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑓:𝑛–onto→𝐴) |
17 | | simplr 520 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑛 ∈ ω) |
18 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∅ ∈ 𝑛) |
19 | | eqid 2157 |
. . . . . . . . 9
⊢ (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) |
20 | 16, 17, 18, 19 | enumctlemm 7059 |
. . . . . . . 8
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))):ω–onto→𝐴) |
21 | | foeq1 5389 |
. . . . . . . . 9
⊢ (𝑔 = (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) → (𝑔:ω–onto→𝐴 ↔ (𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))):ω–onto→𝐴)) |
22 | 21 | spcegv 2800 |
. . . . . . . 8
⊢ ((𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))) ∈ V → ((𝑘 ∈ ω ↦ if(𝑘 ∈ 𝑛, (𝑓‘𝑘), (𝑓‘∅))):ω–onto→𝐴 → ∃𝑔 𝑔:ω–onto→𝐴)) |
23 | 15, 20, 22 | mpsyl 65 |
. . . . . . 7
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑔 𝑔:ω–onto→𝐴) |
24 | | fof 5393 |
. . . . . . . . . . 11
⊢ (𝑓:𝑛–onto→𝐴 → 𝑓:𝑛⟶𝐴) |
25 | 24 | ad2antrr 480 |
. . . . . . . . . 10
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → 𝑓:𝑛⟶𝐴) |
26 | 25, 18 | ffvelrnd 5604 |
. . . . . . . . 9
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → (𝑓‘∅) ∈ 𝐴) |
27 | | eleq1 2220 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓‘∅) → (𝑥 ∈ 𝐴 ↔ (𝑓‘∅) ∈ 𝐴)) |
28 | 27 | spcegv 2800 |
. . . . . . . . 9
⊢ ((𝑓‘∅) ∈ 𝐴 → ((𝑓‘∅) ∈ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴)) |
29 | 26, 26, 28 | sylc 62 |
. . . . . . . 8
⊢ (((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) ∧ ∅ ∈ 𝑛) → ∃𝑥 𝑥 ∈ 𝐴) |
30 | | ctm 7054 |
. . . . . . . 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 4579 |
. . . . . . 7
⊢ (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∅ ∈
𝑛)) |
34 | 33 | adantl 275 |
. . . . . 6
⊢ ((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) → (𝑛 = ∅ ∨ ∅ ∈ 𝑛)) |
35 | 13, 32, 34 | mpjaodan 788 |
. . . . 5
⊢ ((𝑓:𝑛–onto→𝐴 ∧ 𝑛 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
36 | 35 | ex 114 |
. . . 4
⊢ (𝑓:𝑛–onto→𝐴 → (𝑛 ∈ ω → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))) |
37 | 36 | exlimiv 1578 |
. . 3
⊢
(∃𝑓 𝑓:𝑛–onto→𝐴 → (𝑛 ∈ ω → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o))) |
38 | 37 | impcom 124 |
. 2
⊢ ((𝑛 ∈ ω ∧
∃𝑓 𝑓:𝑛–onto→𝐴) → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |
39 | 38 | rexlimiva 2569 |
1
⊢
(∃𝑛 ∈
ω ∃𝑓 𝑓:𝑛–onto→𝐴 → ∃𝑔 𝑔:ω–onto→(𝐴 ⊔ 1o)) |