Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . 3
⊢ (𝑥 = ∅ →
(1𝑜 ↑𝑜 𝑥) = (1𝑜
↑𝑜 ∅)) |
2 | 1 | eqeq1d 2624 |
. 2
⊢ (𝑥 = ∅ →
((1𝑜 ↑𝑜 𝑥) = 1𝑜 ↔
(1𝑜 ↑𝑜 ∅) =
1𝑜)) |
3 | | oveq2 6658 |
. . 3
⊢ (𝑥 = 𝑦 → (1𝑜
↑𝑜 𝑥) = (1𝑜
↑𝑜 𝑦)) |
4 | 3 | eqeq1d 2624 |
. 2
⊢ (𝑥 = 𝑦 → ((1𝑜
↑𝑜 𝑥) = 1𝑜 ↔
(1𝑜 ↑𝑜 𝑦) = 1𝑜)) |
5 | | oveq2 6658 |
. . 3
⊢ (𝑥 = suc 𝑦 → (1𝑜
↑𝑜 𝑥) = (1𝑜
↑𝑜 suc 𝑦)) |
6 | 5 | eqeq1d 2624 |
. 2
⊢ (𝑥 = suc 𝑦 → ((1𝑜
↑𝑜 𝑥) = 1𝑜 ↔
(1𝑜 ↑𝑜 suc 𝑦) = 1𝑜)) |
7 | | oveq2 6658 |
. . 3
⊢ (𝑥 = 𝐴 → (1𝑜
↑𝑜 𝑥) = (1𝑜
↑𝑜 𝐴)) |
8 | 7 | eqeq1d 2624 |
. 2
⊢ (𝑥 = 𝐴 → ((1𝑜
↑𝑜 𝑥) = 1𝑜 ↔
(1𝑜 ↑𝑜 𝐴) = 1𝑜)) |
9 | | 1on 7567 |
. . 3
⊢
1𝑜 ∈ On |
10 | | oe0 7602 |
. . 3
⊢
(1𝑜 ∈ On → (1𝑜
↑𝑜 ∅) = 1𝑜) |
11 | 9, 10 | ax-mp 5 |
. 2
⊢
(1𝑜 ↑𝑜 ∅) =
1𝑜 |
12 | | oesuc 7607 |
. . . . 5
⊢
((1𝑜 ∈ On ∧ 𝑦 ∈ On) → (1𝑜
↑𝑜 suc 𝑦) = ((1𝑜
↑𝑜 𝑦) ·𝑜
1𝑜)) |
13 | 9, 12 | mpan 706 |
. . . 4
⊢ (𝑦 ∈ On →
(1𝑜 ↑𝑜 suc 𝑦) = ((1𝑜
↑𝑜 𝑦) ·𝑜
1𝑜)) |
14 | | oveq1 6657 |
. . . . 5
⊢
((1𝑜 ↑𝑜 𝑦) = 1𝑜 →
((1𝑜 ↑𝑜 𝑦) ·𝑜
1𝑜) = (1𝑜 ·𝑜
1𝑜)) |
15 | | om1 7622 |
. . . . . 6
⊢
(1𝑜 ∈ On → (1𝑜
·𝑜 1𝑜) =
1𝑜) |
16 | 9, 15 | ax-mp 5 |
. . . . 5
⊢
(1𝑜 ·𝑜
1𝑜) = 1𝑜 |
17 | 14, 16 | syl6eq 2672 |
. . . 4
⊢
((1𝑜 ↑𝑜 𝑦) = 1𝑜 →
((1𝑜 ↑𝑜 𝑦) ·𝑜
1𝑜) = 1𝑜) |
18 | 13, 17 | sylan9eq 2676 |
. . 3
⊢ ((𝑦 ∈ On ∧
(1𝑜 ↑𝑜 𝑦) = 1𝑜) →
(1𝑜 ↑𝑜 suc 𝑦) = 1𝑜) |
19 | 18 | ex 450 |
. 2
⊢ (𝑦 ∈ On →
((1𝑜 ↑𝑜 𝑦) = 1𝑜 →
(1𝑜 ↑𝑜 suc 𝑦) = 1𝑜)) |
20 | | iuneq2 4537 |
. . 3
⊢
(∀𝑦 ∈
𝑥 (1𝑜
↑𝑜 𝑦) = 1𝑜 → ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦) = ∪ 𝑦 ∈ 𝑥 1𝑜) |
21 | | vex 3203 |
. . . . . 6
⊢ 𝑥 ∈ V |
22 | | 0lt1o 7584 |
. . . . . . . 8
⊢ ∅
∈ 1𝑜 |
23 | | oelim 7614 |
. . . . . . . 8
⊢
(((1𝑜 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈
1𝑜) → (1𝑜 ↑𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦)) |
24 | 22, 23 | mpan2 707 |
. . . . . . 7
⊢
((1𝑜 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (1𝑜
↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦)) |
25 | 9, 24 | mpan 706 |
. . . . . 6
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (1𝑜
↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦)) |
26 | 21, 25 | mpan 706 |
. . . . 5
⊢ (Lim
𝑥 →
(1𝑜 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦)) |
27 | 26 | eqeq1d 2624 |
. . . 4
⊢ (Lim
𝑥 →
((1𝑜 ↑𝑜 𝑥) = 1𝑜 ↔ ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦) = 1𝑜)) |
28 | | 0ellim 5787 |
. . . . . 6
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
29 | | ne0i 3921 |
. . . . . 6
⊢ (∅
∈ 𝑥 → 𝑥 ≠ ∅) |
30 | | iunconst 4529 |
. . . . . 6
⊢ (𝑥 ≠ ∅ → ∪ 𝑦 ∈ 𝑥 1𝑜 =
1𝑜) |
31 | 28, 29, 30 | 3syl 18 |
. . . . 5
⊢ (Lim
𝑥 → ∪ 𝑦 ∈ 𝑥 1𝑜 =
1𝑜) |
32 | 31 | eqeq2d 2632 |
. . . 4
⊢ (Lim
𝑥 → (∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦) = ∪ 𝑦 ∈ 𝑥 1𝑜 ↔ ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦) = 1𝑜)) |
33 | 27, 32 | bitr4d 271 |
. . 3
⊢ (Lim
𝑥 →
((1𝑜 ↑𝑜 𝑥) = 1𝑜 ↔ ∪ 𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦) = ∪ 𝑦 ∈ 𝑥 1𝑜)) |
34 | 20, 33 | syl5ibr 236 |
. 2
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (1𝑜
↑𝑜 𝑦) = 1𝑜 →
(1𝑜 ↑𝑜 𝑥) = 1𝑜)) |
35 | 2, 4, 6, 8, 11, 19, 34 | tfinds 7059 |
1
⊢ (𝐴 ∈ On →
(1𝑜 ↑𝑜 𝐴) = 1𝑜) |