Step | Hyp | Ref
| Expression |
1 | | omfnex 6052 |
. . . 4
⊢ (𝐴 ∈ On → (𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)) Fn V) |
2 | | 0elon 4147 |
. . . . 5
⊢ ∅
∈ On |
3 | | rdgival 5992 |
. . . . 5
⊢ (((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)) Fn V ∧ ∅ ∈ On
∧ 𝐵 ∈ On) →
(rec((𝑦 ∈ V ↦
(𝑦 +𝑜
𝐴)), ∅)‘𝐵) = (∅ ∪ ∪ 𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥)))) |
4 | 2, 3 | mp3an2 1256 |
. . . 4
⊢ (((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)) Fn V ∧ 𝐵 ∈ On) → (rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝐵) = (∅ ∪ ∪ 𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥)))) |
5 | 1, 4 | sylan 277 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝐵) = (∅ ∪ ∪ 𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥)))) |
6 | | omv 6058 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) = (rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝐵)) |
7 | | onelon 4139 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
8 | | omexg 6054 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
𝑥) ∈
V) |
9 | | omcl 6064 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
𝑥) ∈
On) |
10 | | simpl 107 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
11 | | oacl 6063 |
. . . . . . . . . 10
⊢ (((𝐴 ·𝑜
𝑥) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·𝑜
𝑥) +𝑜
𝐴) ∈
On) |
12 | 9, 10, 11 | syl2anc 403 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((𝐴 ·𝑜
𝑥) +𝑜
𝐴) ∈
On) |
13 | | oveq1 5539 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 ·𝑜 𝑥) → (𝑦 +𝑜 𝐴) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
14 | | eqid 2081 |
. . . . . . . . . 10
⊢ (𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)) = (𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)) |
15 | 13, 14 | fvmptg 5269 |
. . . . . . . . 9
⊢ (((𝐴 ·𝑜
𝑥) ∈ V ∧ ((𝐴 ·𝑜
𝑥) +𝑜
𝐴) ∈ On) →
((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(𝐴 ·𝑜 𝑥)) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
16 | 8, 12, 15 | syl2anc 403 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(𝐴 ·𝑜 𝑥)) = ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |
17 | | omv 6058 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ·𝑜
𝑥) = (rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥)) |
18 | 17 | fveq2d 5202 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(𝐴 ·𝑜 𝑥)) = ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥))) |
19 | 16, 18 | eqtr3d 2115 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((𝐴 ·𝑜
𝑥) +𝑜
𝐴) = ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥))) |
20 | 7, 19 | sylan2 280 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑥 ∈ 𝐵)) → ((𝐴 ·𝑜 𝑥) +𝑜 𝐴) = ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥))) |
21 | 20 | anassrs 392 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ 𝐵) → ((𝐴 ·𝑜 𝑥) +𝑜 𝐴) = ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥))) |
22 | 21 | iuneq2dv 3699 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴) = ∪ 𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥))) |
23 | 22 | uneq2d 3126 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∪ ∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) = (∅ ∪ ∪ 𝑥 ∈ 𝐵 ((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴))‘(rec((𝑦 ∈ V ↦ (𝑦 +𝑜 𝐴)), ∅)‘𝑥)))) |
24 | 5, 6, 23 | 3eqtr4d 2123 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) = (∅ ∪
∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴))) |
25 | | uncom 3116 |
. . 3
⊢ (∅
∪ ∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) = (∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴) ∪
∅) |
26 | | un0 3278 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴) ∪ ∅) = ∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴) |
27 | 25, 26 | eqtri 2101 |
. 2
⊢ (∅
∪ ∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) = ∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴) |
28 | 24, 27 | syl6eq 2129 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) = ∪ 𝑥 ∈ 𝐵 ((𝐴 ·𝑜 𝑥) +𝑜 𝐴)) |