Metamath Proof Explorer

Theorem f1dom2g

Description: The domain of a one-to-one function is dominated by its codomain. This variation of f1domg does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	f1dom2g	$⊢ (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$