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

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 bitrdi 
 |-  ( ( 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 ) ) )