Theorem 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 <-> ( F Fn A /\ A. x e. A ( F ''' x ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		ffn	|- ( F : A --> B -> F Fn A )
2		fafvelrn	|- ( ( F : A --> B /\ x e. A ) -> ( F ''' x ) e. B )
3	2	ralrimiva	|- ( F : A --> B -> A. x e. A ( F ''' x ) e. B )
4	1 3	jca	|- ( F : A --> B -> ( F Fn A /\ A. x e. A ( F ''' x ) e. B ) )
5		simpl	|- ( ( F Fn A /\ A. x e. A ( F ''' x ) e. B ) -> F Fn A )
6		afvelrnb0	|- ( F Fn A -> ( y e. ran F -> E. x e. A ( F ''' x ) = y ) )
7		nfra1	|- F/ x A. x e. A ( F ''' x ) e. B
8		nfv	|- F/ x y e. B
9		rsp	|- ( A. x e. A ( F ''' x ) e. B -> ( x e. A -> ( F ''' x ) e. B ) )
10		eleq1	|- ( ( F ''' x ) = y -> ( ( F ''' x ) e. B <-> y e. B ) )
11	10	biimpcd	|- ( ( F ''' x ) e. B -> ( ( F ''' x ) = y -> y e. B ) )
12	9 11	syl6	|- ( A. x e. A ( F ''' x ) e. B -> ( x e. A -> ( ( F ''' x ) = y -> y e. B ) ) )
13	7 8 12	rexlimd	|- ( A. x e. A ( F ''' x ) e. B -> ( E. x e. A ( F ''' x ) = y -> y e. B ) )
14	6 13	sylan9	|- ( ( F Fn A /\ A. x e. A ( F ''' x ) e. B ) -> ( y e. ran F -> y e. B ) )
15	14	ssrdv	|- ( ( F Fn A /\ A. x e. A ( F ''' x ) e. B ) -> ran F C_ B )
16		df-f	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
17	5 15 16	sylanbrc	|- ( ( F Fn A /\ A. x e. A ( F ''' x ) e. B ) -> F : A --> B )
18	4 17	impbii	|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ''' x ) e. B ) )