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

Theorem fmpt 6052
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
Assertion
Ref Expression
fmpt
Distinct variable groups:   ,   ,

Proof of Theorem fmpt
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fmpt.1 . . . 4
21fnmpt 5712 . . 3
31rnmpt 5253 . . . 4
4 r19.29 2992 . . . . . . 7
5 eleq1 2529 . . . . . . . . 9
65biimparc 487 . . . . . . . 8
76rexlimivw 2946 . . . . . . 7
84, 7syl 16 . . . . . 6
98ex 434 . . . . 5
109abssdv 3573 . . . 4
113, 10syl5eqss 3547 . . 3
12 df-f 5597 . . 3
132, 11, 12sylanbrc 664 . 2
141mptpreima 5505 . . . 4
15 fimacnv 6019 . . . 4
1614, 15syl5reqr 2513 . . 3
17 rabid2 3035 . . 3
1816, 17sylib 196 . 2
1913, 18impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  {cab 2442  A.wral 2807  E.wrex 2808  {crab 2811  C_wss 3475  e.cmpt 4510  `'ccnv 5003  rancrn 5005  "cima 5007  Fnwfn 5588  -->wf 5589
This theorem is referenced by:  f1ompt  6053  fmpti  6054  fmptd  6055  fmptdf  6056  rnmptss  6060  f1oresrab  6063  idref  6153  f1mpt  6169  f1stres  6822  f2ndres  6823  fmpt2x  6866  fmpt2co  6883  onoviun  7033  onnseq  7034  mptelixpg  7526  dom2lem  7575  iinfi  7897  cantnfrescl  8116  acni2  8448  acnlem  8450  dfac4  8524  dfacacn  8542  fin23lem28  8741  axdc2lem  8849  axcclem  8858  ac6num  8880  uzf  11113  repsf  12745  rlim2  13319  rlimi  13336  rlimmptrcl  13430  lo1mptrcl  13444  o1mptrcl  13445  o1fsum  13627  ackbijnn  13640  pcmptcl  14410  vdwlem11  14509  ismon2  15129  isepi2  15136  yonedalem3b  15548  efgsf  16747  gsummhm2  16961  gsummhm2OLD  16962  gsummptcl  16994  gsummptfif1o  16995  gsummptfzcl  16996  gsumcom2  17003  gsummptnn0fz  17014  issrngd  17510  psrass1lem  18029  subrgasclcl  18164  evl1sca  18370  ipcl  18668  frlmgsumOLD  18801  frlmgsum  18802  uvcresum  18824  mavmulcl  19049  m2detleiblem3  19131  m2detleiblem4  19132  iinopn  19411  ordtrest2  19705  iscnp2  19740  discmp  19898  2ndcdisj  19957  ptunimpt  20096  pttopon  20097  txcnp  20121  ptcnplem  20122  ptcnp  20123  upxp  20124  ptcn  20128  txdis1cn  20136  cnmpt11  20164  cnmpt1t  20166  cnmpt12  20168  cnmpt21  20172  cnmptkp  20181  cnmptk1  20182  cnmpt1k  20183  cnmptkk  20184  cnmptk1p  20186  cnmptk2  20187  qtopeu  20217  uzrest  20398  txflf  20507  cnmpt1plusg  20586  clsnsg  20608  tgpconcomp  20611  tsmsf1o  20647  cnmpt1vsca  20696  prdsmet  20873  cnmpt1ds  21347  fsumcn  21374  cncfmpt1f  21417  cncfmpt2ss  21419  iccpnfcnv  21444  lebnumlem1  21461  copco  21518  pcoass  21524  cnmpt1ip  21687  bcth3  21770  voliun  21964  mbfmptcl  22044  i1f1lem  22096  i1fposd  22114  iblcnlem  22195  itgss3  22221  limcvallem  22275  ellimc2  22281  cnmptlimc  22294  dvmptcl  22362  dvmptco  22375  dvle  22408  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvmptrecl  22425  dvfsumlem2  22428  itgparts  22448  itgsubstlem  22449  itgsubst  22450  ulmss  22792  ulmdvlem2  22796  itgulm2  22804  sincn  22839  coscn  22840  logtayl  23041  rlimcxp  23303  harmonicbnd  23333  harmonicbnd2  23334  sqff1o  23456  lgseisenlem3  23626  fargshiftf  24636  fmptdF  27495  ordtrest2NEW  27905  ddemeas  28208  eulerpartgbij  28311  0rrv  28390  lgamgulmlem6  28576  subfacf  28619  tailf  30193  fdc  30238  heiborlem5  30311  elrfirn2  30628  mptfcl  30652  mzpexpmpt  30677  mzpsubst  30681  rabdiophlem1  30734  rabdiophlem2  30735  pw2f1ocnv  30979  refsumcn  31405  mptex2  31445  dvsinax  31708  itgsubsticclem  31774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601
  Copyright terms: Public domain W3C validator