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

Theorem fmpt 5893
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 5574 . . 3  |-  ( A. x  e.  A  C  e.  B  ->  F  Fn  A )
31rnmpt 5119 . . . 4  |-  ran  F  =  { y  |  E. x  e.  A  y  =  C }
4 r19.29 2848 . . . . . . 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 2498 . . . . . . . . 9  |-  ( y  =  C  ->  (
y  e.  B  <->  C  e.  B ) )
65biimparc 475 . . . . . . . 8  |-  ( ( C  e.  B  /\  y  =  C )  ->  y  e.  B )
76rexlimivw 2828 . . . . . . 7  |-  ( E. x  e.  A  ( C  e.  B  /\  y  =  C )  ->  y  e.  B )
84, 7syl 16 . . . . . 6  |-  ( ( A. x  e.  A  C  e.  B  /\  E. x  e.  A  y  =  C )  -> 
y  e.  B )
98ex 425 . . . . 5  |-  ( A. x  e.  A  C  e.  B  ->  ( E. x  e.  A  y  =  C  ->  y  e.  B ) )
109abssdv 3419 . . . 4  |-  ( A. x  e.  A  C  e.  B  ->  { y  |  E. x  e.  A  y  =  C }  C_  B )
113, 10syl5eqss 3394 . . 3  |-  ( A. x  e.  A  C  e.  B  ->  ran  F  C_  B )
12 df-f 5461 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
132, 11, 12sylanbrc 647 . 2  |-  ( A. x  e.  A  C  e.  B  ->  F : A
--> B )
141mptpreima 5366 . . . 4  |-  ( `' F " B )  =  { x  e.  A  |  C  e.  B }
15 fimacnv 5865 . . . 4  |-  ( F : A --> B  -> 
( `' F " B )  =  A )
1614, 15syl5reqr 2485 . . 3  |-  ( F : A --> B  ->  A  =  { x  e.  A  |  C  e.  B } )
17 rabid2 2887 . . 3  |-  ( A  =  { x  e.  A  |  C  e.  B }  <->  A. x  e.  A  C  e.  B )
1816, 17sylib 190 . 2  |-  ( F : A --> B  ->  A. x  e.  A  C  e.  B )
1913, 18impbii 182 1  |-  ( A. x  e.  A  C  e.  B  <->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   {cab 2424   A.wral 2707   E.wrex 2708   {crab 2711    C_ wss 3322    e. cmpt 4269   `'ccnv 4880   ran crn 4882   "cima 4884    Fn wfn 5452   -->wf 5453
This theorem is referenced by:  f1ompt  5894  fmpti  5895  fmptd  5896  rnmptss  5900  idref  5982  f1mpt  6010  f1stres  6371  f2ndres  6372  fmpt2x  6420  fmpt2co  6433  iunon  6603  iinon  6605  onoviun  6608  onnseq  6609  mptelixpg  7102  dom2lem  7150  iinfi  7425  cantnfrescl  7635  acni2  7932  acnlem  7934  dfac4  8008  dfacacn  8026  fin23lem28  8225  axdc2lem  8333  axcclem  8342  ac6num  8364  uzf  10496  rlim2  12295  rlimi  12312  rlimmptrcl  12406  lo1mptrcl  12420  o1mptrcl  12421  o1fsum  12597  ackbijnn  12612  pcmptcl  13265  vdwlem11  13364  ismon2  13965  isepi2  13972  yonedalem3b  14381  efgsf  15366  gsummhm2  15540  gsumcom2  15554  issrngd  15954  psrass1lem  16447  subrgasclcl  16564  ipcl  16869  iinopn  16980  tgiun  17049  ordtrest2  17273  iscnp2  17308  discmp  17466  2ndcdisj  17524  ptunimpt  17632  pttopon  17633  txcnp  17657  ptcnplem  17658  ptcnp  17659  upxp  17660  ptcn  17664  txdis1cn  17672  cnmpt11  17700  cnmpt1t  17702  cnmpt12  17704  cnmpt21  17708  cnmptkp  17717  cnmptk1  17718  cnmpt1k  17719  cnmptkk  17720  cnmptk1p  17722  cnmptk2  17723  qtopeu  17753  uzrest  17934  txflf  18043  cnmpt1plusg  18122  clsnsg  18144  tgpconcomp  18147  tsmsf1o  18179  cnmpt1vsca  18228  prdsmet  18405  cnmpt1ds  18878  fsumcn  18905  cncfmpt1f  18948  cncfmpt2ss  18950  iccpnfcnv  18974  lebnumlem1  18991  copco  19048  pcoass  19054  cnmpt1ip  19206  bcth3  19289  voliun  19453  mbfmptcl  19532  i1f1lem  19584  i1fposd  19602  iblcnlem  19683  itgss3  19709  limcvallem  19763  ellimc2  19769  cnmptlimc  19782  dvmptcl  19850  dvmptco  19863  dvle  19896  dvfsumle  19910  dvfsumge  19911  dvfsumabs  19912  dvmptrecl  19913  dvfsumlem2  19916  itgparts  19936  itgsubstlem  19937  itgsubst  19938  evl1sca  19955  ulmss  20318  ulmdvlem2  20322  itgulm2  20330  sincn  20365  coscn  20366  logtayl  20556  rlimcxp  20817  harmonicbnd  20847  harmonicbnd2  20848  sqff1o  20970  lgseisenlem3  21140  fargshiftf  21628  fmptdF  24074  0rrv  24714  lgamgulmlem6  24823  subfacf  24866  tailf  26418  sdclem2  26460  fdc  26463  heiborlem5  26538  elrfirn2  26764  mptfcl  26791  mzpexpmpt  26816  mzpsubst  26819  rabdiophlem1  26875  rabdiophlem2  26876  pw2f1ocnv  27122  frlmgsum  27223  uvcresum  27233  refsumcn  27691  fmptdf  27708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-fv 5465
  Copyright terms: Public domain W3C validator