Theorem fmpt 5859

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 5532	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5080	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2852	. . . . . . 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 2498	. . . . . . . . 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 2832	. . . . . . 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 3421	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3395	. . 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 664	. 2 |- ( A. x e. A C e. B -> F : A --> B )
14	1	mptpreima 5326	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 5830	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2485	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 2893	. . 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 1369   e. wcel 1756   {cab 2424   A.wral 2710   E.wrex 2711   {crab 2714   C_ wss 3323   e. cmpt 4345   `'ccnv 4834   ran crn 4836   "cima 4838   Fn wfn 5408   -->wf 5409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421

This theorem is referenced by:  f1ompt  5860  fmpti  5861  fmptd  5862  fmptdf  5863  rnmptss  5867  f1oresrab  5870  idref  5953  f1mpt  5969  f1stres  6593  f2ndres  6594  fmpt2x  6635  fmpt2co  6651  iunon  6791  iinon  6793  onoviun  6796  onnseq  6797  mptelixpg  7292  dom2lem  7341  iinfi  7659  cantnfrescl  7876  acni2  8208  acnlem  8210  dfac4  8284  dfacacn  8302  fin23lem28  8501  axdc2lem  8609  axcclem  8618  ac6num  8640  uzf  10856  repsf  12403  rlim2  12966  rlimi  12983  rlimmptrcl  13077  lo1mptrcl  13091  o1mptrcl  13092  o1fsum  13268  ackbijnn  13283  pcmptcl  13945  vdwlem11  14044  ismon2  14665  isepi2  14672  yonedalem3b  15081  pmtrdifwrdellem1  15978  efgsf  16217  gsummhm2  16424  gsummhm2OLD  16425  gsummptcl  16448  gsummptfif1o  16449  gsummptfzcl  16450  gsumcom2  16457  issrngd  16926  psrass1lem  17427  subrgasclcl  17561  evl1sca  17748  ipcl  18042  frlmgsumOLD  18175  frlmgsum  18176  uvcresum  18198  mavmulcl  18338  m2detleiblem3  18415  m2detleiblem4  18416  smadiadetlem3lem1  18452  iinopn  18495  tgiun  18564  ordtrest2  18788  iscnp2  18823  discmp  18981  2ndcdisj  19040  ptunimpt  19148  pttopon  19149  txcnp  19173  ptcnplem  19174  ptcnp  19175  upxp  19176  ptcn  19180  txdis1cn  19188  cnmpt11  19216  cnmpt1t  19218  cnmpt12  19220  cnmpt21  19224  cnmptkp  19233  cnmptk1  19234  cnmpt1k  19235  cnmptkk  19236  cnmptk1p  19238  cnmptk2  19239  qtopeu  19269  uzrest  19450  txflf  19559  cnmpt1plusg  19638  clsnsg  19660  tgpconcomp  19663  tsmsf1o  19699  cnmpt1vsca  19748  prdsmet  19925  cnmpt1ds  20399  fsumcn  20426  cncfmpt1f  20469  cncfmpt2ss  20471  iccpnfcnv  20496  lebnumlem1  20513  copco  20570  pcoass  20576  cnmpt1ip  20739  bcth3  20822  voliun  21015  mbfmptcl  21095  i1f1lem  21147  i1fposd  21165  iblcnlem  21246  itgss3  21272  limcvallem  21326  ellimc2  21332  cnmptlimc  21345  dvmptcl  21413  dvmptco  21426  dvle  21459  dvfsumle  21473  dvfsumge  21474  dvfsumabs  21475  dvmptrecl  21476  dvfsumlem2  21479  itgparts  21499  itgsubstlem  21500  itgsubst  21501  ulmss  21842  ulmdvlem2  21846  itgulm2  21854  sincn  21889  coscn  21890  logtayl  22085  rlimcxp  22347  harmonicbnd  22377  harmonicbnd2  22378  sqff1o  22500  lgseisenlem3  22670  fargshiftf  23490  fmptdF  25940  ordtrest2NEW  26322  ddemeas  26621  eulerpartgbij  26724  0rrv  26803  signsvvf  26949  lgamgulmlem6  26989  subfacf  27032  tailf  28567  sdclem2  28609  fdc  28612  heiborlem5  28685  elrfirn2  29003  mptfcl  29027  mzpexpmpt  29052  mzpsubst  29056  rabdiophlem1  29110  rabdiophlem2  29111  pw2f1ocnv  29357  refsumcn  29723  wwlktovf  30222  gsummptnn0fz  30775