f1domg

Description: The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004)

		Ref	Expression
	Assertion	f1domg	$⊢ B \in C \to (F : A \underset{1-1}{⟶} B \to A ≼ B)$

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2		f1dmex	$⊢ (F : A \underset{1-1}{⟶} B \land B \in C) \to A \in V$
3		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
4	1 2 3	syl2an2r	$⊢ (F : A \underset{1-1}{⟶} B \land B \in C) \to F \in V$
5	4	expcom	$⊢ B \in C \to (F : A \underset{1-1}{⟶} B \to F \in V)$
6		f1eq1	$⊢ f = F \to (f : A \underset{1-1}{⟶} B \leftrightarrow F : A \underset{1-1}{⟶} B)$
7	6	spcegv	$⊢ F \in V \to (F : A \underset{1-1}{⟶} B \to \exists f f : A \underset{1-1}{⟶} B)$
8	5 7	syli	$⊢ B \in C \to (F : A \underset{1-1}{⟶} B \to \exists f f : A \underset{1-1}{⟶} B)$
9		brdomg	$⊢ B \in C \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
10	8 9	sylibrd	$⊢ B \in C \to (F : A \underset{1-1}{⟶} B \to A ≼ B)$

Metamath Proof Explorer