| Step | Hyp | Ref
| Expression |
| 1 | | eleq2 2830 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ∅)) |
| 2 | | noel 4338 |
. . . . . . 7
⊢ ¬
𝐴 ∈
∅ |
| 3 | 2 | pm2.21i 119 |
. . . . . 6
⊢ (𝐴 ∈ ∅ → (∅
∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵)) |
| 4 | 1, 3 | biimtrdi 253 |
. . . . 5
⊢ (𝐵 = ∅ → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐴 → (𝐴 ·o 𝐵) = 𝐵))) |
| 5 | 4 | impd 410 |
. . . 4
⊢ (𝐵 = ∅ → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 6 | 5 | com12 32 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = ∅ → (𝐴 ·o 𝐵) = 𝐵)) |
| 7 | | elpri 4649 |
. . . . . . . . 9
⊢ (𝐴 ∈ {∅, 1o}
→ (𝐴 = ∅ ∨
𝐴 =
1o)) |
| 8 | | eleq2 2830 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → (∅
∈ 𝐴 ↔ ∅
∈ ∅)) |
| 9 | | noel 4338 |
. . . . . . . . . . . 12
⊢ ¬
∅ ∈ ∅ |
| 10 | 9 | pm2.21i 119 |
. . . . . . . . . . 11
⊢ (∅
∈ ∅ → (𝐴
·o 2o) = 2o) |
| 11 | 8, 10 | biimtrdi 253 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (∅
∈ 𝐴 → (𝐴 ·o
2o) = 2o)) |
| 12 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝐴 = 1o → (𝐴 ·o
2o) = (1o ·o
2o)) |
| 13 | | 2on 8520 |
. . . . . . . . . . . . 13
⊢
2o ∈ On |
| 14 | | om1r 8581 |
. . . . . . . . . . . . 13
⊢
(2o ∈ On → (1o ·o
2o) = 2o) |
| 15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1o ·o 2o) =
2o |
| 16 | 12, 15 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝐴 = 1o → (𝐴 ·o
2o) = 2o) |
| 17 | 16 | a1d 25 |
. . . . . . . . . 10
⊢ (𝐴 = 1o → (∅
∈ 𝐴 → (𝐴 ·o
2o) = 2o)) |
| 18 | 11, 17 | jaoi 858 |
. . . . . . . . 9
⊢ ((𝐴 = ∅ ∨ 𝐴 = 1o) →
(∅ ∈ 𝐴 →
(𝐴 ·o
2o) = 2o)) |
| 19 | 7, 18 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ {∅, 1o}
→ (∅ ∈ 𝐴
→ (𝐴
·o 2o) = 2o)) |
| 20 | | df2o3 8514 |
. . . . . . . 8
⊢
2o = {∅, 1o} |
| 21 | 19, 20 | eleq2s 2859 |
. . . . . . 7
⊢ (𝐴 ∈ 2o →
(∅ ∈ 𝐴 →
(𝐴 ·o
2o) = 2o)) |
| 22 | 21 | imp 406 |
. . . . . 6
⊢ ((𝐴 ∈ 2o ∧
∅ ∈ 𝐴) →
(𝐴 ·o
2o) = 2o) |
| 23 | 22 | a1i 11 |
. . . . 5
⊢ (𝐵 = 2o → ((𝐴 ∈ 2o ∧
∅ ∈ 𝐴) →
(𝐴 ·o
2o) = 2o)) |
| 24 | | eleq2 2830 |
. . . . . 6
⊢ (𝐵 = 2o → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 2o)) |
| 25 | 24 | anbi1d 631 |
. . . . 5
⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ∈ 2o ∧ ∅ ∈
𝐴))) |
| 26 | | oveq2 7439 |
. . . . . 6
⊢ (𝐵 = 2o → (𝐴 ·o 𝐵) = (𝐴 ·o
2o)) |
| 27 | | id 22 |
. . . . . 6
⊢ (𝐵 = 2o → 𝐵 =
2o) |
| 28 | 26, 27 | eqeq12d 2753 |
. . . . 5
⊢ (𝐵 = 2o → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o 2o) =
2o)) |
| 29 | 23, 25, 28 | 3imtr4d 294 |
. . . 4
⊢ (𝐵 = 2o → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 30 | 29 | com12 32 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → (𝐵 = 2o → (𝐴 ·o 𝐵) = 𝐵)) |
| 31 | | simpr 484 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
𝐴 ∈ ω) →
𝐴 ∈
ω) |
| 32 | | simpllr 776 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
𝐴 ∈ ω) →
∅ ∈ 𝐴) |
| 33 | | omelon 9686 |
. . . . . . . . . 10
⊢ ω
∈ On |
| 34 | | oecl 8575 |
. . . . . . . . . 10
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ↑o 𝐶) ∈ On) |
| 35 | 33, 34 | mpan 690 |
. . . . . . . . 9
⊢ (𝐶 ∈ On → (ω
↑o 𝐶)
∈ On) |
| 36 | 35 | adantl 481 |
. . . . . . . 8
⊢ ((𝐵 = (ω ↑o
(ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω
↑o 𝐶)
∈ On) |
| 37 | 36 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
𝐴 ∈ ω) →
(ω ↑o 𝐶) ∈ On) |
| 38 | 33 | jctl 523 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → (ω
∈ On ∧ 𝐶 ∈
On)) |
| 39 | | peano1 7910 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
| 40 | | oen0 8624 |
. . . . . . . . . 10
⊢
(((ω ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝐶)) |
| 41 | 38, 39, 40 | sylancl 586 |
. . . . . . . . 9
⊢ (𝐶 ∈ On → ∅ ∈
(ω ↑o 𝐶)) |
| 42 | 41 | adantl 481 |
. . . . . . . 8
⊢ ((𝐵 = (ω ↑o
(ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ∅ ∈ (ω
↑o 𝐶)) |
| 43 | 42 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
𝐴 ∈ ω) →
∅ ∈ (ω ↑o 𝐶)) |
| 44 | | omabs 8689 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ((ω
↑o 𝐶)
∈ On ∧ ∅ ∈ (ω ↑o 𝐶))) → (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 45 | 31, 32, 37, 43, 44 | syl22anc 839 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
𝐴 ∈ ω) →
(𝐴 ·o
(ω ↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 46 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝐵 = (ω ↑o
(ω ↑o 𝐶)) → (𝐴 ·o 𝐵) = (𝐴 ·o (ω
↑o (ω ↑o 𝐶)))) |
| 47 | | id 22 |
. . . . . . . . 9
⊢ (𝐵 = (ω ↑o
(ω ↑o 𝐶)) → 𝐵 = (ω ↑o (ω
↑o 𝐶))) |
| 48 | 46, 47 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝐵 = (ω ↑o
(ω ↑o 𝐶)) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶)))) |
| 49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝐵 = (ω ↑o
(ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶)))) |
| 50 | 49 | ad2antlr 727 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
𝐴 ∈ ω) →
((𝐴 ·o
𝐵) = 𝐵 ↔ (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶)))) |
| 51 | 45, 50 | mpbird 257 |
. . . . 5
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
𝐴 ∈ ω) →
(𝐴 ·o
𝐵) = 𝐵) |
| 52 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝐵 = (ω ↑o
(ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 = (ω ↑o (ω
↑o 𝐶))) |
| 53 | | oecl 8575 |
. . . . . . . . . . . . . 14
⊢ ((ω
∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω
↑o (ω ↑o 𝐶)) ∈ On) |
| 54 | 33, 35, 53 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ On → (ω
↑o (ω ↑o 𝐶)) ∈ On) |
| 55 | 54 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐵 = (ω ↑o
(ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → (ω
↑o (ω ↑o 𝐶)) ∈ On) |
| 56 | 52, 55 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((𝐵 = (ω ↑o
(ω ↑o 𝐶)) ∧ 𝐶 ∈ On) → 𝐵 ∈ On) |
| 57 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → 𝐴 ∈ 𝐵) |
| 58 | | onelon 6409 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ On) |
| 59 | 56, 57, 58 | syl2anr 597 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
𝐴 ∈
On) |
| 60 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
∅ ∈ 𝐴) |
| 61 | | ondif1 8539 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (On ∖
1o) ↔ (𝐴
∈ On ∧ ∅ ∈ 𝐴)) |
| 62 | 59, 60, 61 | sylanbrc 583 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
𝐴 ∈ (On ∖
1o)) |
| 63 | | 1onn 8678 |
. . . . . . . . . 10
⊢
1o ∈ ω |
| 64 | | ondif2 8540 |
. . . . . . . . . 10
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
| 65 | 33, 63, 64 | mpbir2an 711 |
. . . . . . . . 9
⊢ ω
∈ (On ∖ 2o) |
| 66 | 62, 65 | jctil 519 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
(ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖
1o))) |
| 67 | 66 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) →
(ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖
1o))) |
| 68 | | oeeu 8641 |
. . . . . . 7
⊢ ((ω
∈ (On ∖ 2o) ∧ 𝐴 ∈ (On ∖ 1o)) →
∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖
1o)∃𝑧
∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴)) |
| 69 | 67, 68 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) →
∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖
1o)∃𝑧
∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴)) |
| 70 | | euex 2577 |
. . . . . . 7
⊢
(∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖
1o)∃𝑧
∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → ∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖
1o)∃𝑧
∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴)) |
| 71 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) |
| 72 | | 0ss 4400 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∅
⊆ 𝑧 |
| 73 | | 0elon 6438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ On |
| 74 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) → 𝑥 ∈ On) |
| 75 | | oecl 8575 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ω
∈ On ∧ 𝑥 ∈
On) → (ω ↑o 𝑥) ∈ On) |
| 76 | 33, 74, 75 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) →
(ω ↑o 𝑥) ∈ On) |
| 77 | 76 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) → (ω ↑o 𝑥) ∈ On) |
| 78 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ↑o 𝑥) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑥)) → 𝑧 ∈ On) |
| 79 | 77, 78 | sylancom 588 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) → 𝑧 ∈ On) |
| 80 | | 1on 8518 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
1o ∈ On |
| 81 | | omcl 8574 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((ω ↑o 𝑥) ∈ On ∧ 1o ∈ On)
→ ((ω ↑o 𝑥) ·o 1o) ∈
On) |
| 82 | 76, 80, 81 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) →
((ω ↑o 𝑥) ·o 1o) ∈
On) |
| 83 | 82 | ad5ant12 756 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o
1o) ∈ On) |
| 84 | | oaword 8587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((∅
∈ On ∧ 𝑧 ∈ On
∧ ((ω ↑o 𝑥) ·o 1o) ∈
On) → (∅ ⊆ 𝑧 ↔ (((ω ↑o 𝑥) ·o
1o) +o ∅) ⊆ (((ω ↑o
𝑥) ·o
1o) +o 𝑧))) |
| 85 | 84 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((∅
∈ On ∧ 𝑧 ∈ On
∧ ((ω ↑o 𝑥) ·o 1o) ∈
On) → (∅ ⊆ 𝑧 → (((ω ↑o 𝑥) ·o
1o) +o ∅) ⊆ (((ω ↑o
𝑥) ·o
1o) +o 𝑧))) |
| 86 | 73, 79, 83, 85 | mp3an2ani 1470 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ⊆ 𝑧 → (((ω ↑o 𝑥) ·o
1o) +o ∅) ⊆ (((ω ↑o
𝑥) ·o
1o) +o 𝑧))) |
| 87 | 72, 86 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o
1o) +o ∅) ⊆ (((ω ↑o
𝑥) ·o
1o) +o 𝑧)) |
| 88 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ (ω ∖
1o)) |
| 89 | | omsson 7891 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ω
⊆ On |
| 90 | | ssdif 4144 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ω
⊆ On → (ω ∖ 1o) ⊆ (On ∖
1o)) |
| 91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ω
∖ 1o) ⊆ (On ∖ 1o) |
| 92 | 91 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (ω ∖
1o) → 𝑦
∈ (On ∖ 1o)) |
| 93 | | ondif1 8539 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (On ∖
1o) ↔ (𝑦
∈ On ∧ ∅ ∈ 𝑦)) |
| 94 | | df-1o 8506 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
1o = suc ∅ |
| 95 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ On → Ord 𝑦) |
| 96 | | ordsucss 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝑦 → (∅ ∈
𝑦 → suc ∅
⊆ 𝑦)) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ On → (∅
∈ 𝑦 → suc ∅
⊆ 𝑦)) |
| 98 | 97 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ On ∧ ∅ ∈
𝑦) → suc ∅
⊆ 𝑦) |
| 99 | 94, 98 | eqsstrid 4022 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ On ∧ ∅ ∈
𝑦) → 1o
⊆ 𝑦) |
| 100 | 93, 99 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (On ∖
1o) → 1o ⊆ 𝑦) |
| 101 | 88, 92, 100 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑦) |
| 102 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (ω ∖
1o) → 𝑦
∈ ω) |
| 103 | | nnon 7893 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
| 104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (ω ∖
1o) → 𝑦
∈ On) |
| 105 | 104 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) → 𝑦 ∈ On) |
| 106 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ On) |
| 107 | 33, 106, 75 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ On) |
| 108 | | omwordi 8609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1o ∈ On ∧ 𝑦 ∈ On ∧ (ω ↑o
𝑥) ∈ On) →
(1o ⊆ 𝑦
→ ((ω ↑o 𝑥) ·o 1o) ⊆
((ω ↑o 𝑥) ·o 𝑦))) |
| 109 | 80, 105, 107, 108 | mp3an2ani 1470 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑦 → ((ω
↑o 𝑥)
·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦))) |
| 110 | 101, 109 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o
1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦)) |
| 111 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ On) |
| 112 | | omcl 8574 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω
↑o 𝑥)
·o 𝑦)
∈ On) |
| 113 | 107, 111,
112 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o 𝑦) ∈ On) |
| 114 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ On) |
| 115 | | oawordri 8588 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((ω ↑o 𝑥) ·o 1o) ∈
On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On ∧ 𝑧 ∈ On) → (((ω
↑o 𝑥)
·o 1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (((ω
↑o 𝑥)
·o 1o) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))) |
| 116 | 83, 113, 114, 115 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o
1o) ⊆ ((ω ↑o 𝑥) ·o 𝑦) → (((ω ↑o 𝑥) ·o
1o) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧))) |
| 117 | 110, 116 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o
1o) +o 𝑧) ⊆ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧)) |
| 118 | 87, 117 | sstrd 3994 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o
1o) +o ∅) ⊆ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧)) |
| 119 | 33, 75 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (ω
↑o 𝑥)
∈ On) |
| 120 | 119, 80, 81 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → ((ω
↑o 𝑥)
·o 1o) ∈ On) |
| 121 | | oa0 8554 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ω ↑o 𝑥) ·o 1o) ∈
On → (((ω ↑o 𝑥) ·o 1o)
+o ∅) = ((ω ↑o 𝑥) ·o
1o)) |
| 122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → (((ω
↑o 𝑥)
·o 1o) +o ∅) = ((ω
↑o 𝑥)
·o 1o)) |
| 123 | | om1 8580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ω
↑o 𝑥)
∈ On → ((ω ↑o 𝑥) ·o 1o) =
(ω ↑o 𝑥)) |
| 124 | 119, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → ((ω
↑o 𝑥)
·o 1o) = (ω ↑o 𝑥)) |
| 125 | 122, 124 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ On → (((ω
↑o 𝑥)
·o 1o) +o ∅) = (ω
↑o 𝑥)) |
| 126 | 106, 125 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o
1o) +o ∅) = (ω ↑o 𝑥)) |
| 127 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) |
| 128 | 118, 126,
127 | 3sstr3d 4038 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ⊆ 𝐴) |
| 129 | | simp-7l 789 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ 𝐵) |
| 130 | | simplrl 777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) →
𝐵 = (ω
↑o (ω ↑o 𝐶))) |
| 131 | 130 | ad4antr 732 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐵 = (ω ↑o (ω
↑o 𝐶))) |
| 132 | 129, 131 | eleqtrd 2843 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ∈ (ω ↑o (ω
↑o 𝐶))) |
| 133 | 55 | ad6antlr 737 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o
(ω ↑o 𝐶)) ∈ On) |
| 134 | | ontr2 6431 |
. . . . . . . . . . . . . . . . 17
⊢
(((ω ↑o 𝑥) ∈ On ∧ (ω ↑o
(ω ↑o 𝐶)) ∈ On) → (((ω
↑o 𝑥)
⊆ 𝐴 ∧ 𝐴 ∈ (ω
↑o (ω ↑o 𝐶))) → (ω ↑o 𝑥) ∈ (ω
↑o (ω ↑o 𝐶)))) |
| 135 | 107, 133,
134 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω
↑o 𝐶)))
→ (ω ↑o 𝑥) ∈ (ω ↑o (ω
↑o 𝐶)))) |
| 136 | 128, 132,
135 | mp2and 699 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝑥) ∈ (ω
↑o (ω ↑o 𝐶))) |
| 137 | 36 | ad6antlr 737 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o 𝐶) ∈ On) |
| 138 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ∈ (On ∖
2o)) |
| 139 | | oeord 8626 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ (ω
↑o 𝐶)
∈ On ∧ ω ∈ (On ∖ 2o)) → (𝑥 ∈ (ω
↑o 𝐶)
↔ (ω ↑o 𝑥) ∈ (ω ↑o (ω
↑o 𝐶)))) |
| 140 | 106, 137,
138, 139 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 ∈ (ω ↑o 𝐶) ↔ (ω
↑o 𝑥)
∈ (ω ↑o (ω ↑o 𝐶)))) |
| 141 | 136, 140 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑥 ∈ (ω ↑o 𝐶)) |
| 142 | | simp-5r 786 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ 𝐴) |
| 143 | 142, 128 | unssd 4192 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∪ (ω
↑o 𝑥))
⊆ 𝐴) |
| 144 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ∈ (ω ↑o 𝑥)) |
| 145 | | onelpss 6424 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ On ∧ (ω
↑o 𝑥)
∈ On) → (𝑧 ∈
(ω ↑o 𝑥) ↔ (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)))) |
| 146 | 145 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ On ∧ (ω
↑o 𝑥)
∈ On) → (𝑧 ∈
(ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)))) |
| 147 | 79, 107, 146 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ∈ (ω ↑o 𝑥) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥)))) |
| 148 | 144, 147 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ⊆ (ω ↑o 𝑥) ∧ 𝑧 ≠ (ω ↑o 𝑥))) |
| 149 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ⊆ (ω
↑o 𝑥) ∧
𝑧 ≠ (ω
↑o 𝑥))
→ 𝑧 ⊆ (ω
↑o 𝑥)) |
| 150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑧 ⊆ (ω ↑o 𝑥)) |
| 151 | | oaword 8587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ On ∧ (ω
↑o 𝑥)
∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) ↔ (((ω
↑o 𝑥)
·o 𝑦)
+o 𝑧) ⊆
(((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o
𝑥)))) |
| 152 | 151 | biimpd 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ On ∧ (ω
↑o 𝑥)
∈ On ∧ ((ω ↑o 𝑥) ·o 𝑦) ∈ On) → (𝑧 ⊆ (ω ↑o 𝑥) → (((ω
↑o 𝑥)
·o 𝑦)
+o 𝑧) ⊆
(((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o
𝑥)))) |
| 153 | 114, 107,
113, 152 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑧 ⊆ (ω ↑o 𝑥) → (((ω
↑o 𝑥)
·o 𝑦)
+o 𝑧) ⊆
(((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o
𝑥)))) |
| 154 | 150, 153 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ (((ω
↑o 𝑥)
·o 𝑦)
+o (ω ↑o 𝑥))) |
| 155 | | omsuc 8564 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ω ↑o 𝑥) ∈ On ∧ 𝑦 ∈ On) → ((ω
↑o 𝑥)
·o suc 𝑦)
= (((ω ↑o 𝑥) ·o 𝑦) +o (ω ↑o
𝑥))) |
| 156 | 107, 111,
155 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) = (((ω
↑o 𝑥)
·o 𝑦)
+o (ω ↑o 𝑥))) |
| 157 | 154, 156 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω
↑o 𝑥)
·o suc 𝑦)) |
| 158 | | ordom 7897 |
. . . . . . . . . . . . . . . . . . 19
⊢ Ord
ω |
| 159 | 88, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝑦 ∈ ω) |
| 160 | | ordsucss 7838 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
ω → (𝑦 ∈
ω → suc 𝑦
⊆ ω)) |
| 161 | 158, 159,
160 | mpsyl 68 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ ω) |
| 162 | | oe1 8582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ω
∈ On → (ω ↑o 1o) =
ω) |
| 163 | 33, 162 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ω
↑o 1o) = ω |
| 164 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑥 = ∅) |
| 165 | 164 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω
↑o 𝑥) =
(ω ↑o ∅)) |
| 166 | | oe0 8560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (ω
∈ On → (ω ↑o ∅) =
1o) |
| 167 | 33, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ω
↑o ∅) = 1o |
| 168 | 165, 167 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (ω
↑o 𝑥) =
1o) |
| 169 | 168 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω
↑o 𝑥)
·o 𝑦) =
(1o ·o 𝑦)) |
| 170 | 104 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) → 𝑦
∈ On) |
| 171 | 170 | ad5ant12 756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ On) |
| 172 | | om1r 8581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ On → (1o
·o 𝑦) =
𝑦) |
| 173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (1o
·o 𝑦) =
𝑦) |
| 174 | 169, 173 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → ((ω
↑o 𝑥)
·o 𝑦) =
𝑦) |
| 175 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ (ω ↑o 𝑥)) |
| 176 | 175, 168 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 ∈ 1o) |
| 177 | | el1o 8533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ 1o ↔
𝑧 =
∅) |
| 178 | 176, 177 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑧 = ∅) |
| 179 | 174, 178 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω
↑o 𝑥)
·o 𝑦)
+o 𝑧) = (𝑦 +o
∅)) |
| 180 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (((ω
↑o 𝑥)
·o 𝑦)
+o 𝑧) = 𝐴) |
| 181 | | oa0 8554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ On → (𝑦 +o ∅) = 𝑦) |
| 182 | 171, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → (𝑦 +o ∅) = 𝑦) |
| 183 | 179, 180,
182 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 = 𝑦) |
| 184 | 159 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝑦 ∈ ω) |
| 185 | 183, 184 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) ∧ 𝑥 = ∅) → 𝐴 ∈ ω) |
| 186 | 185 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 𝐴 ∈ ω)) |
| 187 | 33, 33 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ω
∈ On ∧ ω ∈ On) |
| 188 | | ontr2 6431 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ω
∈ On ∧ ω ∈ On) → ((ω ⊆ 𝐴 ∧ 𝐴 ∈ ω) → ω ∈
ω)) |
| 189 | 188 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ω
∈ On ∧ ω ∈ On) → (ω ⊆ 𝐴 → (𝐴 ∈ ω → ω ∈
ω))) |
| 190 | 187, 142,
189 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ∈ ω → ω ∈
ω)) |
| 191 | | elirr 9637 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ¬
ω ∈ ω |
| 192 | 191 | pm2.21i 119 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ω
∈ ω → 1o ⊆ 𝑥) |
| 193 | 192 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ∈ ω →
1o ⊆ 𝑥)) |
| 194 | 186, 190,
193 | 3syld 60 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ → 1o ⊆ 𝑥)) |
| 195 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ On → Ord 𝑥) |
| 196 | | ordsucss 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝑥 → (∅ ∈
𝑥 → suc ∅
⊆ 𝑥)) |
| 197 | 196 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Ord
𝑥 ∧ ∅ ∈
𝑥) → suc ∅
⊆ 𝑥) |
| 198 | 94, 197 | eqsstrid 4022 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Ord
𝑥 ∧ ∅ ∈
𝑥) → 1o
⊆ 𝑥) |
| 199 | 198 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Ord
𝑥 → (∅ ∈
𝑥 → 1o
⊆ 𝑥)) |
| 200 | 106, 195,
199 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (∅ ∈ 𝑥 → 1o ⊆ 𝑥)) |
| 201 | | on0eqel 6508 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ On → (𝑥 = ∅ ∨ ∅ ∈
𝑥)) |
| 202 | 106, 201 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥)) |
| 203 | 194, 200,
202 | mpjaod 861 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ⊆ 𝑥) |
| 204 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 1o ∈
On) |
| 205 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ∈ On) |
| 206 | 204, 106,
205 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ∈ On ∧
𝑥 ∈ On ∧ ω
∈ On)) |
| 207 | | oewordi 8629 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (1o ⊆ 𝑥 → (ω ↑o
1o) ⊆ (ω ↑o 𝑥))) |
| 208 | 206, 39, 207 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (1o ⊆ 𝑥 → (ω
↑o 1o) ⊆ (ω ↑o 𝑥))) |
| 209 | 203, 208 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o
1o) ⊆ (ω ↑o 𝑥)) |
| 210 | 163, 209 | eqsstrrid 4023 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ω ⊆ (ω
↑o 𝑥)) |
| 211 | 161, 210 | sstrd 3994 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ⊆ (ω ↑o 𝑥)) |
| 212 | | onsuc 7831 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
| 213 | 111, 212 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → suc 𝑦 ∈ On) |
| 214 | | omwordi 8609 |
. . . . . . . . . . . . . . . . . 18
⊢ ((suc
𝑦 ∈ On ∧ (ω
↑o 𝑥)
∈ On ∧ (ω ↑o 𝑥) ∈ On) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω
↑o 𝑥)
·o suc 𝑦)
⊆ ((ω ↑o 𝑥) ·o (ω
↑o 𝑥)))) |
| 215 | 213, 107,
107, 214 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (suc 𝑦 ⊆ (ω ↑o 𝑥) → ((ω
↑o 𝑥)
·o suc 𝑦)
⊆ ((ω ↑o 𝑥) ·o (ω
↑o 𝑥)))) |
| 216 | 211, 215 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((ω ↑o 𝑥) ·o suc 𝑦) ⊆ ((ω
↑o 𝑥)
·o (ω ↑o 𝑥))) |
| 217 | 157, 216 | sstrd 3994 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) ⊆ ((ω
↑o 𝑥)
·o (ω ↑o 𝑥))) |
| 218 | 127 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 = (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧)) |
| 219 | | oeoa 8635 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
∈ On ∧ 𝑥 ∈ On
∧ 𝑥 ∈ On) →
(ω ↑o (𝑥 +o 𝑥)) = ((ω ↑o 𝑥) ·o (ω
↑o 𝑥))) |
| 220 | 33, 106, 106, 219 | mp3an2i 1468 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (ω ↑o (𝑥 +o 𝑥)) = ((ω
↑o 𝑥)
·o (ω ↑o 𝑥))) |
| 221 | 217, 218,
220 | 3sstr4d 4039 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) |
| 222 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) |
| 223 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ On) |
| 224 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
𝐶 ∈
On) |
| 225 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → 𝑥 ∈ (ω ↑o 𝐶)) |
| 226 | 224, 225 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐶 ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶))) |
| 227 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((ω ↑o 𝐶) ∈ On ∧ 𝑥 ∈ (ω ↑o 𝐶)) → 𝑥 ∈ On) |
| 228 | 35, 227 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω
↑o 𝐶))
→ 𝑥 ∈
On) |
| 229 | | pm4.24 563 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ On ↔ (𝑥 ∈ On ∧ 𝑥 ∈ On)) |
| 230 | 228, 229 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω
↑o 𝐶))
→ (𝑥 ∈ On ∧
𝑥 ∈
On)) |
| 231 | | oacl 8573 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On) → (𝑥 +o 𝑥) ∈ On) |
| 232 | 230, 231 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω
↑o 𝐶))
→ (𝑥 +o
𝑥) ∈
On) |
| 233 | | oecl 8575 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ω
∈ On ∧ (𝑥
+o 𝑥) ∈ On)
→ (ω ↑o (𝑥 +o 𝑥)) ∈ On) |
| 234 | 33, 232, 233 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω
↑o 𝐶))
→ (ω ↑o (𝑥 +o 𝑥)) ∈ On) |
| 235 | 226, 234 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o (𝑥
+o 𝑥)) ∈
On) |
| 236 | 55 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o (ω ↑o 𝐶)) ∈ On) |
| 237 | | omwordri 8610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ (ω
↑o (𝑥
+o 𝑥)) ∈ On
∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o
(𝑥 +o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶))))) |
| 238 | 223, 235,
236, 237 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)) → (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o
(𝑥 +o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶))))) |
| 239 | 222, 238 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) ⊆ ((ω ↑o
(𝑥 +o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 240 | 226, 230,
231 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o 𝑥) ∈ On) |
| 241 | 36 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o 𝐶)
∈ On) |
| 242 | | oeoa 8635 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ω
∈ On ∧ (𝑥
+o 𝑥) ∈ On
∧ (ω ↑o 𝐶) ∈ On) → (ω
↑o ((𝑥
+o 𝑥)
+o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 243 | 33, 240, 241, 242 | mp3an2i 1468 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o ((𝑥
+o 𝑥)
+o (ω ↑o 𝐶))) = ((ω ↑o (𝑥 +o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 244 | 226, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ On) |
| 245 | | oaass 8599 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ On ∧ 𝑥 ∈ On ∧ (ω
↑o 𝐶)
∈ On) → ((𝑥
+o 𝑥)
+o (ω ↑o 𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o
𝐶)))) |
| 246 | 244, 244,
241, 245 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o
𝐶)) = (𝑥 +o (𝑥 +o (ω ↑o
𝐶)))) |
| 247 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝑥 ∈ (ω ↑o 𝐶)) |
| 248 | | ssidd 4007 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o 𝐶)
⊆ (ω ↑o 𝐶)) |
| 249 | | oaabs2 8687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ↑o 𝐶) ∈ On) ∧ (ω
↑o 𝐶)
⊆ (ω ↑o 𝐶)) → (𝑥 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶)) |
| 250 | 247, 241,
248, 249 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶)) |
| 251 | 250 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 +o (𝑥 +o (ω ↑o
𝐶))) = (𝑥 +o (ω ↑o
𝐶))) |
| 252 | 246, 251,
250 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝑥 +o 𝑥) +o (ω ↑o
𝐶)) = (ω
↑o 𝐶)) |
| 253 | 252 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o ((𝑥
+o 𝑥)
+o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 254 | 243, 253 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω
↑o (𝑥
+o 𝑥))
·o (ω ↑o (ω ↑o
𝐶))) = (ω
↑o (ω ↑o 𝐶))) |
| 255 | 239, 254 | sseqtrd 4020 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) ⊆ (ω ↑o
(ω ↑o 𝐶))) |
| 256 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = ∅ → (ω
↑o 𝑥) =
(ω ↑o ∅)) |
| 257 | 256, 167 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = ∅ → (ω
↑o 𝑥) =
1o) |
| 258 | 257 | uneq2d 4168 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = ∅ → (ω ∪
(ω ↑o 𝑥)) = (ω ∪
1o)) |
| 259 | 33 | oneluni 6503 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(1o ∈ ω → (ω ∪ 1o) =
ω) |
| 260 | 63, 259 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ω
∪ 1o) = ω |
| 261 | 260, 163 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ω
∪ 1o) = (ω ↑o
1o) |
| 262 | 258, 261 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ∅ → (ω ∪
(ω ↑o 𝑥)) = (ω ↑o
1o)) |
| 263 | 262 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (ω ∪ (ω
↑o 𝑥)) =
(ω ↑o 1o)) |
| 264 | 263 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω
↑o 𝑥))
·o (ω ↑o (ω ↑o
𝐶))) = ((ω
↑o 1o) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 265 | 224 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → 𝐶 ∈ On) |
| 266 | | oecl 8575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((ω
∈ On ∧ ∅ ∈ On) → (ω ↑o ∅)
∈ On) |
| 267 | 33, 73, 266 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (ω
↑o ∅) ∈ On |
| 268 | | oecl 8575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ω
∈ On ∧ (ω ↑o ∅) ∈ On) → (ω
↑o (ω ↑o ∅)) ∈
On) |
| 269 | 33, 267, 268 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ω
↑o (ω ↑o ∅)) ∈
On |
| 270 | 269 | 2a1i 12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω
↑o (ω ↑o ∅)) ∈
On)) |
| 271 | 270, 54 | jca2 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ((ω
↑o (ω ↑o ∅)) ∈ On ∧
(ω ↑o (ω ↑o 𝐶)) ∈ On))) |
| 272 | 167 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (ω
↑o (ω ↑o ∅)) = (ω
↑o 1o) |
| 273 | 272, 163 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (ω
↑o (ω ↑o ∅)) =
ω |
| 274 | | ssun1 4178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ω
⊆ (ω ∪ (ω ↑o 𝑥)) |
| 275 | 273, 274 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (ω
↑o (ω ↑o ∅)) ⊆ (ω ∪
(ω ↑o 𝑥)) |
| 276 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω ∪
(ω ↑o 𝑥)) ⊆ 𝐴) |
| 277 | 275, 276 | sstrid 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (ω
↑o (ω ↑o ∅)) ⊆ 𝐴) |
| 278 | 277 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o (ω ↑o ∅)) ⊆ 𝐴) |
| 279 | 57 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ 𝐵) |
| 280 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐵 = (ω ↑o (ω
↑o 𝐶))) |
| 281 | 279, 280 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → 𝐴 ∈ (ω ↑o (ω
↑o 𝐶))) |
| 282 | 278, 281 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω
↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω
↑o 𝐶)))) |
| 283 | 282 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω
↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω
↑o 𝐶)))) |
| 284 | | ontr2 6431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((ω ↑o (ω ↑o ∅))
∈ On ∧ (ω ↑o (ω ↑o 𝐶)) ∈ On) → (((ω
↑o (ω ↑o ∅)) ⊆ 𝐴 ∧ 𝐴 ∈ (ω ↑o (ω
↑o 𝐶)))
→ (ω ↑o (ω ↑o ∅)) ∈
(ω ↑o (ω ↑o 𝐶)))) |
| 285 | 271, 283,
284 | syl6ci 71 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → (ω
↑o (ω ↑o ∅)) ∈ (ω
↑o (ω ↑o 𝐶)))) |
| 286 | | oeord 8626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((∅
∈ On ∧ 𝐶 ∈ On
∧ ω ∈ (On ∖ 2o)) → (∅ ∈ 𝐶 ↔ (ω
↑o ∅) ∈ (ω ↑o 𝐶))) |
| 287 | 73, 65, 286 | mp3an13 1454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ (ω
↑o ∅) ∈ (ω ↑o 𝐶))) |
| 288 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐶 ∈ On → ω ∈
(On ∖ 2o)) |
| 289 | | oeord 8626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ω ↑o ∅) ∈ On ∧ (ω
↑o 𝐶)
∈ On ∧ ω ∈ (On ∖ 2o)) → ((ω
↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω
↑o (ω ↑o ∅)) ∈ (ω
↑o (ω ↑o 𝐶)))) |
| 290 | 267, 35, 288, 289 | mp3an2i 1468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐶 ∈ On → ((ω
↑o ∅) ∈ (ω ↑o 𝐶) ↔ (ω
↑o (ω ↑o ∅)) ∈ (ω
↑o (ω ↑o 𝐶)))) |
| 291 | 287, 290 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ (ω
↑o (ω ↑o ∅)) ∈ (ω
↑o (ω ↑o 𝐶)))) |
| 292 | 291 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐶 ∈ On → ((ω
↑o (ω ↑o ∅)) ∈ (ω
↑o (ω ↑o 𝐶)) → ∅ ∈ 𝐶)) |
| 293 | 285, 292 | sylcom 30 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → ∅ ∈ 𝐶)) |
| 294 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐶 ∈ On → Ord 𝐶) |
| 295 | | ordsucss 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Ord
𝐶 → (∅ ∈
𝐶 → suc ∅
⊆ 𝐶)) |
| 296 | 94 | sseq1i 4012 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(1o ⊆ 𝐶 ↔ suc ∅ ⊆ 𝐶) |
| 297 | 295, 296 | imbitrrdi 252 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝐶 → (∅ ∈
𝐶 → 1o
⊆ 𝐶)) |
| 298 | 294, 297 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 →
1o ⊆ 𝐶)) |
| 299 | 293, 298 | sylcom 30 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On → 1o ⊆
𝐶)) |
| 300 | 265, 299 | jcai 516 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → (𝐶 ∈ On ∧ 1o ⊆ 𝐶)) |
| 301 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐶 ∈ On → ω ∈
On) |
| 302 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐶 ∈ On → 1o
∈ On) |
| 303 | 301, 302,
35 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐶 ∈ On → (ω
∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On)) |
| 304 | 303 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) → (ω
∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On)) |
| 305 | | oeoa 8635 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ω
∈ On ∧ 1o ∈ On ∧ (ω ↑o 𝐶) ∈ On) → (ω
↑o (1o +o (ω ↑o
𝐶))) = ((ω
↑o 1o) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 306 | 304, 305 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) → (ω
↑o (1o +o (ω ↑o
𝐶))) = ((ω
↑o 1o) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 307 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) →
1o ∈ ω) |
| 308 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) → (ω
↑o 𝐶)
∈ On) |
| 309 | | oeword 8628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((1o ∈ On ∧ 𝐶 ∈ On ∧ ω ∈ (On ∖
2o)) → (1o ⊆ 𝐶 ↔ (ω ↑o
1o) ⊆ (ω ↑o 𝐶))) |
| 310 | 80, 65, 309 | mp3an13 1454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐶 ∈ On → (1o
⊆ 𝐶 ↔ (ω
↑o 1o) ⊆ (ω ↑o 𝐶))) |
| 311 | 310 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) → (ω
↑o 1o) ⊆ (ω ↑o 𝐶)) |
| 312 | 163, 311 | eqsstrrid 4023 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) → ω
⊆ (ω ↑o 𝐶)) |
| 313 | | oaabs 8686 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((1o ∈ ω ∧ (ω ↑o 𝐶) ∈ On) ∧ ω
⊆ (ω ↑o 𝐶)) → (1o +o
(ω ↑o 𝐶)) = (ω ↑o 𝐶)) |
| 314 | 307, 308,
312, 313 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) →
(1o +o (ω ↑o 𝐶)) = (ω ↑o 𝐶)) |
| 315 | 314 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) → (ω
↑o (1o +o (ω ↑o
𝐶))) = (ω
↑o (ω ↑o 𝐶))) |
| 316 | 306, 315 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ On ∧ 1o
⊆ 𝐶) → ((ω
↑o 1o) ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 317 | 300, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω
↑o 1o) ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 318 | 264, 317 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ 𝑥 = ∅) → ((ω ∪ (ω
↑o 𝑥))
·o (ω ↑o (ω ↑o
𝐶))) = (ω
↑o (ω ↑o 𝐶))) |
| 319 | 244, 195,
196 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (∅ ∈
𝑥 → suc ∅
⊆ 𝑥)) |
| 320 | 319 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → suc ∅ ⊆
𝑥) |
| 321 | 94, 320 | eqsstrid 4022 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 1o ⊆
𝑥) |
| 322 | 247 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ (ω ↑o 𝐶)) |
| 323 | 241, 322,
227 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → 𝑥 ∈ On) |
| 324 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ∈ (On
∖ 2o)) |
| 325 | | oeword 8628 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((1o ∈ On ∧ 𝑥 ∈ On ∧ ω ∈ (On ∖
2o)) → (1o ⊆ 𝑥 ↔ (ω ↑o
1o) ⊆ (ω ↑o 𝑥))) |
| 326 | 80, 323, 324, 325 | mp3an2i 1468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (1o ⊆
𝑥 ↔ (ω
↑o 1o) ⊆ (ω ↑o 𝑥))) |
| 327 | 321, 326 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω
↑o 1o) ⊆ (ω ↑o 𝑥)) |
| 328 | 163, 327 | eqsstrrid 4023 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ω ⊆
(ω ↑o 𝑥)) |
| 329 | | ssequn1 4186 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ω
⊆ (ω ↑o 𝑥) ↔ (ω ∪ (ω
↑o 𝑥)) =
(ω ↑o 𝑥)) |
| 330 | 328, 329 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω ∪ (ω
↑o 𝑥)) =
(ω ↑o 𝑥)) |
| 331 | 330 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪
(ω ↑o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 332 | 241 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω
↑o 𝐶)
∈ On) |
| 333 | | oeoa 8635 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ω
∈ On ∧ 𝑥 ∈ On
∧ (ω ↑o 𝐶) ∈ On) → (ω
↑o (𝑥
+o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 334 | 33, 323, 332, 333 | mp3an2i 1468 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω
↑o (𝑥
+o (ω ↑o 𝐶))) = ((ω ↑o 𝑥) ·o (ω
↑o (ω ↑o 𝐶)))) |
| 335 | | ssidd 4007 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω
↑o 𝐶)
⊆ (ω ↑o 𝐶)) |
| 336 | 322, 332,
335, 249 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (𝑥 +o (ω ↑o
𝐶)) = (ω
↑o 𝐶)) |
| 337 | 336 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → (ω
↑o (𝑥
+o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 338 | 331, 334,
337 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) ∧ ∅ ∈ 𝑥) → ((ω ∪
(ω ↑o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 339 | 226, 228,
201 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝑥 = ∅ ∨ ∅ ∈ 𝑥)) |
| 340 | 318, 338,
339 | mpjaodan 961 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪
(ω ↑o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 341 | 276 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪
(ω ↑o 𝑥)) ⊆ 𝐴) |
| 342 | 33, 228, 75 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω
↑o 𝐶))
→ (ω ↑o 𝑥) ∈ On) |
| 343 | 342, 33 | jctil 519 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ On ∧ 𝑥 ∈ (ω
↑o 𝐶))
→ (ω ∈ On ∧ (ω ↑o 𝑥) ∈ On)) |
| 344 | | onun2 6492 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ω
∈ On ∧ (ω ↑o 𝑥) ∈ On) → (ω ∪ (ω
↑o 𝑥))
∈ On) |
| 345 | 226, 343,
344 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω ∪
(ω ↑o 𝑥)) ∈ On) |
| 346 | | omwordri 8610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ∪ (ω ↑o 𝑥)) ∈ On ∧ 𝐴 ∈ On ∧ (ω ↑o
(ω ↑o 𝐶)) ∈ On) → ((ω ∪
(ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω
↑o 𝑥))
·o (ω ↑o (ω ↑o
𝐶))) ⊆ (𝐴 ·o (ω
↑o (ω ↑o 𝐶))))) |
| 347 | 345, 223,
236, 346 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪
(ω ↑o 𝑥)) ⊆ 𝐴 → ((ω ∪ (ω
↑o 𝑥))
·o (ω ↑o (ω ↑o
𝐶))) ⊆ (𝐴 ·o (ω
↑o (ω ↑o 𝐶))))) |
| 348 | 341, 347 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((ω ∪
(ω ↑o 𝑥)) ·o (ω
↑o (ω ↑o 𝐶))) ⊆ (𝐴 ·o (ω
↑o (ω ↑o 𝐶)))) |
| 349 | 340, 348 | eqsstrrd 4019 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (ω
↑o (ω ↑o 𝐶)) ⊆ (𝐴 ·o (ω
↑o (ω ↑o 𝐶)))) |
| 350 | 255, 349 | eqssd 4001 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶))) |
| 351 | 49 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → ((𝐴 ·o 𝐵) = 𝐵 ↔ (𝐴 ·o (ω
↑o (ω ↑o 𝐶))) = (ω ↑o (ω
↑o 𝐶)))) |
| 352 | 350, 351 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
(𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥)))) → (𝐴 ·o 𝐵) = 𝐵) |
| 353 | 352 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
((𝑥 ∈ (ω
↑o 𝐶) ∧
(ω ∪ (ω ↑o 𝑥)) ⊆ 𝐴 ∧ 𝐴 ⊆ (ω ↑o (𝑥 +o 𝑥))) → (𝐴 ·o 𝐵) = 𝐵)) |
| 354 | 353 | ad5antr 734 |
. . . . . . . . . . . . . 14
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → ((𝑥 ∈ (ω ↑o 𝐶) ∧ (ω ∪ (ω
↑o 𝑥))
⊆ 𝐴 ∧ 𝐴 ⊆ (ω
↑o (𝑥
+o 𝑥))) →
(𝐴 ·o
𝐵) = 𝐵)) |
| 355 | 141, 143,
221, 354 | mp3and 1466 |
. . . . . . . . . . . . 13
⊢
((((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) ∧ (((ω ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵) |
| 356 | 355 | ex 412 |
. . . . . . . . . . . 12
⊢
(((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) → ((((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴 → (𝐴 ·o 𝐵) = 𝐵)) |
| 357 | 71, 356 | syl5 34 |
. . . . . . . . . . 11
⊢
(((((((𝐴 ∈
𝐵 ∧ ∅ ∈
𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) ∧ 𝑧
∈ (ω ↑o 𝑥)) → ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 358 | 357 | rexlimdva 3155 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) ∧ 𝑦 ∈ (ω ∖
1o)) → (∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 359 | 358 | rexlimdva 3155 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) ∧
𝑥 ∈ On) →
(∃𝑦 ∈ (ω
∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 360 | 359 | rexlimdva 3155 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) →
(∃𝑥 ∈ On
∃𝑦 ∈ (ω
∖ 1o)∃𝑧 ∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 361 | 360 | exlimdv 1933 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) →
(∃𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖
1o)∃𝑧
∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 362 | 70, 361 | syl5 34 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) →
(∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (ω ∖
1o)∃𝑧
∈ (ω ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((ω ↑o
𝑥) ·o
𝑦) +o 𝑧) = 𝐴) → (𝐴 ·o 𝐵) = 𝐵)) |
| 363 | 69, 362 | mpd 15 |
. . . . 5
⊢ ((((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) ∧
ω ⊆ 𝐴) →
(𝐴 ·o
𝐵) = 𝐵) |
| 364 | | eloni 6394 |
. . . . . . 7
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 365 | 59, 364 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
Ord 𝐴) |
| 366 | | ordtri2or 6482 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord ω) →
(𝐴 ∈ ω ∨
ω ⊆ 𝐴)) |
| 367 | 365, 158,
366 | sylancl 586 |
. . . . 5
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
(𝐴 ∈ ω ∨
ω ⊆ 𝐴)) |
| 368 | 51, 363, 367 | mpjaodan 961 |
. . . 4
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
(𝐴 ·o
𝐵) = 𝐵) |
| 369 | 368 | ex 412 |
. . 3
⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On) →
(𝐴 ·o
𝐵) = 𝐵)) |
| 370 | 6, 30, 369 | 3jaod 1431 |
. 2
⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) → ((𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On)) →
(𝐴 ·o
𝐵) = 𝐵)) |
| 371 | 370 | imp 406 |
1
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω
↑o 𝐶))
∧ 𝐶 ∈ On))) →
(𝐴 ·o
𝐵) = 𝐵) |