Proof of Theorem onsucunipr
| Step | Hyp | Ref
| Expression |
| 1 | | ssequn1 4186 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵) |
| 2 | | suceq 6450 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) = 𝐵 → suc (𝐴 ∪ 𝐵) = suc 𝐵) |
| 3 | 1, 2 | sylbi 217 |
. . . . 5
⊢ (𝐴 ⊆ 𝐵 → suc (𝐴 ∪ 𝐵) = suc 𝐵) |
| 4 | 3 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → suc (𝐴 ∪ 𝐵) = suc 𝐵) |
| 5 | | onsucwordi 43301 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → suc 𝐴 ⊆ suc 𝐵)) |
| 6 | 5 | imp 406 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → suc 𝐴 ⊆ suc 𝐵) |
| 7 | | ssequn1 4186 |
. . . . 5
⊢ (suc
𝐴 ⊆ suc 𝐵 ↔ (suc 𝐴 ∪ suc 𝐵) = suc 𝐵) |
| 8 | 6, 7 | sylib 218 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (suc 𝐴 ∪ suc 𝐵) = suc 𝐵) |
| 9 | 4, 8 | eqtr4d 2780 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → suc (𝐴 ∪ 𝐵) = (suc 𝐴 ∪ suc 𝐵)) |
| 10 | | ssequn2 4189 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐴 ∪ 𝐵) = 𝐴) |
| 11 | | suceq 6450 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) = 𝐴 → suc (𝐴 ∪ 𝐵) = suc 𝐴) |
| 12 | 10, 11 | sylbi 217 |
. . . . 5
⊢ (𝐵 ⊆ 𝐴 → suc (𝐴 ∪ 𝐵) = suc 𝐴) |
| 13 | 12 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → suc (𝐴 ∪ 𝐵) = suc 𝐴) |
| 14 | | onsucwordi 43301 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → (𝐵 ⊆ 𝐴 → suc 𝐵 ⊆ suc 𝐴)) |
| 15 | 14 | ancoms 458 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ 𝐴 → suc 𝐵 ⊆ suc 𝐴)) |
| 16 | 15 | imp 406 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → suc 𝐵 ⊆ suc 𝐴) |
| 17 | | ssequn2 4189 |
. . . . 5
⊢ (suc
𝐵 ⊆ suc 𝐴 ↔ (suc 𝐴 ∪ suc 𝐵) = suc 𝐴) |
| 18 | 16, 17 | sylib 218 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → (suc 𝐴 ∪ suc 𝐵) = suc 𝐴) |
| 19 | 13, 18 | eqtr4d 2780 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐵 ⊆ 𝐴) → suc (𝐴 ∪ 𝐵) = (suc 𝐴 ∪ suc 𝐵)) |
| 20 | | eloni 6394 |
. . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 21 | | eloni 6394 |
. . . 4
⊢ (𝐵 ∈ On → Ord 𝐵) |
| 22 | | ordtri2or2 6483 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |
| 23 | 20, 21, 22 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |
| 24 | 9, 19, 23 | mpjaodan 961 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc (𝐴 ∪ 𝐵) = (suc 𝐴 ∪ suc 𝐵)) |
| 25 | | uniprg 4923 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) |
| 26 | | suceq 6450 |
. . 3
⊢ (∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵) → suc ∪
{𝐴, 𝐵} = suc (𝐴 ∪ 𝐵)) |
| 27 | 25, 26 | syl 17 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc ∪ {𝐴,
𝐵} = suc (𝐴 ∪ 𝐵)) |
| 28 | | onsuc 7831 |
. . 3
⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
| 29 | | onsuc 7831 |
. . 3
⊢ (𝐵 ∈ On → suc 𝐵 ∈ On) |
| 30 | | uniprg 4923 |
. . 3
⊢ ((suc
𝐴 ∈ On ∧ suc 𝐵 ∈ On) → ∪ {suc 𝐴, suc 𝐵} = (suc 𝐴 ∪ suc 𝐵)) |
| 31 | 28, 29, 30 | syl2an 596 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∪ {suc 𝐴, suc 𝐵} = (suc 𝐴 ∪ suc 𝐵)) |
| 32 | 24, 27, 31 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc ∪ {𝐴,
𝐵} = ∪ {suc 𝐴, suc 𝐵}) |