Step | Hyp | Ref
| Expression |
1 | | 0lt1o 6416 |
. . . . 5
⊢ ∅
∈ 1o |
2 | | djurcl 7025 |
. . . . 5
⊢ (∅
∈ 1o → (inr‘∅) ∈ (∅ ⊔
1o)) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢
(inr‘∅) ∈ (∅ ⊔
1o) |
4 | 3 | fconst6 5395 |
. . 3
⊢ (ω
× {(inr‘∅)}):ω⟶(∅ ⊔
1o) |
5 | | peano1 4576 |
. . . . 5
⊢ ∅
∈ ω |
6 | | rex0 3431 |
. . . . . . . . 9
⊢ ¬
∃𝑤 ∈ ∅
𝑦 = (inl‘𝑤) |
7 | | djur 7042 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (∅ ⊔
1o) ↔ (∃𝑤 ∈ ∅ 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤))) |
8 | 7 | biimpi 119 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (∅ ⊔
1o) → (∃𝑤 ∈ ∅ 𝑦 = (inl‘𝑤) ∨ ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤))) |
9 | 8 | ord 719 |
. . . . . . . . 9
⊢ (𝑦 ∈ (∅ ⊔
1o) → (¬ ∃𝑤 ∈ ∅ 𝑦 = (inl‘𝑤) → ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤))) |
10 | 6, 9 | mpi 15 |
. . . . . . . 8
⊢ (𝑦 ∈ (∅ ⊔
1o) → ∃𝑤 ∈ 1o 𝑦 = (inr‘𝑤)) |
11 | | df1o2 6405 |
. . . . . . . . 9
⊢
1o = {∅} |
12 | 11 | rexeqi 2670 |
. . . . . . . 8
⊢
(∃𝑤 ∈
1o 𝑦 =
(inr‘𝑤) ↔
∃𝑤 ∈
{∅}𝑦 =
(inr‘𝑤)) |
13 | 10, 12 | sylib 121 |
. . . . . . 7
⊢ (𝑦 ∈ (∅ ⊔
1o) → ∃𝑤 ∈ {∅}𝑦 = (inr‘𝑤)) |
14 | | 0ex 4114 |
. . . . . . . 8
⊢ ∅
∈ V |
15 | | fveq2 5494 |
. . . . . . . . 9
⊢ (𝑤 = ∅ →
(inr‘𝑤) =
(inr‘∅)) |
16 | 15 | eqeq2d 2182 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑦 = (inr‘𝑤) ↔ 𝑦 = (inr‘∅))) |
17 | 14, 16 | rexsn 3625 |
. . . . . . 7
⊢
(∃𝑤 ∈
{∅}𝑦 =
(inr‘𝑤) ↔ 𝑦 =
(inr‘∅)) |
18 | 13, 17 | sylib 121 |
. . . . . 6
⊢ (𝑦 ∈ (∅ ⊔
1o) → 𝑦 =
(inr‘∅)) |
19 | 3 | elexi 2742 |
. . . . . . . 8
⊢
(inr‘∅) ∈ V |
20 | 19 | fvconst2 5709 |
. . . . . . 7
⊢ (∅
∈ ω → ((ω × {(inr‘∅)})‘∅) =
(inr‘∅)) |
21 | 5, 20 | ax-mp 5 |
. . . . . 6
⊢ ((ω
× {(inr‘∅)})‘∅) =
(inr‘∅) |
22 | 18, 21 | eqtr4di 2221 |
. . . . 5
⊢ (𝑦 ∈ (∅ ⊔
1o) → 𝑦 =
((ω × {(inr‘∅)})‘∅)) |
23 | | fveq2 5494 |
. . . . . 6
⊢ (𝑧 = ∅ → ((ω
× {(inr‘∅)})‘𝑧) = ((ω ×
{(inr‘∅)})‘∅)) |
24 | 23 | rspceeqv 2852 |
. . . . 5
⊢ ((∅
∈ ω ∧ 𝑦 =
((ω × {(inr‘∅)})‘∅)) → ∃𝑧 ∈ ω 𝑦 = ((ω ×
{(inr‘∅)})‘𝑧)) |
25 | 5, 22, 24 | sylancr 412 |
. . . 4
⊢ (𝑦 ∈ (∅ ⊔
1o) → ∃𝑧 ∈ ω 𝑦 = ((ω ×
{(inr‘∅)})‘𝑧)) |
26 | 25 | rgen 2523 |
. . 3
⊢
∀𝑦 ∈
(∅ ⊔ 1o)∃𝑧 ∈ ω 𝑦 = ((ω ×
{(inr‘∅)})‘𝑧) |
27 | | dffo3 5640 |
. . 3
⊢ ((ω
× {(inr‘∅)}):ω–onto→(∅ ⊔ 1o) ↔
((ω × {(inr‘∅)}):ω⟶(∅ ⊔
1o) ∧ ∀𝑦 ∈ (∅ ⊔
1o)∃𝑧
∈ ω 𝑦 =
((ω × {(inr‘∅)})‘𝑧))) |
28 | 4, 26, 27 | mpbir2an 937 |
. 2
⊢ (ω
× {(inr‘∅)}):ω–onto→(∅ ⊔
1o) |
29 | | omex 4575 |
. . . 4
⊢ ω
∈ V |
30 | 19 | snex 4169 |
. . . 4
⊢
{(inr‘∅)} ∈ V |
31 | 29, 30 | xpex 4724 |
. . 3
⊢ (ω
× {(inr‘∅)}) ∈ V |
32 | | foeq1 5414 |
. . 3
⊢ (𝑓 = (ω ×
{(inr‘∅)}) → (𝑓:ω–onto→(∅ ⊔ 1o) ↔
(ω × {(inr‘∅)}):ω–onto→(∅ ⊔
1o))) |
33 | 31, 32 | spcev 2825 |
. 2
⊢ ((ω
× {(inr‘∅)}):ω–onto→(∅ ⊔ 1o) →
∃𝑓 𝑓:ω–onto→(∅ ⊔
1o)) |
34 | 28, 33 | ax-mp 5 |
1
⊢
∃𝑓 𝑓:ω–onto→(∅ ⊔
1o) |