Theorem entric

Description: Trichotomy of equinumerosity and strict dominance. This theorem is equivalent to the Axiom of Choice. Theorem 8 of Suppes p. 242. (Contributed by NM, 4-Jan-2004)

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

Proof

Step	Hyp	Ref	Expression
1		domtri	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\preccurlyeq B\leftrightarrow \neg B\prec A\right)$$
2	1	biimprd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg B\prec A\to A\preccurlyeq B\right)$$
3		brdom2	$$⊢A\preccurlyeq B\leftrightarrow \left(A\prec B\vee A\approx B\right)$$
4	2 3	imbitrdi	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg B\prec A\to \left(A\prec B\vee A\approx B\right)\right)$$
5	4	con1d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\neg \left(A\prec B\vee A\approx B\right)\to B\prec A\right)$$
6	5	orrd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left(A\prec B\vee A\approx B\right)\vee B\prec A\right)$$
7		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)$$
8	6 7	sylibr	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\prec B\vee A\approx B\vee B\prec A\right)$$