| Step | Hyp | Ref
 | Expression | 
| 1 |   | onsuc 4537 | 
. . . . . 6
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) | 
| 2 |   | oav2 6521 | 
. . . . . 6
⊢ ((𝐴 ∈ On ∧ suc 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥))) | 
| 3 | 1, 2 | sylan2 286 | 
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥))) | 
| 4 |   | df-suc 4406 | 
. . . . . . . . . 10
⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | 
| 5 |   | iuneq1 3929 | 
. . . . . . . . . 10
⊢ (suc
𝐵 = (𝐵 ∪ {𝐵}) → ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +o 𝑥)) | 
| 6 | 4, 5 | ax-mp 5 | 
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +o 𝑥) | 
| 7 |   | iunxun 3996 | 
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ (𝐵 ∪ {𝐵})suc (𝐴 +o 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥)) | 
| 8 | 6, 7 | eqtri 2217 | 
. . . . . . . 8
⊢ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥)) | 
| 9 |   | oveq2 5930 | 
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → (𝐴 +o 𝑥) = (𝐴 +o 𝐵)) | 
| 10 |   | suceq 4437 | 
. . . . . . . . . . 11
⊢ ((𝐴 +o 𝑥) = (𝐴 +o 𝐵) → suc (𝐴 +o 𝑥) = suc (𝐴 +o 𝐵)) | 
| 11 | 9, 10 | syl 14 | 
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → suc (𝐴 +o 𝑥) = suc (𝐴 +o 𝐵)) | 
| 12 | 11 | iunxsng 3992 | 
. . . . . . . . 9
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥) = suc (𝐴 +o 𝐵)) | 
| 13 | 12 | uneq2d 3317 | 
. . . . . . . 8
⊢ (𝐵 ∈ On → (∪ 𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ ∪
𝑥 ∈ {𝐵}suc (𝐴 +o 𝑥)) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵))) | 
| 14 | 8, 13 | eqtrid 2241 | 
. . . . . . 7
⊢ (𝐵 ∈ On → ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥) = (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵))) | 
| 15 | 14 | uneq2d 3317 | 
. . . . . 6
⊢ (𝐵 ∈ On → (𝐴 ∪ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵)))) | 
| 16 | 15 | adantl 277 | 
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ ∪ 𝑥 ∈ suc 𝐵 suc (𝐴 +o 𝑥)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵)))) | 
| 17 | 3, 16 | eqtrd 2229 | 
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵)))) | 
| 18 |   | unass 3320 | 
. . . 4
⊢ ((𝐴 ∪ ∪ 𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥)) ∪ suc (𝐴 +o 𝐵)) = (𝐴 ∪ (∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥) ∪ suc (𝐴 +o 𝐵))) | 
| 19 | 17, 18 | eqtr4di 2247 | 
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = ((𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥)) ∪ suc (𝐴 +o 𝐵))) | 
| 20 |   | oav2 6521 | 
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥))) | 
| 21 | 20 | uneq1d 3316 | 
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵)) = ((𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥)) ∪ suc (𝐴 +o 𝐵))) | 
| 22 | 19, 21 | eqtr4d 2232 | 
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵))) | 
| 23 |   | sssucid 4450 | 
. . 3
⊢ (𝐴 +o 𝐵) ⊆ suc (𝐴 +o 𝐵) | 
| 24 |   | ssequn1 3333 | 
. . 3
⊢ ((𝐴 +o 𝐵) ⊆ suc (𝐴 +o 𝐵) ↔ ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵)) = suc (𝐴 +o 𝐵)) | 
| 25 | 23, 24 | mpbi 145 | 
. 2
⊢ ((𝐴 +o 𝐵) ∪ suc (𝐴 +o 𝐵)) = suc (𝐴 +o 𝐵) | 
| 26 | 22, 25 | eqtrdi 2245 | 
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |