ffnafv

Description: A function maps to a class to which all values belong, analogous to ffnfv . (Contributed by Alexander van der Vekens, 25-May-2017)

		Ref	Expression
	Assertion	ffnafv	$⊢ 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		fafvelcdm	$⊢ (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		afvelrnb0	$⊢ F Fn A \to (y \in ran F \to \exists x \in A (F''' x) = y)$
7		nfra1	$⊢ Ⅎ x \forall x \in A (F''' x) \in B$
8		nfv	$⊢ Ⅎ x y \in B$
9		rsp	$⊢ \forall x \in A (F''' x) \in B \to (x \in A \to (F''' x) \in B)$
10		eleq1	$⊢ (F''' x) = y \to ((F''' x) \in B \leftrightarrow y \in B)$
11	10	biimpcd	$⊢ (F''' x) \in B \to ((F''' x) = y \to y \in B)$
12	9 11	syl6	$⊢ \forall x \in A (F''' x) \in B \to (x \in A \to ((F''' x) = y \to y \in B))$
13	7 8 12	rexlimd	$⊢ \forall x \in A (F''' x) \in B \to (\exists x \in A (F''' x) = y \to y \in B)$
14	6 13	sylan9	$⊢ (F Fn A \land \forall x \in A (F''' x) \in B) \to (y \in ran F \to y \in B)$
15	14	ssrdv	$⊢ (F Fn A \land \forall x \in A (F''' x) \in B) \to ran F \subseteq B$
16		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
17	5 15 16	sylanbrc	$⊢ (F Fn A \land \forall x \in A (F''' x) \in B) \to F : A ⟶ B$
18	4 17	impbii	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land \forall x \in A (F''' x) \in B)$

Metamath Proof Explorer