Theorem fmpt 5849

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 5530	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5075	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2806	. . . . . . 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 2464	. . . . . . . . 9 |- ( y = C -> ( y e. B <-> C e. B ) )
6	5	biimparc 474	. . . . . . . 8 |- ( ( C e. B /\ y = C ) -> y e. B )
7	6	rexlimivw 2786	. . . . . . 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 424	. . . . 5 |- ( A. x e. A C e. B -> ( E. x e. A y = C -> y e. B ) )
10	9	abssdv 3377	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3352	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5417	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
13	2, 11, 12	sylanbrc 646	. 2 |- ( A. x e. A C e. B -> F : A --> B )
14	1	mptpreima 5322	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 5821	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2451	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 2845	. . 3 |- ( A = { x e. A | C e. B } <-> A. x e. A C e. B )
18	16, 17	sylib 189	. 2 |- ( F : A --> B -> A. x e. A C e. B )
19	13, 18	impbii 181	1 |- ( A. x e. A C e. B <-> F : A --> B )

Syntax hints:   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   {cab 2390   A.wral 2666   E.wrex 2667   {crab 2670   C_ wss 3280   e. cmpt 4226   `'ccnv 4836   ran crn 4838   "cima 4840   Fn wfn 5408   -->wf 5409

This theorem is referenced by:  f1ompt  5850  fmpti  5851  fmptd  5852  rnmptss  5856  idref  5938  f1mpt  5966  f1stres  6327  f2ndres  6328  fmpt2x  6376  fmpt2co  6389  iunon  6559  iinon  6561  onoviun  6564  onnseq  6565  mptelixpg  7058  dom2lem  7106  iinfi  7380  cantnfrescl  7588  acni2  7883  acnlem  7885  dfac4  7959  dfacacn  7977  fin23lem28  8176  axdc2lem  8284  axcclem  8293  ac6num  8315  uzf  10447  rlim2  12245  rlimi  12262  rlimmptrcl  12356  lo1mptrcl  12370  o1mptrcl  12371  o1fsum  12547  ackbijnn  12562  pcmptcl  13215  vdwlem11  13314  ismon2  13915  isepi2  13922  yonedalem3b  14331  efgsf  15316  gsummhm2  15490  gsumcom2  15504  issrngd  15904  psrass1lem  16397  subrgasclcl  16514  ipcl  16819  iinopn  16930  tgiun  16999  ordtrest2  17222  iscnp2  17257  discmp  17415  2ndcdisj  17472  ptunimpt  17580  pttopon  17581  txcnp  17605  ptcnplem  17606  ptcnp  17607  upxp  17608  ptcn  17612  txdis1cn  17620  cnmpt11  17648  cnmpt1t  17650  cnmpt12  17652  cnmpt21  17656  cnmptkp  17665  cnmptk1  17666  cnmpt1k  17667  cnmptkk  17668  cnmptk1p  17670  cnmptk2  17671  qtopeu  17701  uzrest  17882  txflf  17991  cnmpt1plusg  18070  clsnsg  18092  tgpconcomp  18095  tsmsf1o  18127  cnmpt1vsca  18176  prdsmet  18353  cnmpt1ds  18826  fsumcn  18853  cncfmpt1f  18896  cncfmpt2ss  18898  iccpnfcnv  18922  lebnumlem1  18939  copco  18996  pcoass  19002  cnmpt1ip  19154  bcth3  19237  voliun  19401  mbfmptcl  19482  i1f1lem  19534  i1fposd  19552  iblcnlem  19633  itgss3  19659  limcvallem  19711  ellimc2  19717  cnmptlimc  19730  dvmptcl  19798  dvmptco  19811  dvle  19844  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvmptrecl  19861  dvfsumlem2  19864  itgparts  19884  itgsubstlem  19885  itgsubst  19886  evl1sca  19903  ulmss  20266  ulmdvlem2  20270  itgulm2  20278  sincn  20313  coscn  20314  logtayl  20504  rlimcxp  20765  harmonicbnd  20795  harmonicbnd2  20796  sqff1o  20918  lgseisenlem3  21088  fargshiftf  21576  fmptdF  24022  0rrv  24662  lgamgulmlem6  24771  subfacf  24814  tailf  26294  sdclem2  26336  fdc  26339  heiborlem5  26414  elrfirn2  26640  mptfcl  26667  mzpexpmpt  26692  mzpsubst  26695  rabdiophlem1  26751  rabdiophlem2  26752  pw2f1ocnv  26998  frlmgsum  27100  uvcresum  27110  refsumcn  27568  fmptdf  27585

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421