Metamath Proof Explorer

Theorem ordequn

Description: The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of TakeutiZaring p. 40. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordequn ⊢ 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 1 orcomd ⊢ Ord ⁡ B ∧ Ord ⁡ C → C ⊆ B ∨ B ⊆ C
3 ssequn2 ⊢ C ⊆ B ↔ B ∪ C = B
4 eqeq1 ⊢ A = B ∪ C → A = B ↔ B ∪ C = B
5 3 4 bitr4id ⊢ A = B ∪ C → C ⊆ B ↔ A = B
6 ssequn1 ⊢ B ⊆ C ↔ B ∪ C = C
7 eqeq1 ⊢ A = B ∪ C → A = C ↔ B ∪ C = C
8 6 7 bitr4id ⊢ A = B ∪ C → B ⊆ C ↔ A = C
9 5 8 orbi12d ⊢ A = B ∪ C → C ⊆ B ∨ B ⊆ C ↔ A = B ∨ A = C
10 2 9 syl5ibcom ⊢ Ord ⁡ B ∧ Ord ⁡ C → A = B ∪ C → A = B ∨ A = C