Theorem fmpt 6053

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 5713	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5258	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2992	. . . . . . 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 2529	. . . . . . . . 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 2946	. . . . . . 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 3570	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3543	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5598	. . 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 5506	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 6020	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2513	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 3035	. . 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 1395   e. wcel 1819   {cab 2442   A.wral 2807   E.wrex 2808   {crab 2811   C_ wss 3471   |-> cmpt 4515   `'ccnv 5007   ran crn 5009   "cima 5011   Fn wfn 5589   -->wf 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-fv 5602

This theorem is referenced by:  f1ompt  6054  fmpti  6055  fmptd  6056  fmptdf  6057  rnmptss  6061  f1oresrab  6064  idref  6154  f1mpt  6170  f1stres  6821  f2ndres  6822  fmpt2x  6865  fmpt2co  6882  onoviun  7032  onnseq  7033  mptelixpg  7525  dom2lem  7574  iinfi  7895  cantnfrescl  8112  acni2  8444  acnlem  8446  dfac4  8520  dfacacn  8538  fin23lem28  8737  axdc2lem  8845  axcclem  8854  ac6num  8876  uzf  11109  repsf  12757  rlim2  13331  rlimi  13348  rlimmptrcl  13442  lo1mptrcl  13456  o1mptrcl  13457  o1fsum  13639  ackbijnn  13652  pcmptcl  14422  vdwlem11  14521  ismon2  15150  isepi2  15157  yonedalem3b  15675  efgsf  16874  gsummhm2  17088  gsummhm2OLD  17089  gsummptcl  17121  gsummptfif1o  17122  gsummptfzcl  17123  gsumcom2  17130  gsummptnn0fz  17141  issrngd  17637  psrass1lem  18156  subrgasclcl  18291  evl1sca  18497  ipcl  18795  frlmgsumOLD  18928  frlmgsum  18929  uvcresum  18951  mavmulcl  19176  m2detleiblem3  19258  m2detleiblem4  19259  iinopn  19538  ordtrest2  19832  iscnp2  19867  discmp  20025  2ndcdisj  20083  ptunimpt  20222  pttopon  20223  txcnp  20247  ptcnplem  20248  ptcnp  20249  upxp  20250  ptcn  20254  txdis1cn  20262  cnmpt11  20290  cnmpt1t  20292  cnmpt12  20294  cnmpt21  20298  cnmptkp  20307  cnmptk1  20308  cnmpt1k  20309  cnmptkk  20310  cnmptk1p  20312  cnmptk2  20313  qtopeu  20343  uzrest  20524  txflf  20633  cnmpt1plusg  20712  clsnsg  20734  tgpconcomp  20737  tsmsf1o  20773  cnmpt1vsca  20822  prdsmet  20999  cnmpt1ds  21473  fsumcn  21500  cncfmpt1f  21543  cncfmpt2ss  21545  iccpnfcnv  21570  lebnumlem1  21587  copco  21644  pcoass  21650  cnmpt1ip  21813  bcth3  21896  voliun  22090  mbfmptcl  22170  i1f1lem  22222  i1fposd  22240  iblcnlem  22321  itgss3  22347  limcvallem  22401  ellimc2  22407  cnmptlimc  22420  dvmptcl  22488  dvmptco  22501  dvle  22534  dvfsumle  22548  dvfsumge  22549  dvfsumabs  22550  dvmptrecl  22551  dvfsumlem2  22554  itgparts  22574  itgsubstlem  22575  itgsubst  22576  ulmss  22918  ulmdvlem2  22922  itgulm2  22930  sincn  22965  coscn  22966  logtayl  23167  rlimcxp  23429  harmonicbnd  23459  harmonicbnd2  23460  sqff1o  23582  lgseisenlem3  23752  fargshiftf  24763  fmptdF  27643  ordtrest2NEW  28066  ddemeas  28381  eulerpartgbij  28508  0rrv  28587  lgamgulmlem6  28773  subfacf  28816  tailf  30398  fdc  30443  heiborlem5  30516  elrfirn2  30833  mptfcl  30857  mzpexpmpt  30882  mzpsubst  30886  rabdiophlem1  30939  rabdiophlem2  30940  pw2f1ocnv  31183  refsumcn  31608  mptex2  31648  dvsinax  31911  itgsubsticclem  31977