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∈BC

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∈BC↔B∪C=B∨B∪C=C
12 10 11 syl ⊢B∈On∧C∈On→B∪C∈BC↔B∪C=B∨B∪C=C
13 9 12 mpbird ⊢B∈On∧C∈On→B∪C∈BC