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