Metamath Proof Explorer


Theorem ordtri2

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995)

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

Proof

Step Hyp Ref Expression
1 ordsseleq
 |-  ( ( Ord B /\ Ord A ) -> ( B C_ A <-> ( B e. A \/ B = A ) ) )
2 eqcom
 |-  ( B = A <-> A = B )
3 2 orbi2i
 |-  ( ( B e. A \/ B = A ) <-> ( B e. A \/ A = B ) )
4 orcom
 |-  ( ( B e. A \/ A = B ) <-> ( A = B \/ B e. A ) )
5 3 4 bitri
 |-  ( ( B e. A \/ B = A ) <-> ( A = B \/ B e. A ) )
6 1 5 syl6bb
 |-  ( ( Ord B /\ Ord A ) -> ( B C_ A <-> ( A = B \/ B e. A ) ) )
7 ordtri1
 |-  ( ( Ord B /\ Ord A ) -> ( B C_ A <-> -. A e. B ) )
8 6 7 bitr3d
 |-  ( ( Ord B /\ Ord A ) -> ( ( A = B \/ B e. A ) <-> -. A e. B ) )
9 8 ancoms
 |-  ( ( Ord A /\ Ord B ) -> ( ( A = B \/ B e. A ) <-> -. A e. B ) )
10 9 con2bid
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )