Metamath Proof Explorer

Theorem ordssun

Description: Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordssun ⊢ Ord ⁡ B ∧ Ord ⁡ C → A ⊆ B ∪ C ↔ A ⊆ B ∨ A ⊆ C

Proof

Step Hyp Ref Expression
1 ordtri2or2 ⊢ Ord ⁡ B ∧ Ord ⁡ C → B ⊆ C ∨ C ⊆ B
2 ssequn1 ⊢ B ⊆ C ↔ B ∪ C = C
3 sseq2 ⊢ B ∪ C = C → A ⊆ B ∪ C ↔ A ⊆ C
4 2 3 sylbi ⊢ B ⊆ C → A ⊆ B ∪ C ↔ A ⊆ C
5 olc ⊢ A ⊆ C → A ⊆ B ∨ A ⊆ C
6 4 5 biimtrdi ⊢ B ⊆ C → A ⊆ B ∪ C → A ⊆ B ∨ A ⊆ C
7 ssequn2 ⊢ C ⊆ B ↔ B ∪ C = B
8 sseq2 ⊢ B ∪ C = B → A ⊆ B ∪ C ↔ A ⊆ B
9 7 8 sylbi ⊢ C ⊆ B → A ⊆ B ∪ C ↔ A ⊆ B
10 orc ⊢ A ⊆ B → A ⊆ B ∨ A ⊆ C
11 9 10 biimtrdi ⊢ C ⊆ B → A ⊆ B ∪ C → A ⊆ B ∨ A ⊆ C
12 6 11 jaoi ⊢ B ⊆ C ∨ C ⊆ B → A ⊆ B ∪ C → A ⊆ B ∨ A ⊆ C
13 1 12 syl ⊢ Ord ⁡ B ∧ Ord ⁡ C → A ⊆ B ∪ C → A ⊆ B ∨ A ⊆ C
14 ssun ⊢ A ⊆ B ∨ A ⊆ C → A ⊆ B ∪ C
15 13 14 impbid1 ⊢ Ord ⁡ B ∧ Ord ⁡ C → A ⊆ B ∪ C ↔ A ⊆ B ∨ A ⊆ C