Metamath Proof Explorer

Theorem ordtri2or

Description: A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ordtri2or 
|- ( ( Ord A /\ Ord B ) -> ( A e. B \/ B C_ A ) )

Proof

Step Hyp Ref Expression
1 ordtri1 
 |-  ( ( Ord B /\ Ord A ) -> ( B C_ A <-> -. A e. B ) )
2 1 ancoms 
 |-  ( ( Ord A /\ Ord B ) -> ( B C_ A <-> -. A e. B ) )
3 2 biimprd 
 |-  ( ( Ord A /\ Ord B ) -> ( -. A e. B -> B C_ A ) )
4 3 orrd 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B \/ B C_ A ) )