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 } )