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	|- ( ( A e. V /\ B e. Fin ) -> ( A ~<_ B <-> -. B ~< A ) )

Proof

Step	Hyp	Ref	Expression
1		domnsym	|- ( A ~<_ B -> -. B ~< A )
2		sdomdom	|- ( A ~< B -> A ~<_ B )
3	2	con3i	|- ( -. A ~<_ B -> -. A ~< B )
4		fidomtri	|- ( ( B e. Fin /\ A e. V ) -> ( B ~<_ A <-> -. A ~< B ) )
5	4	ancoms	|- ( ( A e. V /\ B e. Fin ) -> ( B ~<_ A <-> -. A ~< B ) )
6	3 5	imbitrrid	|- ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> B ~<_ A ) )
7		ensym	|- ( B ~~ A -> A ~~ B )
8		endom	|- ( A ~~ B -> A ~<_ B )
9	7 8	syl	|- ( B ~~ A -> A ~<_ B )
10	9	con3i	|- ( -. A ~<_ B -> -. B ~~ A )
11	6 10	jca2	|- ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> ( B ~<_ A /\ -. B ~~ A ) ) )
12		brsdom	|- ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
13	11 12	imbitrrdi	|- ( ( A e. V /\ B e. Fin ) -> ( -. A ~<_ B -> B ~< A ) )
14	13	con1d	|- ( ( A e. V /\ B e. Fin ) -> ( -. B ~< A -> A ~<_ B ) )
15	1 14	impbid2	|- ( ( A e. V /\ B e. Fin ) -> ( A ~<_ B <-> -. B ~< A ) )