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 5693	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5234	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2976	. . . . . . 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 2513	. . . . . . . . 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 2930	. . . . . . 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 3556	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3530	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5578	. . 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 5486	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 6000	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2497	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 3019	. . 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 1381   e. wcel 1802   {cab 2426   A.wral 2791   E.wrex 2792   {crab 2795   C_ wss 3458   |-> cmpt 4491   `'ccnv 4984   ran crn 4986   "cima 4988   Fn wfn 5569   -->wf 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-fv 5582

This theorem is referenced by:  f1ompt  6034  fmpti  6035  fmptd  6036  fmptdf  6037  rnmptss  6041  f1oresrab  6044  idref  6134  f1mpt  6150  f1stres  6803  f2ndres  6804  fmpt2x  6847  fmpt2co  6864  onoviun  7012  onnseq  7013  mptelixpg  7504  dom2lem  7553  iinfi  7875  cantnfrescl  8093  acni2  8425  acnlem  8427  dfac4  8501  dfacacn  8519  fin23lem28  8718  axdc2lem  8826  axcclem  8835  ac6num  8857  uzf  11088  repsf  12719  rlim2  13293  rlimi  13310  rlimmptrcl  13404  lo1mptrcl  13418  o1mptrcl  13419  o1fsum  13601  ackbijnn  13614  pcmptcl  14282  vdwlem11  14381  ismon2  15001  isepi2  15008  yonedalem3b  15417  efgsf  16616  gsummhm2  16830  gsummhm2OLD  16831  gsummptcl  16863  gsummptfif1o  16864  gsummptfzcl  16865  gsumcom2  16872  gsummptnn0fz  16883  issrngd  17378  psrass1lem  17897  subrgasclcl  18032  evl1sca  18238  ipcl  18535  frlmgsumOLD  18668  frlmgsum  18669  uvcresum  18691  mavmulcl  18916  m2detleiblem3  18998  m2detleiblem4  18999  iinopn  19278  ordtrest2  19571  iscnp2  19606  discmp  19764  2ndcdisj  19823  ptunimpt  19962  pttopon  19963  txcnp  19987  ptcnplem  19988  ptcnp  19989  upxp  19990  ptcn  19994  txdis1cn  20002  cnmpt11  20030  cnmpt1t  20032  cnmpt12  20034  cnmpt21  20038  cnmptkp  20047  cnmptk1  20048  cnmpt1k  20049  cnmptkk  20050  cnmptk1p  20052  cnmptk2  20053  qtopeu  20083  uzrest  20264  txflf  20373  cnmpt1plusg  20452  clsnsg  20474  tgpconcomp  20477  tsmsf1o  20513  cnmpt1vsca  20562  prdsmet  20739  cnmpt1ds  21213  fsumcn  21240  cncfmpt1f  21283  cncfmpt2ss  21285  iccpnfcnv  21310  lebnumlem1  21327  copco  21384  pcoass  21390  cnmpt1ip  21553  bcth3  21636  voliun  21830  mbfmptcl  21910  i1f1lem  21962  i1fposd  21980  iblcnlem  22061  itgss3  22087  limcvallem  22141  ellimc2  22147  cnmptlimc  22160  dvmptcl  22228  dvmptco  22241  dvle  22274  dvfsumle  22288  dvfsumge  22289  dvfsumabs  22290  dvmptrecl  22291  dvfsumlem2  22294  itgparts  22314  itgsubstlem  22315  itgsubst  22316  ulmss  22657  ulmdvlem2  22661  itgulm2  22669  sincn  22704  coscn  22705  logtayl  22906  rlimcxp  23168  harmonicbnd  23198  harmonicbnd2  23199  sqff1o  23321  lgseisenlem3  23491  fargshiftf  24501  fmptdF  27360  ordtrest2NEW  27771  ddemeas  28074  eulerpartgbij  28177  0rrv  28256  lgamgulmlem6  28442  subfacf  28485  tailf  30161  fdc  30206  heiborlem5  30279  elrfirn2  30596  mptfcl  30620  mzpexpmpt  30645  mzpsubst  30649  rabdiophlem1  30702  rabdiophlem2  30703  pw2f1ocnv  30947  refsumcn  31352  mptex2  31391  dvsinax  31608  itgsubsticclem  31660