ffnfv

Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003)

		Ref	Expression
	Assertion	ffnfv	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B)$

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ B \to F Fn A$
2		ffvelcdm	$⊢ (F : A ⟶ B \land x \in A) \to F (x) \in B$
3	2	ralrimiva	$⊢ F : A ⟶ B \to \forall x \in A F (x) \in B$
4	1 3	jca	$⊢ F : A ⟶ B \to (F Fn A \land \forall x \in A F (x) \in B)$
5		simpl	$⊢ (F Fn A \land \forall x \in A F (x) \in B) \to F Fn A$
6		fvelrnb	$⊢ F Fn A \to (y \in ran F \leftrightarrow \exists x \in A F (x) = y)$
7	6	biimpd	$⊢ F Fn A \to (y \in ran F \to \exists x \in A F (x) = y)$
8		nfra1	$⊢ Ⅎ x \forall x \in A F (x) \in B$
9		nfv	$⊢ Ⅎ x y \in B$
10		rsp	$⊢ \forall x \in A F (x) \in B \to (x \in A \to F (x) \in B)$
11		eleq1	$⊢ F (x) = y \to (F (x) \in B \leftrightarrow y \in B)$
12	11	biimpcd	$⊢ F (x) \in B \to (F (x) = y \to y \in B)$
13	10 12	syl6	$⊢ \forall x \in A F (x) \in B \to (x \in A \to (F (x) = y \to y \in B))$
14	8 9 13	rexlimd	$⊢ \forall x \in A F (x) \in B \to (\exists x \in A F (x) = y \to y \in B)$
15	7 14	sylan9	$⊢ (F Fn A \land \forall x \in A F (x) \in B) \to (y \in ran F \to y \in B)$
16	15	ssrdv	$⊢ (F Fn A \land \forall x \in A F (x) \in B) \to ran F \subseteq B$
17		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
18	5 16 17	sylanbrc	$⊢ (F Fn A \land \forall x \in A F (x) \in B) \to F : A ⟶ B$
19	4 18	impbii	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B)$

Metamath Proof Explorer