Theorem fmpt2d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014)

	Ref	Expression
Hypotheses	fmpt2d.2	|- ( ( ph /\ x e. A ) -> B e. V )
	fmpt2d.1	|- ( ph -> F = ( x e. A |-> B ) )
	fmpt2d.3	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. C )
Assertion	fmpt2d	|- ( ph -> F : A --> C )

Proof

Step	Hyp	Ref	Expression
1		fmpt2d.2	|- ( ( ph /\ x e. A ) -> B e. V )
2		fmpt2d.1	|- ( ph -> F = ( x e. A |-> B ) )
3		fmpt2d.3	|- ( ( ph /\ y e. A ) -> ( F ` y ) e. C )
4	1	ralrimiva	|- ( ph -> A. x e. A B e. V )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	5	fnmpt	|- ( A. x e. A B e. V -> ( x e. A |-> B ) Fn A )
7	4 6	syl	|- ( ph -> ( x e. A |-> B ) Fn A )
8	2	fneq1d	|- ( ph -> ( F Fn A <-> ( x e. A |-> B ) Fn A ) )
9	7 8	mpbird	|- ( ph -> F Fn A )
10	3	ralrimiva	|- ( ph -> A. y e. A ( F ` y ) e. C )
11		ffnfv	|- ( F : A --> C <-> ( F Fn A /\ A. y e. A ( F ` y ) e. C ) )
12	9 10 11	sylanbrc	|- ( ph -> F : A --> C )