| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . 3
⊢ (𝑥 = ∅ → (1o
↑o 𝑥) =
(1o ↑o ∅)) |
| 2 | 1 | eqeq1d 2739 |
. 2
⊢ (𝑥 = ∅ →
((1o ↑o 𝑥) = 1o ↔ (1o
↑o ∅) = 1o)) |
| 3 | | oveq2 7439 |
. . 3
⊢ (𝑥 = 𝑦 → (1o ↑o
𝑥) = (1o
↑o 𝑦)) |
| 4 | 3 | eqeq1d 2739 |
. 2
⊢ (𝑥 = 𝑦 → ((1o ↑o
𝑥) = 1o ↔
(1o ↑o 𝑦) = 1o)) |
| 5 | | oveq2 7439 |
. . 3
⊢ (𝑥 = suc 𝑦 → (1o ↑o
𝑥) = (1o
↑o suc 𝑦)) |
| 6 | 5 | eqeq1d 2739 |
. 2
⊢ (𝑥 = suc 𝑦 → ((1o ↑o
𝑥) = 1o ↔
(1o ↑o suc 𝑦) = 1o)) |
| 7 | | oveq2 7439 |
. . 3
⊢ (𝑥 = 𝐴 → (1o ↑o
𝑥) = (1o
↑o 𝐴)) |
| 8 | 7 | eqeq1d 2739 |
. 2
⊢ (𝑥 = 𝐴 → ((1o ↑o
𝑥) = 1o ↔
(1o ↑o 𝐴) = 1o)) |
| 9 | | 1on 8518 |
. . 3
⊢
1o ∈ On |
| 10 | | oe0 8560 |
. . 3
⊢
(1o ∈ On → (1o ↑o
∅) = 1o) |
| 11 | 9, 10 | ax-mp 5 |
. 2
⊢
(1o ↑o ∅) =
1o |
| 12 | | oesuc 8565 |
. . . . 5
⊢
((1o ∈ On ∧ 𝑦 ∈ On) → (1o
↑o suc 𝑦) =
((1o ↑o 𝑦) ·o
1o)) |
| 13 | 9, 12 | mpan 690 |
. . . 4
⊢ (𝑦 ∈ On → (1o
↑o suc 𝑦) =
((1o ↑o 𝑦) ·o
1o)) |
| 14 | | oveq1 7438 |
. . . . 5
⊢
((1o ↑o 𝑦) = 1o → ((1o
↑o 𝑦)
·o 1o) = (1o ·o
1o)) |
| 15 | | om1 8580 |
. . . . . 6
⊢
(1o ∈ On → (1o ·o
1o) = 1o) |
| 16 | 9, 15 | ax-mp 5 |
. . . . 5
⊢
(1o ·o 1o) =
1o |
| 17 | 14, 16 | eqtrdi 2793 |
. . . 4
⊢
((1o ↑o 𝑦) = 1o → ((1o
↑o 𝑦)
·o 1o) = 1o) |
| 18 | 13, 17 | sylan9eq 2797 |
. . 3
⊢ ((𝑦 ∈ On ∧ (1o
↑o 𝑦) =
1o) → (1o ↑o suc 𝑦) = 1o) |
| 19 | 18 | ex 412 |
. 2
⊢ (𝑦 ∈ On →
((1o ↑o 𝑦) = 1o → (1o
↑o suc 𝑦) =
1o)) |
| 20 | | iuneq2 5011 |
. . 3
⊢
(∀𝑦 ∈
𝑥 (1o
↑o 𝑦) =
1o → ∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦) = ∪ 𝑦 ∈ 𝑥 1o) |
| 21 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 22 | | 0lt1o 8542 |
. . . . . . . 8
⊢ ∅
∈ 1o |
| 23 | | oelim 8572 |
. . . . . . . 8
⊢
(((1o ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 1o) →
(1o ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦)) |
| 24 | 22, 23 | mpan2 691 |
. . . . . . 7
⊢
((1o ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (1o ↑o
𝑥) = ∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦)) |
| 25 | 9, 24 | mpan 690 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (1o
↑o 𝑥) =
∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦)) |
| 26 | 21, 25 | mpan 690 |
. . . . 5
⊢ (Lim
𝑥 → (1o
↑o 𝑥) =
∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦)) |
| 27 | 26 | eqeq1d 2739 |
. . . 4
⊢ (Lim
𝑥 → ((1o
↑o 𝑥) =
1o ↔ ∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦) =
1o)) |
| 28 | | 0ellim 6447 |
. . . . . 6
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
| 29 | | ne0i 4341 |
. . . . . 6
⊢ (∅
∈ 𝑥 → 𝑥 ≠ ∅) |
| 30 | | iunconst 5001 |
. . . . . 6
⊢ (𝑥 ≠ ∅ → ∪ 𝑦 ∈ 𝑥 1o =
1o) |
| 31 | 28, 29, 30 | 3syl 18 |
. . . . 5
⊢ (Lim
𝑥 → ∪ 𝑦 ∈ 𝑥 1o =
1o) |
| 32 | 31 | eqeq2d 2748 |
. . . 4
⊢ (Lim
𝑥 → (∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦) = ∪ 𝑦 ∈ 𝑥 1o ↔ ∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦) =
1o)) |
| 33 | 27, 32 | bitr4d 282 |
. . 3
⊢ (Lim
𝑥 → ((1o
↑o 𝑥) =
1o ↔ ∪ 𝑦 ∈ 𝑥 (1o ↑o 𝑦) = ∪ 𝑦 ∈ 𝑥 1o)) |
| 34 | 20, 33 | imbitrrid 246 |
. 2
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (1o ↑o 𝑦) = 1o →
(1o ↑o 𝑥) = 1o)) |
| 35 | 2, 4, 6, 8, 11, 19, 34 | tfinds 7881 |
1
⊢ (𝐴 ∈ On → (1o
↑o 𝐴) =
1o) |