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 )