Metamath Proof Explorer

Theorem fidomtri

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

		Ref	Expression
	Assertion	fidomtri	$⊢ (A \in Fin \land B \in V) \to (A ≼ B \leftrightarrow \neg B ≺ A)$

Proof

Step	Hyp	Ref	Expression
1		domnsym	$⊢ A ≼ B \to \neg B ≺ A$
2		finnum	$⊢ A \in Fin \to A \in dom card$
3	2	adantr	$⊢ (A \in Fin \land B \in V) \to A \in dom card$
4		finnum	$⊢ B \in Fin \to B \in dom card$
5		domtri2	$⊢ (A \in dom card \land B \in dom card) \to (A ≼ B \leftrightarrow \neg B ≺ A)$
6	3 4 5	syl2an	$⊢ ((A \in Fin \land B \in V) \land B \in Fin) \to (A ≼ B \leftrightarrow \neg B ≺ A)$
7	6	biimprd	$⊢ ((A \in Fin \land B \in V) \land B \in Fin) \to (\neg B ≺ A \to A ≼ B)$
8		isinffi	$⊢ (\neg B \in Fin \land A \in Fin) \to \exists a a : A \underset{1-1}{⟶} B$
9	8	ancoms	$⊢ (A \in Fin \land \neg B \in Fin) \to \exists a a : A \underset{1-1}{⟶} B$
10	9	adantlr	$⊢ ((A \in Fin \land B \in V) \land \neg B \in Fin) \to \exists a a : A \underset{1-1}{⟶} B$
11		brdomg	$⊢ B \in V \to (A ≼ B \leftrightarrow \exists a a : A \underset{1-1}{⟶} B)$
12	11	ad2antlr	$⊢ ((A \in Fin \land B \in V) \land \neg B \in Fin) \to (A ≼ B \leftrightarrow \exists a a : A \underset{1-1}{⟶} B)$
13	10 12	mpbird	$⊢ ((A \in Fin \land B \in V) \land \neg B \in Fin) \to A ≼ B$
14	13	a1d	$⊢ ((A \in Fin \land B \in V) \land \neg B \in Fin) \to (\neg B ≺ A \to A ≼ B)$
15	7 14	pm2.61dan	$⊢ (A \in Fin \land B \in V) \to (\neg B ≺ A \to A ≼ B)$
16	1 15	impbid2	$⊢ (A \in Fin \land B \in V) \to (A ≼ B \leftrightarrow \neg B ≺ A)$