Theorem ordunel

Description: The maximum of two ordinals belongs to a third if each of them do. (Contributed by NM, 18-Sep-2006) (Revised by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Assertion	ordunel	|- ( ( Ord A /\ B e. A /\ C e. A ) -> ( B u. C ) e. A )

Proof

Step	Hyp	Ref	Expression
1		prssi	|- ( ( B e. A /\ C e. A ) -> { B , C } C_ A )
2	1	3adant1	|- ( ( Ord A /\ B e. A /\ C e. A ) -> { B , C } C_ A )
3		ordelon	|- ( ( Ord A /\ B e. A ) -> B e. On )
4	3	3adant3	|- ( ( Ord A /\ B e. A /\ C e. A ) -> B e. On )
5		ordelon	|- ( ( Ord A /\ C e. A ) -> C e. On )
6		ordunpr	|- ( ( B e. On /\ C e. On ) -> ( B u. C ) e. { B , C } )
7	4 5 6	3imp3i2an	|- ( ( Ord A /\ B e. A /\ C e. A ) -> ( B u. C ) e. { B , C } )
8	2 7	sseldd	|- ( ( Ord A /\ B e. A /\ C e. A ) -> ( B u. C ) e. A )