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

Metamath Proof Explorer

Theorem fmpt

Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis fmpt.1 
|- F = ( x e. A |-> C )
Assertion fmpt 
|- ( A. x e. A C e. B <-> F : A --> B )

Proof

Step Hyp Ref Expression
1 fmpt.1 
 |-  F = ( x e. A |-> C )
2 1 fnmpt 
 |-  ( A. x e. A C e. B -> F Fn A )
3 1 rnmpt 
 |-  ran F = { y | E. x e. A y = C }
4 r19.29 
 |-  ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> E. x e. A ( C e. B /\ y = C ) )
5 eleq1 
 |-  ( y = C -> ( y e. B <-> C e. B ) )
6 5 biimparc 
 |-  ( ( C e. B /\ y = C ) -> y e. B )
7 6 rexlimivw 
 |-  ( E. x e. A ( C e. B /\ y = C ) -> y e. B )
8 4 7 syl 
 |-  ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> y e. B )
9 8 ex 
 |-  ( A. x e. A C e. B -> ( E. x e. A y = C -> y e. B ) )
10 9 abssdv 
 |-  ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11 3 10 eqsstrid 
 |-  ( A. x e. A C e. B -> ran F C_ B )
12 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
13 2 11 12 sylanbrc 
 |-  ( A. x e. A C e. B -> F : A --> B )
14 fimacnv 
 |-  ( F : A --> B -> ( `' F " B ) = A )
15 1 mptpreima 
 |-  ( `' F " B ) = { x e. A | C e. B }
16 14 15 eqtr3di 
 |-  ( F : A --> B -> A = { x e. A | C e. B } )
17 rabid2 
 |-  ( A = { x e. A | C e. B } <-> A. x e. A C e. B )
18 16 17 sylib 
 |-  ( F : A --> B -> A. x e. A C e. B )
19 13 18 impbii 
 |-  ( A. x e. A C e. B <-> F : A --> B )