Theorem fidomtri2

Description: Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 7-May-2015)

	Ref	Expression
Assertion	fidomtri2	$$⊢\left(A\in V\wedge B\in \mathrm{Fin}\right)\to \left(A\preccurlyeq B\leftrightarrow \neg B\prec A\right)$$

Proof

Step	Hyp	Ref	Expression
1		domnsym	$$⊢A\preccurlyeq B\to \neg B\prec A$$
2		sdomdom	$$⊢A\prec B\to A\preccurlyeq B$$
3	2	con3i	$$⊢\neg A\preccurlyeq B\to \neg A\prec B$$
4		fidomtri	$$⊢\left(B\in \mathrm{Fin}\wedge A\in V\right)\to \left(B\preccurlyeq A\leftrightarrow \neg A\prec B\right)$$
5	4	ancoms	$$⊢\left(A\in V\wedge B\in \mathrm{Fin}\right)\to \left(B\preccurlyeq A\leftrightarrow \neg A\prec B\right)$$
6	3 5	imbitrrid	$$⊢\left(A\in V\wedge B\in \mathrm{Fin}\right)\to \left(\neg A\preccurlyeq B\to B\preccurlyeq A\right)$$
7		ensym	$$⊢B\approx A\to A\approx B$$
8		endom	$$⊢A\approx B\to A\preccurlyeq B$$
9	7 8	syl	$$⊢B\approx A\to A\preccurlyeq B$$
10	9	con3i	$$⊢\neg A\preccurlyeq B\to \neg B\approx A$$
11	6 10	jca2	$$⊢\left(A\in V\wedge B\in \mathrm{Fin}\right)\to \left(\neg A\preccurlyeq B\to \left(B\preccurlyeq A\wedge \neg B\approx A\right)\right)$$
12		brsdom	$$⊢B\prec A\leftrightarrow \left(B\preccurlyeq A\wedge \neg B\approx A\right)$$
13	11 12	imbitrrdi	$$⊢\left(A\in V\wedge B\in \mathrm{Fin}\right)\to \left(\neg A\preccurlyeq B\to B\prec A\right)$$
14	13	con1d	$$⊢\left(A\in V\wedge B\in \mathrm{Fin}\right)\to \left(\neg B\prec A\to A\preccurlyeq B\right)$$
15	1 14	impbid2	$$⊢\left(A\in V\wedge B\in \mathrm{Fin}\right)\to \left(A\preccurlyeq B\leftrightarrow \neg B\prec A\right)$$