Theorem fmpt 5963

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 5635	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5183	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2953	. . . . . . 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 2523	. . . . . . . . 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 2933	. . . . . . 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 3524	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3498	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5520	. . 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 5429	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 5934	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2507	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 2994	. . 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 1370   e. wcel 1758   {cab 2436   A.wral 2795   E.wrex 2796   {crab 2799   C_ wss 3426   |-> cmpt 4448   `'ccnv 4937   ran crn 4939   "cima 4941   Fn wfn 5511   -->wf 5512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-fv 5524

This theorem is referenced by:  f1ompt  5964  fmpti  5965  fmptd  5966  fmptdf  5967  rnmptss  5971  f1oresrab  5974  idref  6057  f1mpt  6073  f1stres  6698  f2ndres  6699  fmpt2x  6740  fmpt2co  6756  iunon  6899  iinon  6901  onoviun  6904  onnseq  6905  mptelixpg  7400  dom2lem  7449  iinfi  7768  cantnfrescl  7985  acni2  8317  acnlem  8319  dfac4  8393  dfacacn  8411  fin23lem28  8610  axdc2lem  8718  axcclem  8727  ac6num  8749  uzf  10965  repsf  12513  rlim2  13076  rlimi  13093  rlimmptrcl  13187  lo1mptrcl  13201  o1mptrcl  13202  o1fsum  13378  ackbijnn  13393  pcmptcl  14055  vdwlem11  14154  ismon2  14775  isepi2  14782  yonedalem3b  15191  pmtrdifwrdellem1  16089  efgsf  16330  gsummhm2  16539  gsummhm2OLD  16540  gsummptcl  16563  gsummptfif1o  16564  gsummptfzcl  16565  gsumcom2  16572  issrngd  17052  psrass1lem  17553  subrgasclcl  17688  evl1sca  17877  ipcl  18171  frlmgsumOLD  18304  frlmgsum  18305  uvcresum  18327  mavmulcl  18469  m2detleiblem3  18551  m2detleiblem4  18552  smadiadetlem3lem1  18588  iinopn  18631  tgiun  18700  ordtrest2  18924  iscnp2  18959  discmp  19117  2ndcdisj  19176  ptunimpt  19284  pttopon  19285  txcnp  19309  ptcnplem  19310  ptcnp  19311  upxp  19312  ptcn  19316  txdis1cn  19324  cnmpt11  19352  cnmpt1t  19354  cnmpt12  19356  cnmpt21  19360  cnmptkp  19369  cnmptk1  19370  cnmpt1k  19371  cnmptkk  19372  cnmptk1p  19374  cnmptk2  19375  qtopeu  19405  uzrest  19586  txflf  19695  cnmpt1plusg  19774  clsnsg  19796  tgpconcomp  19799  tsmsf1o  19835  cnmpt1vsca  19884  prdsmet  20061  cnmpt1ds  20535  fsumcn  20562  cncfmpt1f  20605  cncfmpt2ss  20607  iccpnfcnv  20632  lebnumlem1  20649  copco  20706  pcoass  20712  cnmpt1ip  20875  bcth3  20958  voliun  21151  mbfmptcl  21231  i1f1lem  21283  i1fposd  21301  iblcnlem  21382  itgss3  21408  limcvallem  21462  ellimc2  21468  cnmptlimc  21481  dvmptcl  21549  dvmptco  21562  dvle  21595  dvfsumle  21609  dvfsumge  21610  dvfsumabs  21611  dvmptrecl  21612  dvfsumlem2  21615  itgparts  21635  itgsubstlem  21636  itgsubst  21637  ulmss  21978  ulmdvlem2  21982  itgulm2  21990  sincn  22025  coscn  22026  logtayl  22221  rlimcxp  22483  harmonicbnd  22513  harmonicbnd2  22514  sqff1o  22636  lgseisenlem3  22806  fargshiftf  23657  fmptdF  26106  ordtrest2NEW  26487  ddemeas  26786  eulerpartgbij  26889  0rrv  26968  signsvvf  27114  lgamgulmlem6  27154  subfacf  27197  tailf  28734  sdclem2  28776  fdc  28779  heiborlem5  28852  elrfirn2  29170  mptfcl  29194  mzpexpmpt  29219  mzpsubst  29223  rabdiophlem1  29277  rabdiophlem2  29278  pw2f1ocnv  29524  refsumcn  29890  wwlktovf  30389  gsummptnn0fz  30947