MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmpt Unicode version

Theorem fmpt 5761
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.
StepHypRef Expression
1 fmpt.1 . . . 4  |-  F  =  ( x  e.  A  |->  C )
21fnmpt 5449 . . 3  |-  ( A. x  e.  A  C  e.  B  ->  F  Fn  A )
31rnmpt 5004 . . . 4  |-  ran  F  =  { y  |  E. x  e.  A  y  =  C }
4 r19.29 2759 . . . . . . 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 2418 . . . . . . . . 9  |-  ( y  =  C  ->  (
y  e.  B  <->  C  e.  B ) )
65biimparc 473 . . . . . . . 8  |-  ( ( C  e.  B  /\  y  =  C )  ->  y  e.  B )
76rexlimivw 2739 . . . . . . 7  |-  ( E. x  e.  A  ( C  e.  B  /\  y  =  C )  ->  y  e.  B )
84, 7syl 15 . . . . . 6  |-  ( ( A. x  e.  A  C  e.  B  /\  E. x  e.  A  y  =  C )  -> 
y  e.  B )
98ex 423 . . . . 5  |-  ( A. x  e.  A  C  e.  B  ->  ( E. x  e.  A  y  =  C  ->  y  e.  B ) )
109abssdv 3323 . . . 4  |-  ( A. x  e.  A  C  e.  B  ->  { y  |  E. x  e.  A  y  =  C }  C_  B )
113, 10syl5eqss 3298 . . 3  |-  ( A. x  e.  A  C  e.  B  ->  ran  F  C_  B )
12 df-f 5338 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
132, 11, 12sylanbrc 645 . 2  |-  ( A. x  e.  A  C  e.  B  ->  F : A
--> B )
141mptpreima 5245 . . . 4  |-  ( `' F " B )  =  { x  e.  A  |  C  e.  B }
15 fimacnv 5737 . . . 4  |-  ( F : A --> B  -> 
( `' F " B )  =  A )
1614, 15syl5reqr 2405 . . 3  |-  ( F : A --> B  ->  A  =  { x  e.  A  |  C  e.  B } )
17 rabid2 2793 . . 3  |-  ( A  =  { x  e.  A  |  C  e.  B }  <->  A. x  e.  A  C  e.  B )
1816, 17sylib 188 . 2  |-  ( F : A --> B  ->  A. x  e.  A  C  e.  B )
1913, 18impbii 180 1  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1642    e. wcel 1710   {cab 2344   A.wral 2619   E.wrex 2620   {crab 2623    C_ wss 3228    e. cmpt 4156   `'ccnv 4767   ran crn 4769   "cima 4771    Fn wfn 5329   -->wf 5330
This theorem is referenced by:  f1ompt  5762  fmpti  5763  fmptd  5764  idref  5842  f1mpt  5869  f1stres  6225  f2ndres  6226  fmpt2x  6274  fmpt2co  6286  iunon  6439  iinon  6441  onoviun  6444  onnseq  6445  mptelixpg  6938  dom2lem  6986  iinfi  7258  cantnfrescl  7465  acni2  7760  acnlem  7762  dfac4  7836  dfacacn  7854  fin23lem28  8053  axdc2lem  8161  axcclem  8170  ac6num  8193  uzf  10322  rlim2  12060  rlimi  12077  rlimmptrcl  12171  lo1mptrcl  12185  o1mptrcl  12186  o1fsum  12362  ackbijnn  12377  pcmptcl  13030  vdwlem11  13129  ismon2  13730  isepi2  13737  yonedalem3b  14146  efgsf  15131  gsummhm2  15305  gsumcom2  15319  issrngd  15719  psrass1lem  16216  subrgasclcl  16333  ipcl  16637  iinopn  16748  tgiun  16817  ordtrest2  17034  iscnp2  17069  discmp  17225  2ndcdisj  17282  ptunimpt  17390  pttopon  17391  txcnp  17414  ptcnplem  17415  ptcnp  17416  upxp  17417  ptcn  17421  txdis1cn  17429  cnmpt11  17457  cnmpt1t  17459  cnmpt12  17461  cnmpt21  17465  cnmptkp  17474  cnmptk1  17475  cnmpt1k  17476  cnmptkk  17477  cnmptk1p  17479  cnmptk2  17480  qtopeu  17507  uzrest  17688  txflf  17797  cnmpt1plusg  17866  clsnsg  17888  tgpconcomp  17891  tsmsf1o  17923  cnmpt1vsca  17972  prdsmet  18030  cnmpt1ds  18444  fsumcn  18471  cncfmpt1f  18514  cncfmpt2ss  18516  iccpnfcnv  18540  lebnumlem1  18557  copco  18614  pcoass  18620  cnmpt1ip  18772  bcth3  18851  voliun  19009  mbfmptcl  19090  i1f1lem  19142  i1fposd  19160  iblcnlem  19241  itgss3  19267  limcvallem  19319  ellimc2  19325  cnmptlimc  19338  dvmptcl  19406  dvmptco  19419  dvle  19452  dvfsumle  19466  dvfsumge  19467  dvfsumabs  19468  dvmptrecl  19469  dvfsumlem2  19472  itgparts  19492  itgsubstlem  19493  itgsubst  19494  evl1sca  19511  ulmss  19874  ulmdvlem2  19878  itgulm2  19886  sincn  19921  coscn  19922  logtayl  20112  rlimcxp  20373  harmonicbnd  20403  harmonicbnd2  20404  sqff1o  20526  lgseisenlem3  20696  xppreima2  23260  fmptdF  23269  rnmptss  23286  xrge0mulc1cn  23483  ustuqtop0  23544  esumcst  23721  mbfmco2  23879  0rrv  23958  lgamgulmlem6  24067  subfacf  24110  tailf  25648  sdclem2  25776  fdc  25779  heiborlem5  25862  elrfirn2  26094  mptfcl  26121  mzpexpmpt  26146  mzpsubst  26149  rabdiophlem1  26205  rabdiophlem2  26206  pw2f1ocnv  26453  frlmgsum  26555  uvcresum  26565  refsumcn  27024  fmptdf  27041  clim1fr1  27050  stoweidlem35  27107  stoweidlem42  27114  stoweidlem48  27120  wallispilem5  27141  wallispi  27142  stirlinglem5  27150  stirlinglem13  27158  stirlinglem14  27159  stirlinglem15  27160  stirlingr  27162  fargshiftf  27742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-mpt 4158  df-id 4388  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-fv 5342
  Copyright terms: Public domain W3C validator