Theorem entri2

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

	Ref	Expression
Assertion	entri2	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\preccurlyeq B\vee B\prec A\right)$$

Proof

Step	Hyp	Ref	Expression
1		entric	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\prec B\vee A\approx B\vee B\prec A\right)$$
2		brdom2	$$⊢A\preccurlyeq B\leftrightarrow \left(A\prec B\vee A\approx B\right)$$
3	2	orbi1i	$$⊢\left(A\preccurlyeq B\vee B\prec A\right)\leftrightarrow \left(\left(A\prec B\vee A\approx B\right)\vee B\prec A\right)$$
4		df-3or	$$⊢\left(A\prec B\vee A\approx B\vee B\prec A\right)\leftrightarrow \left(\left(A\prec B\vee A\approx B\right)\vee B\prec A\right)$$
5	3 4	bitr4i	$$⊢\left(A\preccurlyeq B\vee B\prec A\right)\leftrightarrow \left(A\prec B\vee A\approx B\vee B\prec A\right)$$
6	1 5	sylibr	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\preccurlyeq B\vee B\prec A\right)$$