focdmex

Description: The codomain of an onto function is a set if its domain is a set. (Contributed by AV, 4-May-2021)

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

Step	Hyp	Ref	Expression
1		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
2	1	anim2i	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to (A \in V \land F : A ⟶ B)$
3	2	ancomd	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to (F : A ⟶ B \land A \in V)$
4		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
5		rnexg	$⊢ F \in V \to ran F \in V$
6	3 4 5	3syl	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to ran F \in V$
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	8	adantl	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to (ran F \in V \leftrightarrow B \in V)$
10	6 9	mpbid	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to B \in V$

Metamath Proof Explorer