Step | Hyp | Ref
| Expression |
1 | | suceloni 4462 |
. . . . . 6
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
2 | | oav2 6412 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ suc 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥))) |
3 | 1, 2 | sylan2 284 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥))) |
4 | | df-suc 4333 |
. . . . . . . . . 10
⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) |
5 | | iuneq1 3864 |
. . . . . . . . . 10
⊢ (suc
𝐵 = (𝐵 ∪ {𝐵}) → ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +o 𝑥)) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +o 𝑥) |
7 | | iunxun 3930 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +o 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥)) |
8 | 6, 7 | eqtri 2178 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥)) |
9 | | oveq2 5834 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → (𝐴 +o 𝑥) = (𝐴 +o 𝐵)) |
10 | | suceq 4364 |
. . . . . . . . . . 11
⊢ ((𝐴 +o 𝑥) = (𝐴 +o 𝐵) → suc (𝐴 +o 𝑥) = suc (𝐴 +o 𝐵)) |
11 | 9, 10 | syl 14 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → suc (𝐴 +o 𝑥) = suc (𝐴 +o 𝐵)) |
12 | 11 | iunxsng 3926 |
. . . . . . . . 9
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥) = suc (𝐴 +o 𝐵)) |
13 | 12 | uneq2d 3262 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (∪ 𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥)) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵))) |
14 | 8, 13 | syl5eq 2202 |
. . . . . . 7
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵))) |
15 | 14 | uneq2d 3262 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝐴 ∪ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵)))) |
16 | 15 | adantl 275 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵)))) |
17 | 3, 16 | eqtrd 2190 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵)))) |
18 | | unass 3265 |
. . . 4
⊢ ((𝐴 ∪ ∪ 𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥)) ∪ suc (𝐴 +o 𝐵)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵))) |
19 | 17, 18 | eqtr4di 2208 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = ((𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥)) ∪ suc (𝐴 +o 𝐵))) |
20 | | oav2 6412 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥))) |
21 | 20 | uneq1d 3261 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵)) = ((𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥)) ∪ suc (𝐴 +o 𝐵))) |
22 | 19, 21 | eqtr4d 2193 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵))) |
23 | | sssucid 4377 |
. . 3
⊢ (𝐴 +o 𝐵) ⊆ suc (𝐴 +o 𝐵) |
24 | | ssequn1 3278 |
. . 3
⊢ ((𝐴 +o 𝐵) ⊆ suc (𝐴 +o 𝐵) ↔ ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵)) = suc (𝐴 +o 𝐵)) |
25 | 23, 24 | mpbi 144 |
. 2
⊢ ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵)) = suc (𝐴 +o 𝐵) |
26 | 22, 25 | eqtrdi 2206 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |