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) (Proof shortened by BTernaryTau, 25-Sep-2024)

		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		f1dom3g	$⊢ (F \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to A ≼ B$
6	4 5	syld3an1	$⊢ (A \in V \land B \in W \land F : A \underset{1-1}{⟶} B) \to A ≼ B$

Metamath Proof Explorer

Theorem f1dom2g

Proof