| Step | Hyp | Ref
| Expression |
| 1 | | ordun 6488 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∪ 𝐵)) |
| 2 | | ordsuc 7833 |
. . . . 5
⊢ (Ord
(𝐴 ∪ 𝐵) ↔ Ord suc (𝐴 ∪ 𝐵)) |
| 3 | | ordelon 6408 |
. . . . . 6
⊢ ((Ord suc
(𝐴 ∪ 𝐵) ∧ 𝑥 ∈ suc (𝐴 ∪ 𝐵)) → 𝑥 ∈ On) |
| 4 | 3 | ex 412 |
. . . . 5
⊢ (Ord suc
(𝐴 ∪ 𝐵) → (𝑥 ∈ suc (𝐴 ∪ 𝐵) → 𝑥 ∈ On)) |
| 5 | 2, 4 | sylbi 217 |
. . . 4
⊢ (Ord
(𝐴 ∪ 𝐵) → (𝑥 ∈ suc (𝐴 ∪ 𝐵) → 𝑥 ∈ On)) |
| 6 | 1, 5 | syl 17 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝑥 ∈ suc (𝐴 ∪ 𝐵) → 𝑥 ∈ On)) |
| 7 | | ordsuc 7833 |
. . . 4
⊢ (Ord
𝐴 ↔ Ord suc 𝐴) |
| 8 | | ordsuc 7833 |
. . . 4
⊢ (Ord
𝐵 ↔ Ord suc 𝐵) |
| 9 | | ordun 6488 |
. . . . 5
⊢ ((Ord suc
𝐴 ∧ Ord suc 𝐵) → Ord (suc 𝐴 ∪ suc 𝐵)) |
| 10 | | ordelon 6408 |
. . . . . 6
⊢ ((Ord
(suc 𝐴 ∪ suc 𝐵) ∧ 𝑥 ∈ (suc 𝐴 ∪ suc 𝐵)) → 𝑥 ∈ On) |
| 11 | 10 | ex 412 |
. . . . 5
⊢ (Ord (suc
𝐴 ∪ suc 𝐵) → (𝑥 ∈ (suc 𝐴 ∪ suc 𝐵) → 𝑥 ∈ On)) |
| 12 | 9, 11 | syl 17 |
. . . 4
⊢ ((Ord suc
𝐴 ∧ Ord suc 𝐵) → (𝑥 ∈ (suc 𝐴 ∪ suc 𝐵) → 𝑥 ∈ On)) |
| 13 | 7, 8, 12 | syl2anb 598 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝑥 ∈ (suc 𝐴 ∪ suc 𝐵) → 𝑥 ∈ On)) |
| 14 | | ordssun 6486 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝑥 ⊆ (𝐴 ∪ 𝐵) ↔ (𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐵))) |
| 15 | 14 | adantl 481 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ (Ord 𝐴 ∧ Ord 𝐵)) → (𝑥 ⊆ (𝐴 ∪ 𝐵) ↔ (𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐵))) |
| 16 | | ordsssuc 6473 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ Ord (𝐴 ∪ 𝐵)) → (𝑥 ⊆ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ suc (𝐴 ∪ 𝐵))) |
| 17 | 1, 16 | sylan2 593 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ (Ord 𝐴 ∧ Ord 𝐵)) → (𝑥 ⊆ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ suc (𝐴 ∪ 𝐵))) |
| 18 | | ordsssuc 6473 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ Ord 𝐴) → (𝑥 ⊆ 𝐴 ↔ 𝑥 ∈ suc 𝐴)) |
| 19 | 18 | adantrr 717 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ (Ord 𝐴 ∧ Ord 𝐵)) → (𝑥 ⊆ 𝐴 ↔ 𝑥 ∈ suc 𝐴)) |
| 20 | | ordsssuc 6473 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ Ord 𝐵) → (𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵)) |
| 21 | 20 | adantrl 716 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ (Ord 𝐴 ∧ Ord 𝐵)) → (𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵)) |
| 22 | 19, 21 | orbi12d 919 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ (Ord 𝐴 ∧ Ord 𝐵)) → ((𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐵) ↔ (𝑥 ∈ suc 𝐴 ∨ 𝑥 ∈ suc 𝐵))) |
| 23 | 15, 17, 22 | 3bitr3d 309 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ (Ord 𝐴 ∧ Ord 𝐵)) → (𝑥 ∈ suc (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ suc 𝐴 ∨ 𝑥 ∈ suc 𝐵))) |
| 24 | | elun 4153 |
. . . . 5
⊢ (𝑥 ∈ (suc 𝐴 ∪ suc 𝐵) ↔ (𝑥 ∈ suc 𝐴 ∨ 𝑥 ∈ suc 𝐵)) |
| 25 | 23, 24 | bitr4di 289 |
. . . 4
⊢ ((𝑥 ∈ On ∧ (Ord 𝐴 ∧ Ord 𝐵)) → (𝑥 ∈ suc (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (suc 𝐴 ∪ suc 𝐵))) |
| 26 | 25 | expcom 413 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝑥 ∈ On → (𝑥 ∈ suc (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (suc 𝐴 ∪ suc 𝐵)))) |
| 27 | 6, 13, 26 | pm5.21ndd 379 |
. 2
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝑥 ∈ suc (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ (suc 𝐴 ∪ suc 𝐵))) |
| 28 | 27 | eqrdv 2735 |
1
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → suc (𝐴 ∪ 𝐵) = (suc 𝐴 ∪ suc 𝐵)) |