Theorem fmpt 6027

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 5686	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5058	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2893	. . . . . . 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 2518	. . . . . . . . 9 |- ( y = C -> ( y e. B <-> C e. B ) )
6	5	biimparc 494	. . . . . . . 8 |- ( ( C e. B /\ y = C ) -> y e. B )
7	6	rexlimivw 2850	. . . . . . 7 |- ( E. x e. A ( C e. B /\ y = C ) -> y e. B )
8	4, 7	syl 17	. . . . . 6 |- ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> y e. B )
9	8	ex 440	. . . . 5 |- ( A. x e. A C e. B -> ( E. x e. A y = C -> y e. B ) )
10	9	abssdv 3471	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3444	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5565	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
13	2, 11, 12	sylanbrc 675	. 2 |- ( A. x e. A C e. B -> F : A --> B )
14	1	mptpreima 5307	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 5996	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2501	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 2936	. . 3 |- ( A = { x e. A | C e. B } <-> A. x e. A C e. B )
18	16, 17	sylib 201	. 2 |- ( F : A --> B -> A. x e. A C e. B )
19	13, 18	impbii 192	1 |- ( A. x e. A C e. B <-> F : A --> B )

Syntax hints:   <-> wb 189   /\ wa 375   = wceq 1448   e. wcel 1891   {cab 2438   A.wral 2737   E.wrex 2738   {crab 2741   C_ wss 3372   |-> cmpt 4433   `'ccnv 4811   ran crn 4813   "cima 4815   Fn wfn 5556   -->wf 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-fv 5569

This theorem is referenced by:  f1ompt  6028  fmpti  6029  fmptd  6030  fmptdf  6032  rnmptss  6037  f1oresrab  6040  idref  6132  f1mpt  6148  f1stres  6803  f2ndres  6804  fmpt2x  6847  fmpt2co  6867  onoviun  7049  onnseq  7050  mptelixpg  7546  dom2lem  7596  iinfi  7918  cantnfrescl  8168  acni2  8464  acnlem  8466  dfac4  8540  dfacacn  8558  fin23lem28  8757  axdc2lem  8865  axcclem  8874  ac6num  8896  uzf  11152  repsf  12875  rlim2  13571  rlimi  13588  rlimmptrcl  13682  lo1mptrcl  13696  o1mptrcl  13697  o1fsum  13884  ackbijnn  13897  pcmptcl  14847  vdwlem11  14952  ismon2  15650  isepi2  15657  yonedalem3b  16175  efgsf  17390  gsummhm2  17583  gsummptcl  17610  gsummptfif1o  17611  gsummptfzcl  17612  gsumcom2  17618  gsummptnn0fz  17626  issrngd  18100  psrass1lem  18612  subrgasclcl  18733  evl1sca  18933  ipcl  19211  frlmgsum  19341  uvcresum  19362  mavmulcl  19583  m2detleiblem3  19665  m2detleiblem4  19666  iinopn  19943  ordtrest2  20231  iscnp2  20266  discmp  20424  2ndcdisj  20482  ptunimpt  20621  pttopon  20622  txcnp  20646  ptcnplem  20647  ptcnp  20648  upxp  20649  ptcn  20653  txdis1cn  20661  cnmpt11  20689  cnmpt1t  20691  cnmpt12  20693  cnmpt21  20697  cnmptkp  20706  cnmptk1  20707  cnmpt1k  20708  cnmptkk  20709  cnmptk1p  20711  cnmptk2  20712  qtopeu  20742  uzrest  20923  txflf  21032  cnmpt1plusg  21113  clsnsg  21135  tgpconcomp  21138  tsmsf1o  21170  cnmpt1vsca  21219  prdsmet  21396  cnmpt1ds  21871  fsumcn  21913  cncfmpt1f  21956  cncfmpt2ss  21958  iccpnfcnv  21983  lebnumlem1  22000  lebnumlem1OLD  22003  copco  22060  pcoass  22066  cnmpt1ip  22229  bcth3  22310  voliun  22519  mbfmptcl  22605  i1f1lem  22659  i1fposd  22677  iblcnlem  22758  itgss3  22784  limcvallem  22838  ellimc2  22844  cnmptlimc  22857  dvmptcl  22925  dvmptco  22938  dvle  22971  dvfsumle  22985  dvfsumge  22986  dvfsumabs  22987  dvmptrecl  22988  dvfsumlem2  22991  itgparts  23011  itgsubstlem  23012  itgsubst  23013  ulmss  23364  ulmdvlem2  23368  itgulm2  23376  sincn  23411  coscn  23412  logtayl  23617  rlimcxp  23911  harmonicbnd  23941  harmonicbnd2  23942  lgamgulmlem6  23971  sqff1o  24121  lgseisenlem3  24291  fargshiftf  25376  fmptdF  28264  ordtrest2NEW  28736  ddemeas  29065  eulerpartgbij  29211  0rrv  29290  subfacf  29904  tailf  31037  fdc  32076  heiborlem5  32149  elrfirn2  35540  mptfcl  35564  mzpexpmpt  35589  mzpsubst  35592  rabdiophlem1  35646  rabdiophlem2  35647  pw2f1ocnv  35894  refsumcn  37348  mptex2  37443  fompt  37477  dvsinax  37825  itgsubsticclem  37894