This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )