Theorem ordtri2or2

Description: A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003)

	Ref	Expression
Assertion	ordtri2or2	|- ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )

Proof

Step	Hyp	Ref	Expression
1		ordtri2or	|- ( ( Ord A /\ Ord B ) -> ( A e. B \/ B C_ A ) )
2		ordelss	|- ( ( Ord B /\ A e. B ) -> A C_ B )
3	2	ex	|- ( Ord B -> ( A e. B -> A C_ B ) )
4	3	orim1d	|- ( Ord B -> ( ( A e. B \/ B C_ A ) -> ( A C_ B \/ B C_ A ) ) )
5	4	adantl	|- ( ( Ord A /\ Ord B ) -> ( ( A e. B \/ B C_ A ) -> ( A C_ B \/ B C_ A ) ) )
6	1 5	mpd	|- ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )