Theorem entri3

Description: Trichotomy of dominance. This theorem is equivalent to the Axiom of Choice. Part of Proposition 4.42(d) of Mendelson p. 275. (Contributed by NM, 4-Jan-2004)

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

Proof

Step	Hyp	Ref	Expression
1		entri2	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\preccurlyeq B\vee B\prec A\right)$$
2		sdomdom	$$⊢B\prec A\to B\preccurlyeq A$$
3	2	orim2i	$$⊢\left(A\preccurlyeq B\vee B\prec A\right)\to \left(A\preccurlyeq B\vee B\preccurlyeq A\right)$$
4	1 3	syl	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\preccurlyeq B\vee B\preccurlyeq A\right)$$