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

Metamath Proof Explorer

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 )