Metamath Proof Explorer

Theorem f1dom2gOLD

Description: Obsolete version of f1dom2g as of 25-Sep-2024. (Contributed by Mario Carneiro, 24-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	f1dom2gOLD	$⊢ (A \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to A ≼ B$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2		fex2	$⊢ (F : A ⟶ B \land A \in V \land B \in W) \to F \in V$
3	1 2	syl3an1	$⊢ (F : A \underset{1-1}{⟶} B \land A \in V \land B \in W) \to F \in V$
4	3	3coml	$⊢ (A \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to F \in V$
5		simp3	$⊢ (A \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to F : A \underset{1-1}{⟶} B$
6		f1eq1	$⊢ f = F \to (f : A \underset{1-1}{⟶} B \leftrightarrow F : A \underset{1-1}{⟶} B)$
7	4 5 6	spcedv	$⊢ (A \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to \exists f f : A \underset{1-1}{⟶} B$
8		brdomg	$⊢ B \in W \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
9	8	3ad2ant2	$⊢ (A \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
10	7 9	mpbird	$⊢ (A \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to A ≼ B$