| Step | Hyp | Ref
| Expression |
| 1 | | 0elon 6438 |
. . . . 5
⊢ ∅
∈ On |
| 2 | | 0lt1o 8542 |
. . . . . . 7
⊢ ∅
∈ 1o |
| 3 | | omelon 9686 |
. . . . . . . 8
⊢ ω
∈ On |
| 4 | | oe0 8560 |
. . . . . . . 8
⊢ (ω
∈ On → (ω ↑o ∅) =
1o) |
| 5 | 3, 4 | ax-mp 5 |
. . . . . . 7
⊢ (ω
↑o ∅) = 1o |
| 6 | 2, 5 | eleqtrri 2840 |
. . . . . 6
⊢ ∅
∈ (ω ↑o ∅) |
| 7 | 6 | a1i 11 |
. . . . 5
⊢ (𝐴 = ∅ → ∅ ∈
(ω ↑o ∅)) |
| 8 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑥 = ∅ → (ω
↑o 𝑥) =
(ω ↑o ∅)) |
| 9 | 8 | eleq2d 2827 |
. . . . . 6
⊢ (𝑥 = ∅ → (∅
∈ (ω ↑o 𝑥) ↔ ∅ ∈ (ω
↑o ∅))) |
| 10 | 9 | rspcev 3622 |
. . . . 5
⊢ ((∅
∈ On ∧ ∅ ∈ (ω ↑o ∅)) →
∃𝑥 ∈ On ∅
∈ (ω ↑o 𝑥)) |
| 11 | 1, 7, 10 | sylancr 587 |
. . . 4
⊢ (𝐴 = ∅ → ∃𝑥 ∈ On ∅ ∈
(ω ↑o 𝑥)) |
| 12 | | eleq1 2829 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ∈ (ω
↑o 𝑥)
↔ ∅ ∈ (ω ↑o 𝑥))) |
| 13 | 12 | rexbidv 3179 |
. . . 4
⊢ (𝐴 = ∅ → (∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥) ↔ ∃𝑥 ∈ On ∅ ∈
(ω ↑o 𝑥))) |
| 14 | 11, 13 | mpbird 257 |
. . 3
⊢ (𝐴 = ∅ → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) |
| 15 | 14 | a1i 11 |
. 2
⊢ (𝐴 ∈ On → (𝐴 = ∅ → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
| 16 | | 1onn 8678 |
. . . . . 6
⊢
1o ∈ ω |
| 17 | | ondif2 8540 |
. . . . . 6
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
| 18 | 3, 16, 17 | mpbir2an 711 |
. . . . 5
⊢ ω
∈ (On ∖ 2o) |
| 19 | | ondif1 8539 |
. . . . . 6
⊢ (𝐴 ∈ (On ∖
1o) ↔ (𝐴
∈ On ∧ ∅ ∈ 𝐴)) |
| 20 | 19 | biimpri 228 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → 𝐴 ∈ (On ∖
1o)) |
| 21 | | oeeu 8641 |
. . . . 5
⊢ ((ω
∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)) →
∃!𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴)) |
| 22 | 18, 20, 21 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∃!𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴)) |
| 23 | | euex 2577 |
. . . . 5
⊢
(∃!𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴)) |
| 24 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) |
| 25 | | simp1 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑎 ∈ On) |
| 26 | | onsuc 7831 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ On → suc 𝑎 ∈ On) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → suc 𝑎 ∈ On) |
| 28 | 27 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) → suc 𝑎 ∈ On) |
| 29 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) |
| 30 | | oecl 8575 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ω
∈ On ∧ 𝑎 ∈
On) → (ω ↑o 𝑎) ∈ On) |
| 31 | 3, 25, 30 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (ω ↑o 𝑎) ∈ On) |
| 32 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ω ∈ On) |
| 33 | | omcl 8574 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ω ↑o 𝑎) ∈ On ∧ ω ∈ On) →
((ω ↑o 𝑎) ·o ω) ∈
On) |
| 34 | 31, 32, 33 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ((ω ↑o 𝑎) ·o ω)
∈ On) |
| 35 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑐 ∈ (ω ↑o 𝑎)) |
| 36 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ (ω ∖
1o) → 𝑏
∈ ω) |
| 37 | | nnon 7893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ ω → 𝑏 ∈ On) |
| 38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ∈ (ω ∖
1o) → 𝑏
∈ On) |
| 39 | 38 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑏 ∈ On) |
| 40 | | omcl 8574 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((ω ↑o 𝑎) ∈ On ∧ 𝑏 ∈ On) → ((ω
↑o 𝑎)
·o 𝑏)
∈ On) |
| 41 | 31, 39, 40 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ((ω ↑o 𝑎) ·o 𝑏) ∈ On) |
| 42 | | oaordi 8584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ↑o 𝑎) ∈ On ∧ ((ω
↑o 𝑎)
·o 𝑏)
∈ On) → (𝑐 ∈
(ω ↑o 𝑎) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ (((ω
↑o 𝑎)
·o 𝑏)
+o (ω ↑o 𝑎)))) |
| 43 | 31, 41, 42 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (𝑐 ∈ (ω ↑o 𝑎) → (((ω
↑o 𝑎)
·o 𝑏)
+o 𝑐) ∈
(((ω ↑o 𝑎) ·o 𝑏) +o (ω ↑o
𝑎)))) |
| 44 | 35, 43 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ (((ω
↑o 𝑎)
·o 𝑏)
+o (ω ↑o 𝑎))) |
| 45 | | omsuc 8564 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ω ↑o 𝑎) ∈ On ∧ 𝑏 ∈ On) → ((ω
↑o 𝑎)
·o suc 𝑏)
= (((ω ↑o 𝑎) ·o 𝑏) +o (ω ↑o
𝑎))) |
| 46 | 31, 39, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ((ω ↑o 𝑎) ·o suc 𝑏) = (((ω
↑o 𝑎)
·o 𝑏)
+o (ω ↑o 𝑎))) |
| 47 | 44, 46 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω
↑o 𝑎)
·o suc 𝑏)) |
| 48 | 36 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑏 ∈ ω) |
| 49 | | peano2 7912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ ω → suc 𝑏 ∈
ω) |
| 50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → suc 𝑏 ∈ ω) |
| 51 | | peano1 7910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∅
∈ ω |
| 52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ∅ ∈
ω) |
| 53 | | oen0 8624 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ∈ On ∧ 𝑎 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝑎)) |
| 54 | 32, 25, 52, 53 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ∅ ∈ (ω
↑o 𝑎)) |
| 55 | | omordi 8604 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ω ∈ On ∧ (ω ↑o 𝑎) ∈ On) ∧ ∅
∈ (ω ↑o 𝑎)) → (suc 𝑏 ∈ ω → ((ω
↑o 𝑎)
·o suc 𝑏)
∈ ((ω ↑o 𝑎) ·o
ω))) |
| 56 | 32, 31, 54, 55 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (suc 𝑏 ∈ ω → ((ω
↑o 𝑎)
·o suc 𝑏)
∈ ((ω ↑o 𝑎) ·o
ω))) |
| 57 | 50, 56 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ((ω ↑o 𝑎) ·o suc 𝑏) ∈ ((ω
↑o 𝑎)
·o ω)) |
| 58 | | ontr1 6430 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ω ↑o 𝑎) ·o ω) ∈ On
→ (((((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω ↑o 𝑎) ·o suc 𝑏) ∧ ((ω
↑o 𝑎)
·o suc 𝑏)
∈ ((ω ↑o 𝑎) ·o ω)) →
(((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω ↑o 𝑎) ·o
ω))) |
| 59 | 58 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ω ↑o 𝑎) ·o ω) ∈ On
∧ ((((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω ↑o 𝑎) ·o suc 𝑏) ∧ ((ω
↑o 𝑎)
·o suc 𝑏)
∈ ((ω ↑o 𝑎) ·o ω))) →
(((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω ↑o 𝑎) ·o
ω)) |
| 60 | 34, 47, 57, 59 | syl12anc 837 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω
↑o 𝑎)
·o ω)) |
| 61 | | oesuc 8565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
∈ On ∧ 𝑎 ∈
On) → (ω ↑o suc 𝑎) = ((ω ↑o 𝑎) ·o
ω)) |
| 62 | 3, 25, 61 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (ω ↑o suc
𝑎) = ((ω
↑o 𝑎)
·o ω)) |
| 63 | 60, 62 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ (ω
↑o suc 𝑎)) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ (ω
↑o suc 𝑎)) |
| 65 | 29, 64 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → 𝐴 ∈ (ω ↑o suc
𝑎)) |
| 66 | 65 | adantll 714 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → 𝐴 ∈ (ω ↑o suc
𝑎)) |
| 67 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = suc 𝑎 → (ω ↑o 𝑥) = (ω ↑o
suc 𝑎)) |
| 68 | 67 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑎 → (𝐴 ∈ (ω ↑o 𝑥) ↔ 𝐴 ∈ (ω ↑o suc
𝑎))) |
| 69 | 68 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢ ((suc
𝑎 ∈ On ∧ 𝐴 ∈ (ω
↑o suc 𝑎))
→ ∃𝑥 ∈ On
𝐴 ∈ (ω
↑o 𝑥)) |
| 70 | 28, 66, 69 | syl2an2r 685 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) |
| 71 | 70 | ex 412 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) → ((((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴 → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
| 72 | 24, 71 | syl5 34 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) → ((𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
| 73 | 72 | 3exp2 1355 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (𝑎 ∈ On → (𝑏 ∈ (ω ∖
1o) → (𝑐
∈ (ω ↑o 𝑎) → ((𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)))))) |
| 74 | 73 | imp4b 421 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ 𝑎 ∈ On) → ((𝑏 ∈ (ω ∖ 1o) ∧
𝑐 ∈ (ω
↑o 𝑎))
→ ((𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)))) |
| 75 | 74 | rexlimdvv 3212 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ 𝑎 ∈ On) → (∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
| 76 | 75 | rexlimdva 3155 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
| 77 | 76 | exlimdv 1933 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∃𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
| 78 | 23, 77 | syl5 34 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∃!𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
| 79 | 22, 78 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) |
| 80 | 79 | ex 412 |
. 2
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 →
∃𝑥 ∈ On 𝐴 ∈ (ω
↑o 𝑥))) |
| 81 | | on0eqel 6508 |
. 2
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
| 82 | 15, 80, 81 | mpjaod 861 |
1
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) |