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

Theorem fmptd 6055
Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013.)
Hypotheses
Ref Expression
fmptd.1
fmptd.2
Assertion
Ref Expression
fmptd
Distinct variable groups:   ,   ,   ,

Proof of Theorem fmptd
StepHypRef Expression
1 fmptd.1 . . 3
21ralrimiva 2871 . 2
3 fmptd.2 . . 3
43fmpt 6052 . 2
52, 4sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  e.cmpt 4510  -->wf 5589
This theorem is referenced by:  fmptco  6064  fliftrel  6206  off  6554  caofinvl  6567  curry1f  6894  curry2f  6896  fnwelem  6915  fdiagfn  7482  resixpfo  7527  pw2f1olem  7641  mapxpen  7703  xpmapenlem  7704  unxpdomlem3  7746  fsuppmptdm  7860  fsuppmptif  7879  wdom2d  8027  cantnfp1lem1  8118  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnflem1d  8128  cantnflem1  8129  cantnf  8133  cantnfp1lem1OLD  8144  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  cantnflem1OLD  8152  cantnfOLD  8155  fseqenlem1  8426  fseqenlem2  8427  dfac8clem  8434  ac5num  8438  acni2  8448  infpwfien  8464  coftr  8674  fin23lem39  8751  isf34lem2  8774  fin1a2lem12  8812  axcc2lem  8837  axdc2lem  8849  axdc3lem4  8854  pwcfsdom  8979  canthp1lem2  9052  wuncval2  9146  gruf  9210  rpnnen1lem1  11237  monoord2  12138  seqf1o  12148  ccatcl  12593  swrdcl  12646  revcl  12735  revlen  12736  ello1mpt  13344  lo1o12  13356  lo1eq  13391  rlimeq  13392  climmpt2  13396  climrecl  13406  climge0  13407  o1compt  13410  rlimcn1b  13412  rlimdiv  13468  isercoll2  13491  caurcvg2  13500  caucvg  13501  sumrblem  13533  summolem2a  13537  fsumf1o  13545  sumss  13546  fsumss  13547  fsumcl2lem  13553  fsumadd  13561  isumclim3  13574  isummulc2  13577  fsummulc2  13599  fsumrelem  13621  climfsum  13634  isumshft  13651  divcnv  13665  supcvg  13667  prodfdiv  13705  prodrblem  13736  prodmolem2a  13741  fprodf1o  13753  prodss  13754  fprodss  13755  fprodser  13756  fprodcl2lem  13757  fprodmul  13765  fproddiv  13766  fprodn0  13783  iprodclim3  13793  fprodefsum  13830  rpnnen2lem2  13949  crt  14308  eulerthlem1  14311  iserodd  14359  prmreclem2  14435  prmreclem6  14439  1arithlem3  14443  4sqlem11  14473  vdwapf  14490  vdwlem2  14500  vdwlem4  14502  vdwlem6  14504  vdwlem10  14508  ramub1lem2  14545  ramcl  14547  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  mrcflem  15003  mreacs  15055  acsfn  15056  homaf  15357  prfcl  15472  curf1cl  15497  hofcllem  15527  hofcl  15528  yonedalem3a  15543  yonedalem4c  15546  yonedainv  15550  prdspjmhm  15998  pwsco1mhm  16001  pwsco2mhm  16002  gsumz  16005  gsumwspan  16014  vrmdfval  16024  vrmdf  16026  frmdup1  16032  grpinvf  16094  cycsubgcl  16227  cycsubgss  16228  conjghm  16297  conjnmz  16300  qusghm  16303  galactghm  16428  symgextf  16442  symgfixf  16461  pmtrf  16480  pmtrdifwrdellem1  16506  psgnunilem5  16519  odf1  16584  dfod2  16586  odf1o2  16593  pgpssslw  16634  sylow2blem1  16640  pj1f  16715  frgpmhm  16783  vrgpf  16786  mulgmhm  16836  mulgghm  16837  iscyggen2  16884  cyggenod  16887  iscyg3  16889  gsummptfsadd  16940  gsummptfsaddOLD  16941  gsumzsplit  16944  gsumzsplitOLD  16945  gsumsplit2  16948  gsumsplit2OLD  16949  gsummptfidmsplitres  16951  gsumconst  16954  gsummptshft  16956  gsummhm2  16961  gsummhm2OLD  16962  gsummptmhm  16963  gsummptfidminv  16972  gsummptfssub  16976  gsumzunsnd  16982  gsummptf1o  16990  gsummpt1n0  16992  gsum2dlem1  16997  gsum2dlem2  16998  gsum2d  16999  gsum2dOLD  17000  prdsgsum  17007  prdsgsumOLD  17008  dprdfeq0  17062  dprdfeq0OLD  17069  dprdlub  17073  dprdz  17077  dprd2dlem1  17090  dprd2da  17091  ablfac1b  17121  ablfac2  17140  srglmhm  17186  srgrmhm  17187  ringlghm  17250  ringrghm  17251  gsumdixpOLD  17257  gsumdixp  17258  abvtrivd  17489  issrngd  17510  lmodvsghm  17571  lspf  17620  pwssplit0  17704  asclf  17986  snifpsrbag  18015  psrass1lem  18029  psrbasOLD  18031  psrmulcllem  18040  psr1cl  18055  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  psrcom  18064  resspsrmul  18072  subrgpsr  18074  mvridlemOLD  18075  mvrf  18080  mplmon  18125  mplmonmul  18126  mplcoe1  18127  mplcoe3OLD  18129  mplcoe5lem  18130  mplcoe5  18131  mplcoe2OLD  18133  mplbas2  18134  mplbas2OLD  18135  psrbagsn  18160  evlslem4OLD  18173  evlslem4  18174  evlslem2  18180  evlslem6  18181  evlslem6OLD  18182  evlslem3  18183  evlslem1  18184  evlsval2  18189  psropprmul  18279  coe1mul2  18310  coe1tmmul2  18317  coe1tmmul  18318  ply1coe  18337  ply1coeOLD  18338  gsumsmonply1  18345  gsummoncoe1  18346  gsumfsum  18484  expmhm  18485  expghm  18529  expghmOLD  18530  mulgghm2  18531  mulgghm2OLD  18534  evpmodpmf1o  18632  isphld  18689  pjff  18743  frlmgsumOLD  18801  frlmgsum  18802  frlmsplit2  18803  frlmphl  18812  uvcff  18822  uvcresum  18824  frlmup1  18832  mamulid  18943  mamurid  18944  scmatf  19031  mdetf  19097  mdetunilem9  19122  mdetuni0  19123  mdetmul  19125  maduf  19143  smadiadetlem3lem1  19168  cpm2mf  19253  m2cpmfo  19257  pmatcollpw1  19277  pmatcollpw3lem  19284  pmatcollpw3fi1lem1  19287  pmatcollpw3fi1lem2  19288  pm2mpcl  19298  mply1topmatcl  19306  mp2pm2mplem2  19308  mp2pm2mp  19312  pm2mpmhmlem2  19320  chfacfisf  19355  chfacfisfcpmat  19356  cpmidpmatlem2  19372  cayhamlem4  19389  pptbas  19509  tgrest  19660  resttopon  19662  rest0  19670  restfpw  19680  ordtbaslem  19689  ordtuni  19691  ordtrest  19703  cnpfval  19735  pnrmopn  19844  cncmp  19892  discmp  19898  1stcfb  19946  2ndcomap  19959  dis2ndc  19961  lly1stc  19997  comppfsc  20033  kgencmp  20046  ptpjpre1  20072  ptpjcn  20112  ptcldmpt  20115  ptclsg  20116  dfac14  20119  xkoccn  20120  txcnp  20121  ptcnp  20123  txcnmpt  20125  uptx  20126  ptcn  20128  ptrescn  20140  txlm  20149  xkoptsub  20155  xkoco1cn  20158  xkoco2cn  20159  cnmpt11  20164  xkoinjcn  20188  kqffn  20226  pt1hmeo  20307  fbasrn  20385  trfilss  20390  trfg  20392  rnelfmlem  20453  txflf  20507  flfcnp2  20508  fclscmpi  20530  alexsublem  20544  ptcmplem3  20554  symgtgp  20600  subgntr  20605  opnsubg  20606  clsnsg  20608  tgpconcomp  20611  tsmsfbas  20626  eltsms  20631  haustsms  20634  tsmscls  20636  tsms0  20643  tsmsmhm  20648  tgptsmscls  20652  tsmssplit  20654  tsmsxplem1  20655  tsmsxplem2  20656  ustuqtop0  20743  prdsdsf  20870  prdsxmetlem  20871  imasdsf1olem  20876  prdsbl  20994  stdbdxmet  21018  met1stc  21024  nmf2  21113  nmof  21226  xrge0gsumle  21338  xrge0tsms  21339  metdsf  21352  metdsge  21353  mulc1cncf  21409  cncfmpt2ss  21419  cnmptre  21427  evth  21459  evth2  21460  lebnumlem1  21461  cphnmf  21642  tchcph  21680  cmetcaulem  21727  rrxmval  21832  minveclem1  21839  minveclem3b  21843  ovollb2lem  21899  ovolctb  21901  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovoliun  21916  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  iunmbl  21963  ioombl1lem1  21968  uniioombllem2  21992  uniioombllem3  21994  volsup2  22014  volcn  22015  vitalilem4  22020  vitalilem5  22021  mbfconst  22042  ismbfcn2  22046  mbfeqalem  22049  mbfss  22053  mbfmulc2re  22055  mbfmax  22056  mbfneg  22057  mbfpos  22058  mbfposr  22059  mbfposb  22060  mbfadd  22068  mbfmulc2  22070  mbfsup  22071  mbfinf  22072  mbflimsup  22073  mbflimlem  22074  mbflim  22075  i1f1lem  22096  i1f1  22097  i1fres  22112  itg1climres  22121  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1flimlem  22129  mbfi1flim  22130  mbfmullem2  22131  mbfmul  22133  itg2const2  22148  itg2seq  22149  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  itg2i1fseq  22162  itg2i1fseq2  22163  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  itg2cn  22170  iblss  22211  itgitg1  22215  itgle  22216  itgeqa  22220  itgss3  22221  ibladdlem  22226  itgaddlem1  22229  iblabslem  22234  iblabs  22235  iblabsr  22236  iblmulc2  22237  itgmulc2lem1  22238  bddmulibl  22245  itggt0  22248  itgcn  22249  ellimc2  22281  limcmpt  22287  limcres  22290  limccnp  22295  limccnp2  22296  limcco  22297  perfdvf  22307  dvreslem  22313  dvcnp2  22323  dvaddbr  22341  dvmulbr  22342  dvcjbr  22352  dvexp  22356  dvrec  22358  dvmptres3  22359  dvmptadd  22363  dvmptmul  22364  dvmptres2  22365  dvmptcmul  22367  dvmptcj  22371  dvmptntr  22374  dvmptco  22375  dvcnvlem  22377  dvef  22381  dvferm1  22386  dvferm2  22388  rolle  22391  dvlipcn  22395  dvle  22408  dvivthlem1  22409  dvivth  22411  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvfsumle  22422  dvfsumge  22423  dvmptrecl  22425  dvfsumrlimf  22426  dvfsumlem2  22428  dvfsumlem3  22429  ftc1lem2  22437  ftc1lem6  22442  itgsubstlem  22449  tdeglem1  22456  tdeglem4  22458  coe1mul3  22500  elply2  22593  plyf  22595  elplyd  22599  plypf1  22609  coeeq2  22639  coemullem  22647  coe1termlem  22655  dvply2g  22681  elqaalem2  22716  taylfvallem  22753  taylf  22756  tayl0  22757  taylpfval  22760  taylpf  22761  taylthlem1  22768  taylthlem2  22769  ulmshftlem  22784  ulmshft  22785  ulmcau  22790  ulmss  22792  ulmdvlem1  22795  ulmdvlem3  22797  mtest  22799  mtestbdd  22800  itgulm2  22804  psergf  22807  radcnvlem1  22808  dvradcnv  22816  pserulm  22817  psercn2  22818  pserdvlem2  22823  abelthlem4  22829  abelthlem9  22835  pige3  22910  efif1olem4  22932  logtayl  23041  logccv  23044  loglesqrt  23132  leibpi  23273  rlimcnp  23295  rlimcnp2  23296  xrlimcnp  23298  efrlim  23299  dfef2  23300  o1cxp  23304  cxp2lim  23306  amgmlem  23319  basellem2  23355  basellem4  23357  basellem7  23360  basellem9  23362  sqff1o  23456  fsumvma  23488  dchrelbasd  23514  lgsfcl2  23577  lgsqrlem2  23617  lgseisenlem1  23624  lgseisenlem3  23626  lgseisenlem4  23627  chpo1ub  23665  dchrmusum2  23679  dchrvmasumiflem1  23686  dchrisum0ff  23692  dchrisum0lem1b  23700  dchrisum0lem2a  23702  logsqvma2  23728  pnt2  23798  pnt  23799  abvcxp  23800  padicabv  23815  lmif  24151  axlowdimlem15  24259  nbgraf1olem2  24442  wlkiswwlk2lem5  24695  wlknwwlknfun  24710  wlkiswwlkfun  24717  wwlkextfun  24729  clwlkisclwwlklem2a  24785  clwwlkf  24794  clwlkfclwwlk  24844  vdgrf  24898  vdgrfif  24899  frgrancvvdeqlem5  25034  numclwlk1lem2f  25092  numclwlk2lem2f  25103  efghgrpOLD  25375  ipblnfi  25771  ubthlem1  25786  minvecolem1  25790  htthlem  25834  hlimadd  26110  chscllem1  26555  hoaddcl  26677  homulcl  26678  brafn  26866  kbop  26872  cnlnadjlem2  26987  strlem3a  27171  hstrlem3a  27179  off2  27481  xppreima2  27488  fmpt3d  27496  fpwrelmap  27556  regsumfsum  27772  gsumvsca1  27773  gsumvsca2  27774  xrge0tsmsd  27775  ordtrestNEW  27903  xrge0mulc1cn  27923  esumf1o  28061  esumadd  28064  esumcst  28071  esumpfinval  28081  esumpcvgval  28084  esumcvg  28092  measinb  28192  measdivcst  28196  mbfmco2  28236  sitgclg  28284  eulerpartlems  28299  dstfrvclim1  28416  gsumncl  28492  gsumnunsn  28493  lgamgulmlem2  28572  lgamgulmlem6  28576  lgamcvg2  28597  gamcvg  28598  regamcl  28603  relgamcl  28604  erdszelem9  28643  indispcon  28679  cvxpcon  28687  cvmsss2  28719  cvmliftlem6  28735  cvmliftlem8  28737  cvmlift3lem3  28766  mrsubcv  28870  mrsubff  28872  mrsubrn  28873  mrsubccat  28878  elmrsubrn  28880  msubrn  28889  msubff  28890  mvhf  28918  divcnvlin  29118  iprodefisum  29124  faclimlem2  29169  faclim  29171  faclim2  29173  finixpnum  30038  ptrest  30048  mblfinlem2  30052  volsupnfl  30059  mbfposadd  30062  itg2addnclem2  30067  itg2gt0cn  30070  ibladdnclem  30071  itgaddnclem1  30073  itgaddnc  30075  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  itgmulc2nclem1  30081  itgmulc2nclem2  30082  itgmulc2nc  30083  itgabsnc  30084  bddiblnc  30085  itggt0cn  30087  ftc1cnnc  30089  ftc1anclem1  30090  ftc1anclem2  30091  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirclem4  30110  upixp  30220  totbndbnd  30285  prdsbnd  30289  cntotbnd  30292  rrnequiv  30331  cmpfiiin  30629  mzpclall  30659  mzpindd  30678  fphpdo  30751  dnnumch3  30993  kelac1  31009  dfac21  31012  itgpowd  31182  expgrowth  31240  binomcxplemradcnv  31257  binomcxplemcvg  31259  binomcxplemnotnn0  31261  rnmptc  31449  mptelpm  31453  expcnfg  31586  clim1fr1  31607  mullimc  31622  ellimcabssub0  31623  mullimcf  31629  constlimc  31630  idlimc  31632  sumnnodd  31636  neglimc  31653  addlimc  31654  0ellimcdiv  31655  cncfmptssg  31672  cncfshift  31676  cncfcompt  31685  icccncfext  31690  cncfiooiccre  31698  cxpcncf2  31703  dvsinax  31708  fperdvper  31715  dvmptresicc  31716  dvcosax  31723  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmptdivc  31735  dvnxpaek  31739  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  itgsinexplem1  31752  iblsplit  31765  itgcoscmulx  31768  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  dirkerf  31879  dirkeritg  31884  dirkercncflem2  31886  fourierdlem4  31893  fourierdlem5  31894  fourierdlem9  31898  fourierdlem14  31903  fourierdlem16  31905  fourierdlem17  31906  fourierdlem18  31907  fourierdlem21  31910  fourierdlem22  31911  fourierdlem37  31926  fourierdlem50  31939  fourierdlem51  31940  fourierdlem53  31942  fourierdlem55  31944  fourierdlem57  31946  fourierdlem58  31947  fourierdlem59  31948  fourierdlem60  31949  fourierdlem61  31950  fourierdlem67  31956  fourierdlem68  31957  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem80  31969  fourierdlem81  31970  fourierdlem83  31972  fourierdlem84  31973  fourierdlem88  31977  fourierdlem92  31981  fourierdlem93  31982  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  sqwvfoura  32011  elaa2lem  32016  etransclem1  32018  etransclem8  32025  etransclem20  32037  etransclem33  32050  etransclem35  32052  etransclem39  32056  funcestrcsetclem3  32648  funcsetcestrclem3  32662  c0mgm  32715  c0mhm  32716  c0snmgmhm  32720  funcringcsetcOLD2lem3  32846  funcringcsetclem3OLD  32869  gsumlsscl  32976  ply1mulgsum  32990  lincfsuppcl  33014  linccl  33015  lincvalsc0  33022  lcoc0  33023  linc0scn0  33024  linc1  33026  lincsum  33030  lincscm  33031  lincscmcl  33033  lcoss  33037  lincext1  33055  el0ldep  33067  lincresunit1  33078  lincresunit3  33082  lmod1zr  33094  aacllem  33216  lsatlss  34721  lflnegcl  34800  lshpkrcl  34841  tendoplcl  36507  tendo0cl  36516  tendoicl  36522
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