Step | Hyp | Ref
| Expression |
1 | | df-suc 4354 |
. . . . . . 7
⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) |
2 | | iuneq1 3884 |
. . . . . . 7
⊢ (suc
𝐵 = (𝐵 ∪ {𝐵}) → ∪ 𝑥 ∈ suc 𝐵((𝐴 ·o 𝑥) +o 𝐴) = ∪
𝑥 ∈ (𝐵 ∪ {𝐵})((𝐴 ·o 𝑥) +o 𝐴)) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ ∪ 𝑥 ∈ suc 𝐵((𝐴 ·o 𝑥) +o 𝐴) = ∪
𝑥 ∈ (𝐵 ∪ {𝐵})((𝐴 ·o 𝑥) +o 𝐴) |
4 | | iunxun 3950 |
. . . . . 6
⊢ ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})((𝐴 ·o 𝑥) +o 𝐴) = (∪
𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴) ∪ ∪
𝑥 ∈ {𝐵} ((𝐴 ·o 𝑥) +o 𝐴)) |
5 | 3, 4 | eqtri 2191 |
. . . . 5
⊢ ∪ 𝑥 ∈ suc 𝐵((𝐴 ·o 𝑥) +o 𝐴) = (∪
𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴) ∪ ∪
𝑥 ∈ {𝐵} ((𝐴 ·o 𝑥) +o 𝐴)) |
6 | | oveq2 5859 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝐵)) |
7 | 6 | oveq1d 5866 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → ((𝐴 ·o 𝑥) +o 𝐴) = ((𝐴 ·o 𝐵) +o 𝐴)) |
8 | 7 | iunxsng 3946 |
. . . . . 6
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ {𝐵} ((𝐴 ·o 𝑥) +o 𝐴) = ((𝐴 ·o 𝐵) +o 𝐴)) |
9 | 8 | uneq2d 3281 |
. . . . 5
⊢ (𝐵 ∈ On → (∪ 𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴) ∪ ∪
𝑥 ∈ {𝐵} ((𝐴 ·o 𝑥) +o 𝐴)) = (∪
𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴) ∪ ((𝐴 ·o 𝐵) +o 𝐴))) |
10 | 5, 9 | eqtrid 2215 |
. . . 4
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ suc 𝐵((𝐴 ·o 𝑥) +o 𝐴) = (∪
𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴) ∪ ((𝐴 ·o 𝐵) +o 𝐴))) |
11 | 10 | adantl 275 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∪ 𝑥 ∈ suc 𝐵((𝐴 ·o 𝑥) +o 𝐴) = (∪
𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴) ∪ ((𝐴 ·o 𝐵) +o 𝐴))) |
12 | | suceloni 4483 |
. . . 4
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
13 | | omv2 6442 |
. . . 4
⊢ ((𝐴 ∈ On ∧ suc 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ∪ 𝑥 ∈ suc 𝐵((𝐴 ·o 𝑥) +o 𝐴)) |
14 | 12, 13 | sylan2 284 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ∪ 𝑥 ∈ suc 𝐵((𝐴 ·o 𝑥) +o 𝐴)) |
15 | | omv2 6442 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) = ∪ 𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴)) |
16 | 15 | uneq1d 3280 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) ∪ ((𝐴 ·o 𝐵) +o 𝐴)) = (∪
𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴) ∪ ((𝐴 ·o 𝐵) +o 𝐴))) |
17 | 11, 14, 16 | 3eqtr4d 2213 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) ∪ ((𝐴 ·o 𝐵) +o 𝐴))) |
18 | | omcl 6438 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
19 | | simpl 108 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ∈ On) |
20 | | oaword1 6448 |
. . . 4
⊢ (((𝐴 ·o 𝐵) ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·o 𝐵) ⊆ ((𝐴 ·o 𝐵) +o 𝐴)) |
21 | | ssequn1 3297 |
. . . 4
⊢ ((𝐴 ·o 𝐵) ⊆ ((𝐴 ·o 𝐵) +o 𝐴) ↔ ((𝐴 ·o 𝐵) ∪ ((𝐴 ·o 𝐵) +o 𝐴)) = ((𝐴 ·o 𝐵) +o 𝐴)) |
22 | 20, 21 | sylib 121 |
. . 3
⊢ (((𝐴 ·o 𝐵) ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·o 𝐵) ∪ ((𝐴 ·o 𝐵) +o 𝐴)) = ((𝐴 ·o 𝐵) +o 𝐴)) |
23 | 18, 19, 22 | syl2anc 409 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) ∪ ((𝐴 ·o 𝐵) +o 𝐴)) = ((𝐴 ·o 𝐵) +o 𝐴)) |
24 | 17, 23 | eqtrd 2203 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) |