| Step | Hyp | Ref
| Expression |
| 1 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (∅
∈ 𝑥 ↔ ∅
∈ ∅)) |
| 2 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (ω
↑o 𝑥) =
(ω ↑o ∅)) |
| 3 | 2 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐴 ·o (ω
↑o 𝑥)) =
(𝐴 ·o
(ω ↑o ∅))) |
| 4 | 3, 2 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥) ↔ (𝐴 ·o (ω
↑o ∅)) = (ω ↑o
∅))) |
| 5 | 1, 4 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((∅
∈ 𝑥 → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥)) ↔ (∅ ∈ ∅ →
(𝐴 ·o
(ω ↑o ∅)) = (ω ↑o
∅)))) |
| 6 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝑦)) |
| 7 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (ω ↑o 𝑥) = (ω ↑o
𝑦)) |
| 8 | 7 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 ·o (ω
↑o 𝑥)) =
(𝐴 ·o
(ω ↑o 𝑦))) |
| 9 | 8, 7 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥) ↔ (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) |
| 10 | 6, 9 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥)) ↔ (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)))) |
| 11 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → (∅ ∈ 𝑥 ↔ ∅ ∈ suc 𝑦)) |
| 12 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (ω ↑o 𝑥) = (ω ↑o
suc 𝑦)) |
| 13 | 12 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o (ω
↑o 𝑥)) =
(𝐴 ·o
(ω ↑o suc 𝑦))) |
| 14 | 13, 12 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥) ↔ (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦))) |
| 15 | 11, 14 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥)) ↔ (∅ ∈ suc 𝑦 → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦)))) |
| 16 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (∅ ∈ 𝑥 ↔ ∅ ∈ 𝐵)) |
| 17 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (ω ↑o 𝑥) = (ω ↑o
𝐵)) |
| 18 | 17 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝐴 ·o (ω
↑o 𝑥)) =
(𝐴 ·o
(ω ↑o 𝐵))) |
| 19 | 18, 17 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥) ↔ (𝐴 ·o (ω
↑o 𝐵)) =
(ω ↑o 𝐵))) |
| 20 | 16, 19 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((∅ ∈ 𝑥 → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥)) ↔ (∅ ∈ 𝐵 → (𝐴 ·o (ω
↑o 𝐵)) =
(ω ↑o 𝐵)))) |
| 21 | | noel 4338 |
. . . . . . . . 9
⊢ ¬
∅ ∈ ∅ |
| 22 | 21 | pm2.21i 119 |
. . . . . . . 8
⊢ (∅
∈ ∅ → (𝐴
·o (ω ↑o ∅)) = (ω
↑o ∅)) |
| 23 | 22 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) → (∅ ∈ ∅ → (𝐴 ·o (ω
↑o ∅)) = (ω ↑o
∅))) |
| 24 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ω ∈ On) |
| 25 | | simpll 767 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → 𝐴 ∈
ω) |
| 26 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ∅ ∈ 𝐴) |
| 27 | | omabslem 8688 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
∈ On ∧ 𝐴 ∈
ω ∧ ∅ ∈ 𝐴) → (𝐴 ·o ω) =
ω) |
| 28 | 24, 25, 26, 27 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (𝐴
·o ω) = ω) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) ∧ 𝑦 = ∅)
→ (𝐴
·o ω) = ω) |
| 30 | | suceq 6450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅) |
| 31 | | df-1o 8506 |
. . . . . . . . . . . . . . . . . 18
⊢
1o = suc ∅ |
| 32 | 30, 31 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ∅ → suc 𝑦 =
1o) |
| 33 | 32 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ∅ → (ω
↑o suc 𝑦) =
(ω ↑o 1o)) |
| 34 | | oe1 8582 |
. . . . . . . . . . . . . . . . 17
⊢ (ω
∈ On → (ω ↑o 1o) =
ω) |
| 35 | 34 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (ω ↑o 1o) =
ω) |
| 36 | 33, 35 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) ∧ 𝑦 = ∅)
→ (ω ↑o suc 𝑦) = ω) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) ∧ 𝑦 = ∅)
→ (𝐴
·o (ω ↑o suc 𝑦)) = (𝐴 ·o
ω)) |
| 38 | 29, 37, 36 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) ∧ 𝑦 = ∅)
→ (𝐴
·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦)) |
| 39 | 38 | ex 412 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (𝑦 = ∅
→ (𝐴
·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦))) |
| 40 | 39 | a1dd 50 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (𝑦 = ∅
→ ((∅ ∈ 𝑦
→ (𝐴
·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦)))) |
| 41 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) → ((𝐴 ·o (ω
↑o 𝑦))
·o ω) = ((ω ↑o 𝑦) ·o
ω)) |
| 42 | | oesuc 8565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
∈ On ∧ 𝑦 ∈
On) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o
ω)) |
| 43 | 42 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (ω ↑o suc 𝑦) = ((ω ↑o 𝑦) ·o
ω)) |
| 44 | 43 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (𝐴
·o (ω ↑o suc 𝑦)) = (𝐴 ·o ((ω
↑o 𝑦)
·o ω))) |
| 45 | | nnon 7893 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
| 46 | 45 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → 𝐴 ∈
On) |
| 47 | | oecl 8575 |
. . . . . . . . . . . . . . . . . 18
⊢ ((ω
∈ On ∧ 𝑦 ∈
On) → (ω ↑o 𝑦) ∈ On) |
| 48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (ω ↑o 𝑦) ∈ On) |
| 49 | | omass 8618 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ (ω
↑o 𝑦)
∈ On ∧ ω ∈ On) → ((𝐴 ·o (ω
↑o 𝑦))
·o ω) = (𝐴 ·o ((ω
↑o 𝑦)
·o ω))) |
| 50 | 46, 48, 24, 49 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ((𝐴
·o (ω ↑o 𝑦)) ·o ω) = (𝐴 ·o ((ω
↑o 𝑦)
·o ω))) |
| 51 | 44, 50 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (𝐴
·o (ω ↑o suc 𝑦)) = ((𝐴 ·o (ω
↑o 𝑦))
·o ω)) |
| 52 | 51, 43 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ((𝐴
·o (ω ↑o suc 𝑦)) = (ω ↑o suc 𝑦) ↔ ((𝐴 ·o (ω
↑o 𝑦))
·o ω) = ((ω ↑o 𝑦) ·o
ω))) |
| 53 | 41, 52 | imbitrrid 246 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ((𝐴
·o (ω ↑o 𝑦)) = (ω ↑o 𝑦) → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦))) |
| 54 | 53 | imim2d 57 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦)))) |
| 55 | 54 | com23 86 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (∅ ∈ 𝑦 → ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦)))) |
| 56 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → 𝑦 ∈
On) |
| 57 | | on0eqel 6508 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ On → (𝑦 = ∅ ∨ ∅ ∈
𝑦)) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → (𝑦 = ∅
∨ ∅ ∈ 𝑦)) |
| 59 | 40, 55, 58 | mpjaod 861 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦))) |
| 60 | 59 | a1dd 50 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝑦 ∈
On)) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦)))) |
| 61 | 60 | anassrs 467 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) ∧ 𝑦 ∈
On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦)))) |
| 62 | 61 | expcom 413 |
. . . . . . 7
⊢ (𝑦 ∈ On → (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) → ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (∅ ∈ suc 𝑦 → (𝐴 ·o (ω
↑o suc 𝑦))
= (ω ↑o suc 𝑦))))) |
| 63 | 45 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → 𝐴 ∈ On) |
| 64 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ ω ∈ On) |
| 65 | | simprr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ Lim 𝑥) |
| 66 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
| 67 | 65, 66 | jctil 519 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ (𝑥 ∈ V ∧
Lim 𝑥)) |
| 68 | | limelon 6448 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
| 69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ 𝑥 ∈
On) |
| 70 | | oecl 8575 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
∈ On ∧ 𝑥 ∈
On) → (ω ↑o 𝑥) ∈ On) |
| 71 | 64, 69, 70 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ (ω ↑o 𝑥) ∈ On) |
| 72 | 71 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (ω ↑o 𝑥) ∈ On) |
| 73 | | 1onn 8678 |
. . . . . . . . . . . . . . . . 17
⊢
1o ∈ ω |
| 74 | | ondif2 8540 |
. . . . . . . . . . . . . . . . 17
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
| 75 | 64, 73, 74 | sylanblrc 590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ ω ∈ (On ∖ 2o)) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → ω ∈ (On ∖
2o)) |
| 77 | 67 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝑥 ∈ V ∧ Lim 𝑥)) |
| 78 | | oelimcl 8638 |
. . . . . . . . . . . . . . 15
⊢ ((ω
∈ (On ∖ 2o) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (ω ↑o
𝑥)) |
| 79 | 76, 77, 78 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → Lim (ω ↑o
𝑥)) |
| 80 | | omlim 8571 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ ((ω
↑o 𝑥)
∈ On ∧ Lim (ω ↑o 𝑥))) → (𝐴 ·o (ω
↑o 𝑥)) =
∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧)) |
| 81 | 63, 72, 79, 80 | syl12anc 837 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝐴 ·o (ω
↑o 𝑥)) =
∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧)) |
| 82 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → ω ∈
On) |
| 83 | | oelim2 8633 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ω
∈ On ∧ (𝑥 ∈ V
∧ Lim 𝑥)) →
(ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω
↑o 𝑦)) |
| 84 | 82, 77, 83 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (ω ↑o 𝑥) = ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω
↑o 𝑦)) |
| 85 | 84 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ 𝑧 ∈ ∪
𝑦 ∈ (𝑥 ∖ 1o)(ω
↑o 𝑦))) |
| 86 | | eliun 4995 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ∪ 𝑦 ∈ (𝑥 ∖ 1o)(ω
↑o 𝑦)
↔ ∃𝑦 ∈
(𝑥 ∖
1o)𝑧 ∈
(ω ↑o 𝑦)) |
| 87 | 85, 86 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))) |
| 88 | 69 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → 𝑥 ∈ On) |
| 89 | | anass 468 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)))) |
| 90 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
| 91 | | on0eln0 6440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ On → (∅
∈ 𝑦 ↔ 𝑦 ≠ ∅)) |
| 92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅)) |
| 93 | 92 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅))) |
| 94 | | dif1o 8538 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (𝑥 ∖ 1o) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ≠ ∅)) |
| 95 | 93, 94 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ↔ 𝑦 ∈ (𝑥 ∖ 1o))) |
| 96 | 95 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → (((𝑦 ∈ 𝑥 ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω
↑o 𝑦)))) |
| 97 | 89, 96 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) ↔ (𝑦 ∈ (𝑥 ∖ 1o) ∧ 𝑧 ∈ (ω
↑o 𝑦)))) |
| 98 | 97 | rexbidv2 3175 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ On → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))) |
| 99 | 88, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) ↔ ∃𝑦 ∈ (𝑥 ∖ 1o)𝑧 ∈ (ω ↑o 𝑦))) |
| 100 | 87, 99 | bitr4d 282 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) ↔ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)))) |
| 101 | | r19.29 3114 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∃𝑦 ∈ 𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)))) |
| 102 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((∅
∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) |
| 103 | 102 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((∅ ∈ 𝑦
→ (𝐴
·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) |
| 104 | 103 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((∅ ∈ 𝑦
→ (𝐴
·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ ∅ ∈ 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) |
| 105 | 104 | anasss 466 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((∅ ∈ 𝑦
→ (𝐴
·o (ω ↑o 𝑦)) = (ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) |
| 106 | 71 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω
↑o 𝑥)
∈ On) |
| 107 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ω
↑o 𝑥)
∈ On → Ord (ω ↑o 𝑥)) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → Ord (ω
↑o 𝑥)) |
| 109 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ (ω ↑o 𝑦)) |
| 110 | 64 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈
On) |
| 111 | 69 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑥 ∈ On) |
| 112 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ 𝑥) |
| 113 | 111, 112,
90 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑦 ∈ On) |
| 114 | 110, 113,
47 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω
↑o 𝑦)
∈ On) |
| 115 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((ω ↑o 𝑦) ∈ On ∧ 𝑧 ∈ (ω ↑o 𝑦)) → 𝑧 ∈ On) |
| 116 | 114, 109,
115 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝑧 ∈ On) |
| 117 | 45 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ 𝐴 ∈
On) |
| 118 | 117 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → 𝐴 ∈ On) |
| 119 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ ∅ ∈ 𝐴) |
| 120 | 119 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ∅ ∈ 𝐴) |
| 121 | | omord2 8605 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑧 ∈ On ∧ (ω
↑o 𝑦)
∈ On ∧ 𝐴 ∈
On) ∧ ∅ ∈ 𝐴)
→ (𝑧 ∈ (ω
↑o 𝑦)
↔ (𝐴
·o 𝑧)
∈ (𝐴
·o (ω ↑o 𝑦)))) |
| 122 | 116, 114,
118, 120, 121 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑦) ↔ (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω
↑o 𝑦)))) |
| 123 | 109, 122 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (𝐴 ·o (ω
↑o 𝑦))) |
| 124 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) |
| 125 | 123, 124 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦)) |
| 126 | 75 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → ω ∈ (On
∖ 2o)) |
| 127 | | oeord 8626 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ ω ∈
(On ∖ 2o)) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω
↑o 𝑥))) |
| 128 | 113, 111,
126, 127 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝑦 ∈ 𝑥 ↔ (ω ↑o 𝑦) ∈ (ω
↑o 𝑥))) |
| 129 | 112, 128 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (ω
↑o 𝑦)
∈ (ω ↑o 𝑥)) |
| 130 | | ontr1 6430 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ω
↑o 𝑥)
∈ On → (((𝐴
·o 𝑧)
∈ (ω ↑o 𝑦) ∧ (ω ↑o 𝑦) ∈ (ω
↑o 𝑥))
→ (𝐴
·o 𝑧)
∈ (ω ↑o 𝑥))) |
| 131 | 106, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (((𝐴 ·o 𝑧) ∈ (ω ↑o 𝑦) ∧ (ω
↑o 𝑦)
∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥))) |
| 132 | 125, 129,
131 | mp2and 699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)) |
| 133 | | ordelss 6400 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Ord
(ω ↑o 𝑥) ∧ (𝐴 ·o 𝑧) ∈ (ω ↑o 𝑥)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)) |
| 134 | 108, 132,
133 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈
ω ∧ ∅ ∈ 𝐴) ∧ (ω ∈ On ∧ Lim 𝑥)) ∧ 𝑦 ∈ 𝑥) ∧ ((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)) |
| 135 | 134 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ 𝑦 ∈ 𝑥) → (((𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦) ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))) |
| 136 | 105, 135 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ 𝑦 ∈ 𝑥) → (((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))) |
| 137 | 136 | rexlimdva 3155 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ (∃𝑦 ∈
𝑥 ((∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) ∧ (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))) |
| 138 | 101, 137 | syl5 34 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ ((∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) ∧ ∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦))) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))) |
| 139 | 138 | expdimp 452 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (∃𝑦 ∈ 𝑥 (∅ ∈ 𝑦 ∧ 𝑧 ∈ (ω ↑o 𝑦)) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))) |
| 140 | 100, 139 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝑧 ∈ (ω ↑o 𝑥) → (𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥))) |
| 141 | 140 | ralrimiv 3145 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → ∀𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)) |
| 142 | | iunss 5045 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥) ↔ ∀𝑧 ∈ (ω
↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω
↑o 𝑥)) |
| 143 | 141, 142 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → ∪ 𝑧 ∈ (ω ↑o 𝑥)(𝐴 ·o 𝑧) ⊆ (ω ↑o 𝑥)) |
| 144 | 81, 143 | eqsstrd 4018 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝐴 ·o (ω
↑o 𝑥))
⊆ (ω ↑o 𝑥)) |
| 145 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → ∅ ∈ 𝐴) |
| 146 | | omword2 8612 |
. . . . . . . . . . . . 13
⊢
((((ω ↑o 𝑥) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (ω
↑o 𝑥)
⊆ (𝐴
·o (ω ↑o 𝑥))) |
| 147 | 72, 63, 145, 146 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (ω ↑o 𝑥) ⊆ (𝐴 ·o (ω
↑o 𝑥))) |
| 148 | 144, 147 | eqssd 4001 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
∧ ∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦))) → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥)) |
| 149 | 148 | ex 412 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ Lim 𝑥))
→ (∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥))) |
| 150 | 149 | anassrs 467 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) ∧ Lim 𝑥)
→ (∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥))) |
| 151 | 150 | a1dd 50 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) ∧ Lim 𝑥)
→ (∀𝑦 ∈
𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥)))) |
| 152 | 151 | expcom 413 |
. . . . . . 7
⊢ (Lim
𝑥 → (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) → (∀𝑦 ∈ 𝑥 (∅ ∈ 𝑦 → (𝐴 ·o (ω
↑o 𝑦)) =
(ω ↑o 𝑦)) → (∅ ∈ 𝑥 → (𝐴 ·o (ω
↑o 𝑥)) =
(ω ↑o 𝑥))))) |
| 153 | 5, 10, 15, 20, 23, 62, 152 | tfinds3 7886 |
. . . . . 6
⊢ (𝐵 ∈ On → (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) → (∅ ∈ 𝐵 → (𝐴 ·o (ω
↑o 𝐵)) =
(ω ↑o 𝐵)))) |
| 154 | 153 | com12 32 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ ω
∈ On) → (𝐵 ∈
On → (∅ ∈ 𝐵
→ (𝐴
·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)))) |
| 155 | 154 | adantrr 717 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝐵 ∈
On)) → (𝐵 ∈ On
→ (∅ ∈ 𝐵
→ (𝐴
·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)))) |
| 156 | 155 | imp32 418 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (ω
∈ On ∧ 𝐵 ∈
On)) ∧ (𝐵 ∈ On
∧ ∅ ∈ 𝐵))
→ (𝐴
·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)) |
| 157 | 156 | an32s 652 |
. 2
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈
𝐵)) ∧ (ω ∈
On ∧ 𝐵 ∈ On))
→ (𝐴
·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)) |
| 158 | | nnm0 8643 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) =
∅) |
| 159 | 158 | ad3antrrr 730 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈
𝐵)) ∧ ¬ (ω
∈ On ∧ 𝐵 ∈
On)) → (𝐴
·o ∅) = ∅) |
| 160 | | fnoe 8548 |
. . . . . . 7
⊢
↑o Fn (On × On) |
| 161 | | fndm 6671 |
. . . . . . 7
⊢ (
↑o Fn (On × On) → dom ↑o = (On
× On)) |
| 162 | 160, 161 | ax-mp 5 |
. . . . . 6
⊢ dom
↑o = (On × On) |
| 163 | 162 | ndmov 7617 |
. . . . 5
⊢ (¬
(ω ∈ On ∧ 𝐵
∈ On) → (ω ↑o 𝐵) = ∅) |
| 164 | 163 | adantl 481 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈
𝐵)) ∧ ¬ (ω
∈ On ∧ 𝐵 ∈
On)) → (ω ↑o 𝐵) = ∅) |
| 165 | 164 | oveq2d 7447 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈
𝐵)) ∧ ¬ (ω
∈ On ∧ 𝐵 ∈
On)) → (𝐴
·o (ω ↑o 𝐵)) = (𝐴 ·o
∅)) |
| 166 | 159, 165,
164 | 3eqtr4d 2787 |
. 2
⊢ ((((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈
𝐵)) ∧ ¬ (ω
∈ On ∧ 𝐵 ∈
On)) → (𝐴
·o (ω ↑o 𝐵)) = (ω ↑o 𝐵)) |
| 167 | 157, 166 | pm2.61dan 813 |
1
⊢ (((𝐴 ∈ ω ∧ ∅
∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈
𝐵)) → (𝐴 ·o (ω
↑o 𝐵)) =
(ω ↑o 𝐵)) |