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 )