Step | Hyp | Ref
| Expression |
1 | | 0elon 6415 |
. . . . 5
⊢ ∅
∈ On |
2 | | 0lt1o 8499 |
. . . . . . 7
⊢ ∅
∈ 1o |
3 | | omelon 9637 |
. . . . . . . 8
⊢ ω
∈ On |
4 | | oe0 8517 |
. . . . . . . 8
⊢ (ω
∈ On → (ω ↑o ∅) =
1o) |
5 | 3, 4 | ax-mp 5 |
. . . . . . 7
⊢ (ω
↑o ∅) = 1o |
6 | 2, 5 | eleqtrri 2833 |
. . . . . 6
⊢ ∅
∈ (ω ↑o ∅) |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝐴 = ∅ → ∅ ∈
(ω ↑o ∅)) |
8 | | oveq2 7412 |
. . . . . . 7
⊢ (𝑥 = ∅ → (ω
↑o 𝑥) =
(ω ↑o ∅)) |
9 | 8 | eleq2d 2820 |
. . . . . 6
⊢ (𝑥 = ∅ → (∅
∈ (ω ↑o 𝑥) ↔ ∅ ∈ (ω
↑o ∅))) |
10 | 9 | rspcev 3612 |
. . . . 5
⊢ ((∅
∈ On ∧ ∅ ∈ (ω ↑o ∅)) →
∃𝑥 ∈ On ∅
∈ (ω ↑o 𝑥)) |
11 | 1, 7, 10 | sylancr 588 |
. . . 4
⊢ (𝐴 = ∅ → ∃𝑥 ∈ On ∅ ∈
(ω ↑o 𝑥)) |
12 | | eleq1 2822 |
. . . . 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 8635 |
. . . . . 6
⊢
1o ∈ ω |
17 | | ondif2 8497 |
. . . . . 6
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
18 | 3, 16, 17 | mpbir2an 710 |
. . . . 5
⊢ ω
∈ (On ∖ 2o) |
19 | | ondif1 8496 |
. . . . . 6
⊢ (𝐴 ∈ (On ∖
1o) ↔ (𝐴
∈ On ∧ ∅ ∈ 𝐴)) |
20 | 19 | biimpri 227 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → 𝐴 ∈ (On ∖
1o)) |
21 | | oeeu 8599 |
. . . . 5
⊢ ((ω
∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)) →
∃!𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴)) |
22 | 18, 20, 21 | sylancr 588 |
. . . 4
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ∃!𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴)) |
23 | | euex 2572 |
. . . . 5
⊢
(∃!𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑑∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴)) |
24 | | simpr 486 |
. . . . . . . . . . 11
⊢ ((𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) |
25 | | simp1 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑎 ∈ On) |
26 | | onsuc 7794 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ On → suc 𝑎 ∈ On) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → suc 𝑎 ∈ On) |
28 | 27 | adantl 483 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) → suc 𝑎 ∈ On) |
29 | | simpr 486 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) |
30 | | oecl 8532 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ω
∈ On ∧ 𝑎 ∈
On) → (ω ↑o 𝑎) ∈ On) |
31 | 3, 25, 30 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (ω ↑o 𝑎) ∈ On) |
32 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ω ∈ On) |
33 | | omcl 8531 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ω ↑o 𝑎) ∈ On ∧ ω ∈ On) →
((ω ↑o 𝑎) ·o ω) ∈
On) |
34 | 31, 32, 33 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ((ω ↑o 𝑎) ·o ω)
∈ On) |
35 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑐 ∈ (ω ↑o 𝑎)) |
36 | | eldifi 4125 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ (ω ∖
1o) → 𝑏
∈ ω) |
37 | | nnon 7856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ ω → 𝑏 ∈ On) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ∈ (ω ∖
1o) → 𝑏
∈ On) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑏 ∈ On) |
40 | | omcl 8531 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((ω ↑o 𝑎) ∈ On ∧ 𝑏 ∈ On) → ((ω
↑o 𝑎)
·o 𝑏)
∈ On) |
41 | 31, 39, 40 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ((ω ↑o 𝑎) ·o 𝑏) ∈ On) |
42 | | oaordi 8542 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ↑o 𝑎) ∈ On ∧ ((ω
↑o 𝑎)
·o 𝑏)
∈ On) → (𝑐 ∈
(ω ↑o 𝑎) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ (((ω
↑o 𝑎)
·o 𝑏)
+o (ω ↑o 𝑎)))) |
43 | 31, 41, 42 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 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 8521 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ω ↑o 𝑎) ∈ On ∧ 𝑏 ∈ On) → ((ω
↑o 𝑎)
·o suc 𝑏)
= (((ω ↑o 𝑎) ·o 𝑏) +o (ω ↑o
𝑎))) |
46 | 31, 39, 45 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ((ω ↑o 𝑎) ·o suc 𝑏) = (((ω
↑o 𝑎)
·o 𝑏)
+o (ω ↑o 𝑎))) |
47 | 44, 46 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω
↑o 𝑎)
·o suc 𝑏)) |
48 | 36 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → 𝑏 ∈ ω) |
49 | | peano2 7876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ ω → suc 𝑏 ∈
ω) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → suc 𝑏 ∈ ω) |
51 | | peano1 7874 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∅
∈ ω |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ∅ ∈
ω) |
53 | | oen0 8582 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ∈ On ∧ 𝑎 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝑎)) |
54 | 32, 25, 52, 53 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → ∅ ∈ (ω
↑o 𝑎)) |
55 | | omordi 8562 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ω ∈ On ∧ (ω ↑o 𝑎) ∈ On) ∧ ∅
∈ (ω ↑o 𝑎)) → (suc 𝑏 ∈ ω → ((ω
↑o 𝑎)
·o suc 𝑏)
∈ ((ω ↑o 𝑎) ·o
ω))) |
56 | 32, 31, 54, 55 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . 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 6407 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ω ↑o 𝑎) ·o ω) ∈ On
→ (((((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω ↑o 𝑎) ·o suc 𝑏) ∧ ((ω
↑o 𝑎)
·o suc 𝑏)
∈ ((ω ↑o 𝑎) ·o ω)) →
(((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω ↑o 𝑎) ·o
ω))) |
59 | 58 | imp 408 |
. . . . . . . . . . . . . . . . . 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 836 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ ((ω
↑o 𝑎)
·o ω)) |
61 | | oesuc 8522 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
∈ On ∧ 𝑎 ∈
On) → (ω ↑o suc 𝑎) = ((ω ↑o 𝑎) ·o
ω)) |
62 | 3, 25, 61 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (ω ↑o suc
𝑎) = ((ω
↑o 𝑎)
·o ω)) |
63 | 60, 62 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ (ω
↑o suc 𝑎)) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) ∈ (ω
↑o suc 𝑎)) |
65 | 29, 64 | eqeltrrd 2835 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎)) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → 𝐴 ∈ (ω ↑o suc
𝑎)) |
66 | 65 | adantll 713 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → 𝐴 ∈ (ω ↑o suc
𝑎)) |
67 | | oveq2 7412 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = suc 𝑎 → (ω ↑o 𝑥) = (ω ↑o
suc 𝑎)) |
68 | 67 | eleq2d 2820 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = suc 𝑎 → (𝐴 ∈ (ω ↑o 𝑥) ↔ 𝐴 ∈ (ω ↑o suc
𝑎))) |
69 | 68 | rspcev 3612 |
. . . . . . . . . . . . 13
⊢ ((suc
𝑎 ∈ On ∧ 𝐴 ∈ (ω
↑o suc 𝑎))
→ ∃𝑥 ∈ On
𝐴 ∈ (ω
↑o 𝑥)) |
70 | 28, 66, 69 | syl2an2r 684 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝑎 ∈ On ∧ 𝑏 ∈ (ω ∖
1o) ∧ 𝑐
∈ (ω ↑o 𝑎))) ∧ (((ω ↑o 𝑎) ·o 𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) |
71 | 70 | ex 414 |
. . . . . . . . . . 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 423 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ 𝑎 ∈ On) → ((𝑏 ∈ (ω ∖ 1o) ∧
𝑐 ∈ (ω
↑o 𝑎))
→ ((𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)))) |
75 | 74 | rexlimdvv 3211 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ 𝑎 ∈ On) → (∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
76 | 75 | rexlimdva 3156 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → (∃𝑎 ∈ On ∃𝑏 ∈ (ω ∖
1o)∃𝑐
∈ (ω ↑o 𝑎)(𝑑 = 〈𝑎, 𝑏, 𝑐〉 ∧ (((ω ↑o
𝑎) ·o
𝑏) +o 𝑐) = 𝐴) → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))) |
77 | 76 | exlimdv 1937 |
. . . . 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 414 |
. 2
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 →
∃𝑥 ∈ On 𝐴 ∈ (ω
↑o 𝑥))) |
81 | | on0eqel 6485 |
. 2
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
82 | 15, 80, 81 | mpjaod 859 |
1
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥)) |