Metamath Proof Explorer

Theorem ordunpr

Description: The maximum of two ordinals is equal to one of them. (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion ordunpr ⊢ B ∈ On ∧ C ∈ On → B ∪ C ∈ B C

Proof

Step Hyp Ref Expression
1 eloni ⊢ B ∈ On → Ord ⁡ B
2 eloni ⊢ C ∈ On → Ord ⁡ C
3 ordtri2or2 ⊢ Ord ⁡ B ∧ Ord ⁡ C → B ⊆ C ∨ C ⊆ B
4 1 2 3 syl2an ⊢ B ∈ On ∧ C ∈ On → B ⊆ C ∨ C ⊆ B
5 4 orcomd ⊢ B ∈ On ∧ C ∈ On → C ⊆ B ∨ B ⊆ C
6 ssequn2 ⊢ C ⊆ B ↔ B ∪ C = B
7 ssequn1 ⊢ B ⊆ C ↔ B ∪ C = C
8 6 7 orbi12i ⊢ C ⊆ B ∨ B ⊆ C ↔ B ∪ C = B ∨ B ∪ C = C
9 5 8 sylib ⊢ B ∈ On ∧ C ∈ On → B ∪ C = B ∨ B ∪ C = C
10 unexg ⊢ B ∈ On ∧ C ∈ On → B ∪ C ∈ V
11 elprg ⊢ B ∪ C ∈ V → B ∪ C ∈ B C ↔ B ∪ C = B ∨ B ∪ C = C
12 10 11 syl ⊢ B ∈ On ∧ C ∈ On → B ∪ C ∈ B C ↔ B ∪ C = B ∨ B ∪ C = C
13 9 12 mpbird ⊢ B ∈ On ∧ C ∈ On → B ∪ C ∈ B C