Theorem fmpt 6033

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 5698	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5239	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2990	. . . . . . 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 2532	. . . . . . . . 9 |- ( y = C -> ( y e. B <-> C e. B ) )
6	5	biimparc 487	. . . . . . . 8 |- ( ( C e. B /\ y = C ) -> y e. B )
7	6	rexlimivw 2945	. . . . . . 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 3567	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3541	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5583	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
13	2, 11, 12	sylanbrc 664	. 2 |- ( A. x e. A C e. B -> F : A --> B )
14	1	mptpreima 5491	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 6004	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2516	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 3032	. . 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 1374   e. wcel 1762   {cab 2445   A.wral 2807   E.wrex 2808   {crab 2811   C_ wss 3469   |-> cmpt 4498   `'ccnv 4991   ran crn 4993   "cima 4995   Fn wfn 5574   -->wf 5575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587

This theorem is referenced by:  f1ompt  6034  fmpti  6035  fmptd  6036  fmptdf  6037  rnmptss  6041  f1oresrab  6044  idref  6132  f1mpt  6148  f1stres  6796  f2ndres  6797  fmpt2x  6840  fmpt2co  6856  iunon  6999  iinon  7001  onoviun  7004  onnseq  7005  mptelixpg  7496  dom2lem  7545  iinfi  7866  cantnfrescl  8084  acni2  8416  acnlem  8418  dfac4  8492  dfacacn  8510  fin23lem28  8709  axdc2lem  8817  axcclem  8826  ac6num  8848  uzf  11074  repsf  12695  wwlktovf  12844  rlim2  13268  rlimi  13285  rlimmptrcl  13379  lo1mptrcl  13393  o1mptrcl  13394  o1fsum  13576  ackbijnn  13592  pcmptcl  14258  vdwlem11  14357  ismon2  14979  isepi2  14986  yonedalem3b  15395  pmtrdifwrdellem1  16295  efgsf  16536  gsummhm2  16745  gsummhm2OLD  16746  gsummptcl  16778  gsummptfif1o  16779  gsummptfzcl  16780  gsumcom2  16787  gsummptnn0fz  16798  issrngd  17286  psrass1lem  17793  subrgasclcl  17928  evl1sca  18134  ipcl  18428  frlmgsumOLD  18561  frlmgsum  18562  uvcresum  18584  mavmulcl  18809  m2detleiblem3  18891  m2detleiblem4  18892  smadiadetlem3lem1  18928  iinopn  19171  tgiun  19240  ordtrest2  19464  iscnp2  19499  discmp  19657  2ndcdisj  19716  ptunimpt  19824  pttopon  19825  txcnp  19849  ptcnplem  19850  ptcnp  19851  upxp  19852  ptcn  19856  txdis1cn  19864  cnmpt11  19892  cnmpt1t  19894  cnmpt12  19896  cnmpt21  19900  cnmptkp  19909  cnmptk1  19910  cnmpt1k  19911  cnmptkk  19912  cnmptk1p  19914  cnmptk2  19915  qtopeu  19945  uzrest  20126  txflf  20235  cnmpt1plusg  20314  clsnsg  20336  tgpconcomp  20339  tsmsf1o  20375  cnmpt1vsca  20424  prdsmet  20601  cnmpt1ds  21075  fsumcn  21102  cncfmpt1f  21145  cncfmpt2ss  21147  iccpnfcnv  21172  lebnumlem1  21189  copco  21246  pcoass  21252  cnmpt1ip  21415  bcth3  21498  voliun  21692  mbfmptcl  21772  i1f1lem  21824  i1fposd  21842  iblcnlem  21923  itgss3  21949  limcvallem  22003  ellimc2  22009  cnmptlimc  22022  dvmptcl  22090  dvmptco  22103  dvle  22136  dvfsumle  22150  dvfsumge  22151  dvfsumabs  22152  dvmptrecl  22153  dvfsumlem2  22156  itgparts  22176  itgsubstlem  22177  itgsubst  22178  ulmss  22519  ulmdvlem2  22523  itgulm2  22531  sincn  22566  coscn  22567  logtayl  22762  rlimcxp  23024  harmonicbnd  23054  harmonicbnd2  23055  sqff1o  23177  lgseisenlem3  23347  fargshiftf  24298  fmptdF  27017  ordtrest2NEW  27391  ddemeas  27698  eulerpartgbij  27801  0rrv  27880  signsvvf  28026  lgamgulmlem6  28066  subfacf  28109  tailf  29647  sdclem2  29689  fdc  29692  heiborlem5  29765  elrfirn2  30083  mptfcl  30107  mzpexpmpt  30132  mzpsubst  30136  rabdiophlem1  30189  rabdiophlem2  30190  pw2f1ocnv  30436  refsumcn  30802  mptex2  30842  cncfmptssg  31027  icccncfext  31045  cncficcgt0  31046  cncfiooicclem1  31051  dvsinax  31060  dvcosax  31075  iblsplit  31103  itgsubsticclem  31112  itgsbtaddcnst  31119  fourierdlem43  31269  fourierdlem57  31283  fourierdlem93  31319  fourierdlem101  31327  fourierdlem111  31337  fouriersw  31351