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