Metamath Proof Explorer

Theorem ordtri4

Description: A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 eqss 
 |-  ( A = B <-> ( A C_ B /\ B C_ A ) )
2 ordtri1 
 |-  ( ( Ord B /\ Ord A ) -> ( B C_ A <-> -. A e. B ) )
3 2 ancoms 
 |-  ( ( Ord A /\ Ord B ) -> ( B C_ A <-> -. A e. B ) )
4 3 anbi2d 
 |-  ( ( Ord A /\ Ord B ) -> ( ( A C_ B /\ B C_ A ) <-> ( A C_ B /\ -. A e. B ) ) )
5 1 4 bitrid 
 |-  ( ( Ord A /\ Ord B ) -> ( A = B <-> ( A C_ B /\ -. A e. B ) ) )