This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. On /\ C e. On ) -> ( B u. C ) e. { B , C } )

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( B e. On -> Ord B )
2 eloni 
 |-  ( C e. On -> Ord C )
3 ordtri2or2 
 |-  ( ( Ord B /\ Ord C ) -> ( B C_ C \/ C C_ B ) )
4 1 2 3 syl2an 
 |-  ( ( B e. On /\ C e. On ) -> ( B C_ C \/ C C_ B ) )
5 4 orcomd 
 |-  ( ( B e. On /\ C e. On ) -> ( C C_ B \/ B C_ C ) )
6 ssequn2 
 |-  ( C C_ B <-> ( B u. C ) = B )
7 ssequn1 
 |-  ( B C_ C <-> ( B u. C ) = C )
8 6 7 orbi12i 
 |-  ( ( C C_ B \/ B C_ C ) <-> ( ( B u. C ) = B \/ ( B u. C ) = C ) )
9 5 8 sylib 
 |-  ( ( B e. On /\ C e. On ) -> ( ( B u. C ) = B \/ ( B u. C ) = C ) )
10 unexg 
 |-  ( ( B e. On /\ C e. On ) -> ( B u. C ) e. _V )
11 elprg 
 |-  ( ( B u. C ) e. _V -> ( ( B u. C ) e. { B , C } <-> ( ( B u. C ) = B \/ ( B u. C ) = C ) ) )
12 10 11 syl 
 |-  ( ( B e. On /\ C e. On ) -> ( ( B u. C ) e. { B , C } <-> ( ( B u. C ) = B \/ ( B u. C ) = C ) ) )
13 9 12 mpbird 
 |-  ( ( B e. On /\ C e. On ) -> ( B u. C ) e. { B , C } )