Theorem fmpt 6058

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 5722	. . 3 |- ( A. x e. A C e. B -> F Fn A )
3	1	rnmpt 5099	. . . 4 |- ran F = { y | E. x e. A y = C }
4		r19.29 2960	. . . . . . 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 2495	. . . . . . . . 9 |- ( y = C -> ( y e. B <-> C e. B ) )
6	5	biimparc 489	. . . . . . . 8 |- ( ( C e. B /\ y = C ) -> y e. B )
7	6	rexlimivw 2911	. . . . . . 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 435	. . . . 5 |- ( A. x e. A C e. B -> ( E. x e. A y = C -> y e. B ) )
10	9	abssdv 3535	. . . 4 |- ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )
11	3, 10	syl5eqss 3508	. . 3 |- ( A. x e. A C e. B -> ran F C_ B )
12		df-f 5605	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
13	2, 11, 12	sylanbrc 668	. 2 |- ( A. x e. A C e. B -> F : A --> B )
14	1	mptpreima 5347	. . . 4 |- ( `' F " B ) = { x e. A | C e. B }
15		fimacnv 6027	. . . 4 |- ( F : A --> B -> ( `' F " B ) = A )
16	14, 15	syl5reqr 2478	. . 3 |- ( F : A --> B -> A = { x e. A | C e. B } )
17		rabid2 3003	. . 3 |- ( A = { x e. A | C e. B } <-> A. x e. A C e. B )
18	16, 17	sylib 199	. 2 |- ( F : A --> B -> A. x e. A C e. B )
19	13, 18	impbii 190	1 |- ( A. x e. A C e. B <-> F : A --> B )

Syntax hints:   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1872   {cab 2407   A.wral 2771   E.wrex 2772   {crab 2775   C_ wss 3436   |-> cmpt 4482   `'ccnv 4852   ran crn 4854   "cima 4856   Fn wfn 5596   -->wf 5597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609

This theorem is referenced by:  f1ompt  6059  fmpti  6060  fmptd  6061  fmptdf  6063  rnmptss  6067  f1oresrab  6070  idref  6161  f1mpt  6177  f1stres  6829  f2ndres  6830  fmpt2x  6873  fmpt2co  6890  onoviun  7073  onnseq  7074  mptelixpg  7570  dom2lem  7619  iinfi  7940  cantnfrescl  8189  acni2  8484  acnlem  8486  dfac4  8560  dfacacn  8578  fin23lem28  8777  axdc2lem  8885  axcclem  8894  ac6num  8916  uzf  11169  repsf  12878  rlim2  13559  rlimi  13576  rlimmptrcl  13670  lo1mptrcl  13684  o1mptrcl  13685  o1fsum  13872  ackbijnn  13885  pcmptcl  14835  vdwlem11  14940  ismon2  15638  isepi2  15645  yonedalem3b  16163  efgsf  17378  gsummhm2  17571  gsummptcl  17598  gsummptfif1o  17599  gsummptfzcl  17600  gsumcom2  17606  gsummptnn0fz  17614  issrngd  18088  psrass1lem  18600  subrgasclcl  18721  evl1sca  18921  ipcl  19198  frlmgsum  19328  uvcresum  19349  mavmulcl  19570  m2detleiblem3  19652  m2detleiblem4  19653  iinopn  19930  ordtrest2  20218  iscnp2  20253  discmp  20411  2ndcdisj  20469  ptunimpt  20608  pttopon  20609  txcnp  20633  ptcnplem  20634  ptcnp  20635  upxp  20636  ptcn  20640  txdis1cn  20648  cnmpt11  20676  cnmpt1t  20678  cnmpt12  20680  cnmpt21  20684  cnmptkp  20693  cnmptk1  20694  cnmpt1k  20695  cnmptkk  20696  cnmptk1p  20698  cnmptk2  20699  qtopeu  20729  uzrest  20910  txflf  21019  cnmpt1plusg  21100  clsnsg  21122  tgpconcomp  21125  tsmsf1o  21157  cnmpt1vsca  21206  prdsmet  21383  cnmpt1ds  21858  fsumcn  21900  cncfmpt1f  21943  cncfmpt2ss  21945  iccpnfcnv  21970  lebnumlem1  21987  lebnumlem1OLD  21990  copco  22047  pcoass  22053  cnmpt1ip  22216  bcth3  22297  voliun  22505  mbfmptcl  22591  i1f1lem  22645  i1fposd  22663  iblcnlem  22744  itgss3  22770  limcvallem  22824  ellimc2  22830  cnmptlimc  22843  dvmptcl  22911  dvmptco  22924  dvle  22957  dvfsumle  22971  dvfsumge  22972  dvfsumabs  22973  dvmptrecl  22974  dvfsumlem2  22977  itgparts  22997  itgsubstlem  22998  itgsubst  22999  ulmss  23350  ulmdvlem2  23354  itgulm2  23362  sincn  23397  coscn  23398  logtayl  23603  rlimcxp  23897  harmonicbnd  23927  harmonicbnd2  23928  lgamgulmlem6  23957  sqff1o  24107  lgseisenlem3  24277  fargshiftf  25362  fmptdF  28257  ordtrest2NEW  28737  ddemeas  29067  eulerpartgbij  29213  0rrv  29292  subfacf  29906  tailf  31036  fdc  32038  heiborlem5  32111  elrfirn2  35507  mptfcl  35531  mzpexpmpt  35556  mzpsubst  35559  rabdiophlem1  35613  rabdiophlem2  35614  pw2f1ocnv  35862  refsumcn  37324  mptex2  37393  fompt  37428  dvsinax  37723  itgsubsticclem  37792