Theorem entri2

Description: Trichotomy of dominance and strict dominance. (Contributed by NM, 4-Jan-2004)

	Ref	Expression
Assertion	entri2	|- ( ( A e. V /\ B e. W ) -> ( A ~<_ B \/ B ~< A ) )

Proof

Step	Hyp	Ref	Expression
1		entric	|- ( ( A e. V /\ B e. W ) -> ( A ~< B \/ A ~~ B \/ B ~< A ) )
2		brdom2	|- ( A ~<_ B <-> ( A ~< B \/ A ~~ B ) )
3	2	orbi1i	|- ( ( A ~<_ B \/ B ~< A ) <-> ( ( A ~< B \/ A ~~ B ) \/ B ~< A ) )
4		df-3or	|- ( ( A ~< B \/ A ~~ B \/ B ~< A ) <-> ( ( A ~< B \/ A ~~ B ) \/ B ~< A ) )
5	3 4	bitr4i	|- ( ( A ~<_ B \/ B ~< A ) <-> ( A ~< B \/ A ~~ B \/ B ~< A ) )
6	1 5	sylibr	|- ( ( A e. V /\ B e. W ) -> ( A ~<_ B \/ B ~< A ) )