Theorem fmpt 5852

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

Hypothesis

Ref	Expression
fmpt.1	|- F = ( x e. A |-> C )

Assertion

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

Distinct variable groups:   x, A   x, B

Allowed substitution hints:   C( x)   F( x)

Proof of Theorem fmpt

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fmpt.1	. . . 4 |- F = ( x e. A |-> C )
2	1	fnmpt 5525	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5072	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2847	. . . . . . 7 |- ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> E. x e. A ( C e. B /\ y = C ) )
5		eleq1 2493	. . . . . . . . 9 |- ( y = C -> ( y e. B <-> C e. B ) )
6	5	biimparc 484	. . . . . . . 8 |- ( ( C e. B /\ y = C ) -> y e. B )
7	6	rexlimivw 2827	. . . . . . 7 |- ( E. x e. A ( C e. B /\ y = C ) -> y e. B )
8	4, 7	syl 16	. . . . . 6 |- ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> y e. B )
9	8	ex 434	. . . . 5 |- ( A. x e. A C e. B -> ( E. x e. A y = C -> y e. B ) )
10	9	abssdv 3414	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3388	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5410	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
13	2, 11, 12	sylanbrc 657	. 2 |- ( A. x e. A C e. B -> F : A --> B )
14	1	mptpreima 5319	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 5823	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2480	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 2888	. . 3 |- ( A = { x e. A | C e. B } <-> A. x e. A C e. B )
18	16, 17	sylib 196	. 2 |- ( F : A --> B -> A. x e. A C e. B )
19	13, 18	impbii 188	1 |- ( A. x e. A C e. B <-> F : A --> B )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   {cab 2419   A.wral 2705   E.wrex 2706   {crab 2709   C_ wss 3316   e. cmpt 4338   `'ccnv 4826   ran crn 4828   "cima 4830   Fn wfn 5401   -->wf 5402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414

This theorem is referenced by:  f1ompt  5853  fmpti  5854  fmptd  5855  rnmptss  5859  f1oresrab  5862  idref  5945  f1mpt  5961  f1stres  6587  f2ndres  6588  fmpt2x  6629  fmpt2co  6645  iunon  6785  iinon  6787  onoviun  6790  onnseq  6791  mptelixpg  7288  dom2lem  7337  iinfi  7655  cantnfrescl  7872  acni2  8204  acnlem  8206  dfac4  8280  dfacacn  8298  fin23lem28  8497  axdc2lem  8605  axcclem  8614  ac6num  8636  uzf  10851  repsf  12394  rlim2  12957  rlimi  12974  rlimmptrcl  13068  lo1mptrcl  13082  o1mptrcl  13083  o1fsum  13258  ackbijnn  13273  pcmptcl  13935  vdwlem11  14034  ismon2  14655  isepi2  14662  yonedalem3b  15071  pmtrdifwrdellem1  15966  efgsf  16205  gsummhm2  16410  gsummhm2OLD  16411  gsummptcl  16431  gsummptfif1o  16432  gsummptfzcl  16433  gsumcom2  16440  issrngd  16869  psrass1lem  17380  subrgasclcl  17512  ipcl  17903  frlmgsumOLD  18036  frlmgsum  18037  uvcresum  18059  mavmulcl  18199  m2detleiblem3  18276  m2detleiblem4  18277  smadiadetlem3lem1  18313  iinopn  18356  tgiun  18425  ordtrest2  18649  iscnp2  18684  discmp  18842  2ndcdisj  18901  ptunimpt  19009  pttopon  19010  txcnp  19034  ptcnplem  19035  ptcnp  19036  upxp  19037  ptcn  19041  txdis1cn  19049  cnmpt11  19077  cnmpt1t  19079  cnmpt12  19081  cnmpt21  19085  cnmptkp  19094  cnmptk1  19095  cnmpt1k  19096  cnmptkk  19097  cnmptk1p  19099  cnmptk2  19100  qtopeu  19130  uzrest  19311  txflf  19420  cnmpt1plusg  19499  clsnsg  19521  tgpconcomp  19524  tsmsf1o  19560  cnmpt1vsca  19609  prdsmet  19786  cnmpt1ds  20260  fsumcn  20287  cncfmpt1f  20330  cncfmpt2ss  20332  iccpnfcnv  20357  lebnumlem1  20374  copco  20431  pcoass  20437  cnmpt1ip  20600  bcth3  20683  voliun  20876  mbfmptcl  20956  i1f1lem  21008  i1fposd  21026  iblcnlem  21107  itgss3  21133  limcvallem  21187  ellimc2  21193  cnmptlimc  21206  dvmptcl  21274  dvmptco  21287  dvle  21320  dvfsumle  21334  dvfsumge  21335  dvfsumabs  21336  dvmptrecl  21337  dvfsumlem2  21340  itgparts  21360  itgsubstlem  21361  itgsubst  21362  evl1sca  21380  ulmss  21746  ulmdvlem2  21750  itgulm2  21758  sincn  21793  coscn  21794  logtayl  21989  rlimcxp  22251  harmonicbnd  22281  harmonicbnd2  22282  sqff1o  22404  lgseisenlem3  22574  fargshiftf  23344  fmptdF  25795  ordtrest2NEW  26206  ddemeas  26505  eulerpartgbij  26602  0rrv  26681  signsvvf  26827  lgamgulmlem6  26867  subfacf  26910  tailf  28437  sdclem2  28479  fdc  28482  heiborlem5  28555  elrfirn2  28874  mptfcl  28898  mzpexpmpt  28923  mzpsubst  28927  rabdiophlem1  28981  rabdiophlem2  28982  pw2f1ocnv  29228  refsumcn  29594  fmptdf  29611  wwlktovf  30094