Step | Hyp | Ref
| Expression |
1 | | suceloni 4227 |
. . . . . 6
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
2 | | oav2 6043 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ suc 𝐵 ∈ On) → (𝐴 +𝑜 suc 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥))) |
3 | 1, 2 | sylan2 270 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 suc 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥))) |
4 | | df-suc 4108 |
. . . . . . . . . 10
⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) |
5 | | iuneq1 3670 |
. . . . . . . . . 10
⊢ (suc
𝐵 = (𝐵 ∪ {𝐵}) → ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥) = ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +𝑜 𝑥)) |
6 | 4, 5 | ax-mp 7 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥) = ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +𝑜 𝑥) |
7 | | iunxun 3735 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +𝑜 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +𝑜 𝑥)) |
8 | 6, 7 | eqtri 2060 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +𝑜 𝑥)) |
9 | | oveq2 5520 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝐵)) |
10 | | suceq 4139 |
. . . . . . . . . . 11
⊢ ((𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝐵) → suc (𝐴 +𝑜 𝑥) = suc (𝐴 +𝑜 𝐵)) |
11 | 9, 10 | syl 14 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → suc (𝐴 +𝑜 𝑥) = suc (𝐴 +𝑜 𝐵)) |
12 | 11 | iunxsng 3732 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ {𝐵}suc (𝐴 +𝑜 𝑥) = suc (𝐴 +𝑜 𝐵)) |
13 | 12 | uneq2d 3097 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (∪ 𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +𝑜 𝑥)) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ suc (𝐴 +𝑜 𝐵))) |
14 | 8, 13 | syl5eq 2084 |
. . . . . . 7
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ suc (𝐴 +𝑜 𝐵))) |
15 | 14 | uneq2d 3097 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝐴 ∪ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ suc (𝐴 +𝑜 𝐵)))) |
16 | 15 | adantl 262 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +𝑜 𝑥)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ suc (𝐴 +𝑜 𝐵)))) |
17 | 3, 16 | eqtrd 2072 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 suc 𝐵) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ suc (𝐴 +𝑜 𝐵)))) |
18 | | unass 3100 |
. . . 4
⊢ ((𝐴 ∪ ∪ 𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥)) ∪ suc (𝐴 +𝑜 𝐵)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥) ∪ suc (𝐴 +𝑜 𝐵))) |
19 | 17, 18 | syl6eqr 2090 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 suc 𝐵) = ((𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥)) ∪ suc (𝐴 +𝑜 𝐵))) |
20 | | oav2 6043 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥))) |
21 | 20 | uneq1d 3096 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) ∪ suc (𝐴 +𝑜 𝐵)) = ((𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +𝑜 𝑥)) ∪ suc (𝐴 +𝑜 𝐵))) |
22 | 19, 21 | eqtr4d 2075 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 suc 𝐵) = ((𝐴 +𝑜 𝐵) ∪ suc (𝐴 +𝑜 𝐵))) |
23 | | sssucid 4152 |
. . 3
⊢ (𝐴 +𝑜 𝐵) ⊆ suc (𝐴 +𝑜 𝐵) |
24 | | ssequn1 3113 |
. . 3
⊢ ((𝐴 +𝑜 𝐵) ⊆ suc (𝐴 +𝑜 𝐵) ↔ ((𝐴 +𝑜 𝐵) ∪ suc (𝐴 +𝑜 𝐵)) = suc (𝐴 +𝑜 𝐵)) |
25 | 23, 24 | mpbi 133 |
. 2
⊢ ((𝐴 +𝑜 𝐵) ∪ suc (𝐴 +𝑜 𝐵)) = suc (𝐴 +𝑜 𝐵) |
26 | 22, 25 | syl6eq 2088 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 suc 𝐵) = suc (𝐴 +𝑜 𝐵)) |