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

Theorem fmpt 5681
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 5370 . . 3  |-  ( A. x  e.  A  C  e.  B  ->  F  Fn  A )
31rnmpt 4925 . . . 4  |-  ran  F  =  { y  |  E. x  e.  A  y  =  C }
4 r19.29 2683 . . . . . . 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 2343 . . . . . . . . 9  |-  ( y  =  C  ->  (
y  e.  B  <->  C  e.  B ) )
65biimparc 473 . . . . . . . 8  |-  ( ( C  e.  B  /\  y  =  C )  ->  y  e.  B )
76rexlimivw 2663 . . . . . . 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 3247 . . . 4  |-  ( A. x  e.  A  C  e.  B  ->  { y  |  E. x  e.  A  y  =  C }  C_  B )
113, 10syl5eqss 3222 . . 3  |-  ( A. x  e.  A  C  e.  B  ->  ran  F  C_  B )
12 df-f 5259 . . 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 5166 . . . 4  |-  ( `' F " B )  =  { x  e.  A  |  C  e.  B }
15 fimacnv 5657 . . . 4  |-  ( F : A --> B  -> 
( `' F " B )  =  A )
1614, 15syl5reqr 2330 . . 3  |-  ( F : A --> B  ->  A  =  { x  e.  A  |  C  e.  B } )
17 rabid2 2717 . . 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 1623    e. wcel 1684   {cab 2269   A.wral 2543   E.wrex 2544   {crab 2547    C_ wss 3152    e. cmpt 4077   `'ccnv 4688   ran crn 4690   "cima 4692    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  f1ompt  5682  fmpti  5683  fmptd  5684  idref  5759  f1mpt  5785  f1stres  6141  f2ndres  6142  fmpt2x  6190  fmpt2co  6202  iunon  6355  iinon  6357  onoviun  6360  onnseq  6361  mptelixpg  6853  dom2lem  6901  iinfi  7171  cantnfrescl  7378  acni2  7673  acnlem  7675  dfac4  7749  dfacacn  7767  fin23lem28  7966  axdc2lem  8074  axcclem  8083  ac6num  8106  uzf  10233  rlim2  11970  rlimi  11987  rlimmptrcl  12081  lo1mptrcl  12095  o1mptrcl  12096  o1fsum  12271  ackbijnn  12286  pcmptcl  12939  vdwlem11  13038  ismon2  13637  isepi2  13644  yonedalem3b  14053  efgsf  15038  gsummhm2  15212  gsumcom2  15226  issrngd  15626  psrass1lem  16123  subrgasclcl  16240  ipcl  16537  iinopn  16648  tgiun  16717  ordtrest2  16934  iscnp2  16969  discmp  17125  2ndcdisj  17182  ptunimpt  17290  pttopon  17291  txcnp  17314  ptcnplem  17315  ptcnp  17316  upxp  17317  ptcn  17321  txdis1cn  17329  cnmpt11  17357  cnmpt1t  17359  cnmpt12  17361  cnmpt21  17365  cnmptkp  17374  cnmptk1  17375  cnmpt1k  17376  cnmptkk  17377  cnmptk1p  17379  cnmptk2  17380  qtopeu  17407  uzrest  17592  txflf  17701  cnmpt1plusg  17770  clsnsg  17792  tgpconcomp  17795  tsmsf1o  17827  cnmpt1vsca  17876  prdsmet  17934  cnmpt1ds  18347  fsumcn  18374  cncfmpt1f  18417  cncfmpt2ss  18419  iccpnfcnv  18442  lebnumlem1  18459  copco  18516  pcoass  18522  cnmpt1ip  18674  bcth3  18753  voliun  18911  mbfmptcl  18992  i1f1lem  19044  i1fposd  19062  iblcnlem  19143  itgss3  19169  limcvallem  19221  ellimc2  19227  cnmptlimc  19240  dvmptcl  19308  dvmptco  19321  dvle  19354  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvmptrecl  19371  dvfsumlem2  19374  itgparts  19394  itgsubstlem  19395  itgsubst  19396  evl1sca  19413  ulmss  19774  ulmdvlem2  19778  itgulm2  19785  sincn  19820  coscn  19821  logtayl  20007  rlimcxp  20268  harmonicbnd  20297  harmonicbnd2  20298  sqff1o  20420  lgseisenlem3  20590  xppreima2  23212  fmptdF  23221  rnmptss  23238  xrge0mulc1cn  23323  esumcst  23436  mbfmco2  23570  0rrv  23654  subfacf  23706  fopab2g  25145  fsumprd  25329  clfsebs  25347  fprodadd  25352  fprodneg  25378  fprodsub  25379  svli2  25484  supnufb  25630  supbrr  25636  claddrvr  25648  sigadd  25649  issubrv  25672  subclrvd  25674  clsmulcv  25682  clsmulrv  25683  fnmulcv  25684  tailf  26324  sdclem2  26452  fdc  26455  heiborlem5  26539  elrfirn2  26771  mptfcl  26798  mzpexpmpt  26823  mzpsubst  26826  rabdiophlem1  26882  rabdiophlem2  26883  pw2f1ocnv  27130  frlmgsum  27232  uvcresum  27242  refsumcn  27701  fmptdf  27718  clim1fr1  27727  stoweidlem35  27784  stoweidlem42  27791  stoweidlem48  27797  wallispilem5  27818  wallispi  27819  stirlinglem5  27827  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  stirlingr  27839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263
  Copyright terms: Public domain W3C validator