focdmex

Description: If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004)

		Ref	Expression
	Assertion	focdmex	$⊢ A \in C \to (F : A \underset{onto}{⟶} B \to B \in V)$

Step	Hyp	Ref	Expression
1		fofun	$⊢ F : A \underset{onto}{⟶} B \to Fun F$
2		funrnex	$⊢ dom F \in C \to (Fun F \to ran F \in V)$
3	1 2	syl5com	$⊢ F : A \underset{onto}{⟶} B \to (dom F \in C \to ran F \in V)$
4		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
5	4	fdmd	$⊢ F : A \underset{onto}{⟶} B \to dom F = A$
6	5	eleq1d	$⊢ F : A \underset{onto}{⟶} B \to (dom F \in C \leftrightarrow A \in C)$
7		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
8	7	eleq1d	$⊢ F : A \underset{onto}{⟶} B \to (ran F \in V \leftrightarrow B \in V)$
9	3 6 8	3imtr3d	$⊢ F : A \underset{onto}{⟶} B \to (A \in C \to B \in V)$
10	9	com12	$⊢ A \in C \to (F : A \underset{onto}{⟶} B \to B \in V)$

Metamath Proof Explorer