| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . 3
⊢ (𝑥 = ∅ → (1o
·o 𝑥) =
(1o ·o ∅)) | 
| 2 |  | id 22 | . . 3
⊢ (𝑥 = ∅ → 𝑥 = ∅) | 
| 3 | 1, 2 | eqeq12d 2752 | . 2
⊢ (𝑥 = ∅ →
((1o ·o 𝑥) = 𝑥 ↔ (1o ·o
∅) = ∅)) | 
| 4 |  | oveq2 7440 | . . 3
⊢ (𝑥 = 𝑦 → (1o ·o
𝑥) = (1o
·o 𝑦)) | 
| 5 |  | id 22 | . . 3
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | 
| 6 | 4, 5 | eqeq12d 2752 | . 2
⊢ (𝑥 = 𝑦 → ((1o ·o
𝑥) = 𝑥 ↔ (1o ·o
𝑦) = 𝑦)) | 
| 7 |  | oveq2 7440 | . . 3
⊢ (𝑥 = suc 𝑦 → (1o ·o
𝑥) = (1o
·o suc 𝑦)) | 
| 8 |  | id 22 | . . 3
⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦) | 
| 9 | 7, 8 | eqeq12d 2752 | . 2
⊢ (𝑥 = suc 𝑦 → ((1o ·o
𝑥) = 𝑥 ↔ (1o ·o
suc 𝑦) = suc 𝑦)) | 
| 10 |  | oveq2 7440 | . . 3
⊢ (𝑥 = 𝐴 → (1o ·o
𝑥) = (1o
·o 𝐴)) | 
| 11 |  | id 22 | . . 3
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | 
| 12 | 10, 11 | eqeq12d 2752 | . 2
⊢ (𝑥 = 𝐴 → ((1o ·o
𝑥) = 𝑥 ↔ (1o ·o
𝐴) = 𝐴)) | 
| 13 |  | 1on 8519 | . . 3
⊢
1o ∈ On | 
| 14 |  | om0 8556 | . . 3
⊢
(1o ∈ On → (1o ·o
∅) = ∅) | 
| 15 | 13, 14 | ax-mp 5 | . 2
⊢
(1o ·o ∅) = ∅ | 
| 16 |  | omsuc 8565 | . . . . . 6
⊢
((1o ∈ On ∧ 𝑦 ∈ On) → (1o
·o suc 𝑦)
= ((1o ·o 𝑦) +o
1o)) | 
| 17 | 13, 16 | mpan 690 | . . . . 5
⊢ (𝑦 ∈ On → (1o
·o suc 𝑦)
= ((1o ·o 𝑦) +o
1o)) | 
| 18 |  | oveq1 7439 | . . . . 5
⊢
((1o ·o 𝑦) = 𝑦 → ((1o ·o
𝑦) +o
1o) = (𝑦
+o 1o)) | 
| 19 | 17, 18 | sylan9eq 2796 | . . . 4
⊢ ((𝑦 ∈ On ∧ (1o
·o 𝑦) =
𝑦) → (1o
·o suc 𝑦)
= (𝑦 +o
1o)) | 
| 20 |  | oa1suc 8570 | . . . . 5
⊢ (𝑦 ∈ On → (𝑦 +o 1o) =
suc 𝑦) | 
| 21 | 20 | adantr 480 | . . . 4
⊢ ((𝑦 ∈ On ∧ (1o
·o 𝑦) =
𝑦) → (𝑦 +o 1o) =
suc 𝑦) | 
| 22 | 19, 21 | eqtrd 2776 | . . 3
⊢ ((𝑦 ∈ On ∧ (1o
·o 𝑦) =
𝑦) → (1o
·o suc 𝑦)
= suc 𝑦) | 
| 23 | 22 | ex 412 | . 2
⊢ (𝑦 ∈ On →
((1o ·o 𝑦) = 𝑦 → (1o ·o
suc 𝑦) = suc 𝑦)) | 
| 24 |  | iuneq2 5010 | . . . 4
⊢
(∀𝑦 ∈
𝑥 (1o
·o 𝑦) =
𝑦 → ∪ 𝑦 ∈ 𝑥 (1o ·o 𝑦) = ∪ 𝑦 ∈ 𝑥 𝑦) | 
| 25 |  | uniiun 5057 | . . . 4
⊢ ∪ 𝑥 =
∪ 𝑦 ∈ 𝑥 𝑦 | 
| 26 | 24, 25 | eqtr4di 2794 | . . 3
⊢
(∀𝑦 ∈
𝑥 (1o
·o 𝑦) =
𝑦 → ∪ 𝑦 ∈ 𝑥 (1o ·o 𝑦) = ∪
𝑥) | 
| 27 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 28 |  | omlim 8572 | . . . . . 6
⊢
((1o ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (1o ·o
𝑥) = ∪ 𝑦 ∈ 𝑥 (1o ·o 𝑦)) | 
| 29 | 13, 28 | mpan 690 | . . . . 5
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (1o
·o 𝑥) =
∪ 𝑦 ∈ 𝑥 (1o ·o 𝑦)) | 
| 30 | 27, 29 | mpan 690 | . . . 4
⊢ (Lim
𝑥 → (1o
·o 𝑥) =
∪ 𝑦 ∈ 𝑥 (1o ·o 𝑦)) | 
| 31 |  | limuni 6444 | . . . 4
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑥) | 
| 32 | 30, 31 | eqeq12d 2752 | . . 3
⊢ (Lim
𝑥 → ((1o
·o 𝑥) =
𝑥 ↔ ∪ 𝑦 ∈ 𝑥 (1o ·o 𝑦) = ∪
𝑥)) | 
| 33 | 26, 32 | imbitrrid 246 | . 2
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (1o ·o 𝑦) = 𝑦 → (1o ·o
𝑥) = 𝑥)) | 
| 34 | 3, 6, 9, 12, 15, 23, 33 | tfinds 7882 | 1
⊢ (𝐴 ∈ On → (1o
·o 𝐴) =
𝐴) |