Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . 3
⊢ (𝑥 = ∅ →
(1𝑜 ·𝑜 𝑥) = (1𝑜
·𝑜 ∅)) |
2 | | id 22 |
. . 3
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
3 | 1, 2 | eqeq12d 2637 |
. 2
⊢ (𝑥 = ∅ →
((1𝑜 ·𝑜 𝑥) = 𝑥 ↔ (1𝑜
·𝑜 ∅) = ∅)) |
4 | | oveq2 6658 |
. . 3
⊢ (𝑥 = 𝑦 → (1𝑜
·𝑜 𝑥) = (1𝑜
·𝑜 𝑦)) |
5 | | id 22 |
. . 3
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
6 | 4, 5 | eqeq12d 2637 |
. 2
⊢ (𝑥 = 𝑦 → ((1𝑜
·𝑜 𝑥) = 𝑥 ↔ (1𝑜
·𝑜 𝑦) = 𝑦)) |
7 | | oveq2 6658 |
. . 3
⊢ (𝑥 = suc 𝑦 → (1𝑜
·𝑜 𝑥) = (1𝑜
·𝑜 suc 𝑦)) |
8 | | id 22 |
. . 3
⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦) |
9 | 7, 8 | eqeq12d 2637 |
. 2
⊢ (𝑥 = suc 𝑦 → ((1𝑜
·𝑜 𝑥) = 𝑥 ↔ (1𝑜
·𝑜 suc 𝑦) = suc 𝑦)) |
10 | | oveq2 6658 |
. . 3
⊢ (𝑥 = 𝐴 → (1𝑜
·𝑜 𝑥) = (1𝑜
·𝑜 𝐴)) |
11 | | id 22 |
. . 3
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
12 | 10, 11 | eqeq12d 2637 |
. 2
⊢ (𝑥 = 𝐴 → ((1𝑜
·𝑜 𝑥) = 𝑥 ↔ (1𝑜
·𝑜 𝐴) = 𝐴)) |
13 | | om0x 7599 |
. 2
⊢
(1𝑜 ·𝑜 ∅) =
∅ |
14 | | 1on 7567 |
. . . . . 6
⊢
1𝑜 ∈ On |
15 | | omsuc 7606 |
. . . . . 6
⊢
((1𝑜 ∈ On ∧ 𝑦 ∈ On) → (1𝑜
·𝑜 suc 𝑦) = ((1𝑜
·𝑜 𝑦) +𝑜
1𝑜)) |
16 | 14, 15 | mpan 706 |
. . . . 5
⊢ (𝑦 ∈ On →
(1𝑜 ·𝑜 suc 𝑦) = ((1𝑜
·𝑜 𝑦) +𝑜
1𝑜)) |
17 | | oveq1 6657 |
. . . . 5
⊢
((1𝑜 ·𝑜 𝑦) = 𝑦 → ((1𝑜
·𝑜 𝑦) +𝑜
1𝑜) = (𝑦
+𝑜 1𝑜)) |
18 | 16, 17 | sylan9eq 2676 |
. . . 4
⊢ ((𝑦 ∈ On ∧
(1𝑜 ·𝑜 𝑦) = 𝑦) → (1𝑜
·𝑜 suc 𝑦) = (𝑦 +𝑜
1𝑜)) |
19 | | oa1suc 7611 |
. . . . 5
⊢ (𝑦 ∈ On → (𝑦 +𝑜
1𝑜) = suc 𝑦) |
20 | 19 | adantr 481 |
. . . 4
⊢ ((𝑦 ∈ On ∧
(1𝑜 ·𝑜 𝑦) = 𝑦) → (𝑦 +𝑜 1𝑜)
= suc 𝑦) |
21 | 18, 20 | eqtrd 2656 |
. . 3
⊢ ((𝑦 ∈ On ∧
(1𝑜 ·𝑜 𝑦) = 𝑦) → (1𝑜
·𝑜 suc 𝑦) = suc 𝑦) |
22 | 21 | ex 450 |
. 2
⊢ (𝑦 ∈ On →
((1𝑜 ·𝑜 𝑦) = 𝑦 → (1𝑜
·𝑜 suc 𝑦) = suc 𝑦)) |
23 | | iuneq2 4537 |
. . . 4
⊢
(∀𝑦 ∈
𝑥 (1𝑜
·𝑜 𝑦) = 𝑦 → ∪
𝑦 ∈ 𝑥 (1𝑜
·𝑜 𝑦) = ∪ 𝑦 ∈ 𝑥 𝑦) |
24 | | uniiun 4573 |
. . . 4
⊢ ∪ 𝑥 =
∪ 𝑦 ∈ 𝑥 𝑦 |
25 | 23, 24 | syl6eqr 2674 |
. . 3
⊢
(∀𝑦 ∈
𝑥 (1𝑜
·𝑜 𝑦) = 𝑦 → ∪
𝑦 ∈ 𝑥 (1𝑜
·𝑜 𝑦) = ∪ 𝑥) |
26 | | vex 3203 |
. . . . 5
⊢ 𝑥 ∈ V |
27 | | omlim 7613 |
. . . . . 6
⊢
((1𝑜 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (1𝑜
·𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (1𝑜
·𝑜 𝑦)) |
28 | 14, 27 | mpan 706 |
. . . . 5
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (1𝑜
·𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (1𝑜
·𝑜 𝑦)) |
29 | 26, 28 | mpan 706 |
. . . 4
⊢ (Lim
𝑥 →
(1𝑜 ·𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (1𝑜
·𝑜 𝑦)) |
30 | | limuni 5785 |
. . . 4
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑥) |
31 | 29, 30 | eqeq12d 2637 |
. . 3
⊢ (Lim
𝑥 →
((1𝑜 ·𝑜 𝑥) = 𝑥 ↔ ∪
𝑦 ∈ 𝑥 (1𝑜
·𝑜 𝑦) = ∪ 𝑥)) |
32 | 25, 31 | syl5ibr 236 |
. 2
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (1𝑜
·𝑜 𝑦) = 𝑦 → (1𝑜
·𝑜 𝑥) = 𝑥)) |
33 | 3, 6, 9, 12, 13, 22, 32 | tfinds 7059 |
1
⊢ (𝐴 ∈ On →
(1𝑜 ·𝑜 𝐴) = 𝐴) |