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

Theorem fss 5413
Description: Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
Assertion
Ref Expression
fss  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )

Proof of Theorem fss
StepHypRef Expression
1 sstr2 3199 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 27 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 548 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5275 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5275 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 261 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 419 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3165   ran crn 4706    Fn wfn 5266   -->wf 5267
This theorem is referenced by:  fconst6g  5446  f1ss  5458  ffoss  5521  fsn2  5714  ofco  6113  tposf2  6274  issmo2  6382  smoiso  6395  mapsn  6825  mapss  6826  ssdomg  6923  ac6sfi  7117  infpwfien  7705  alephfplem4  7750  infmap2  7860  cofsmo  7911  fin23lem17  7980  fin23lem32  7986  hsmexlem1  8068  axdc3lem4  8095  ac6s  8127  pwfseqlem4a  8299  gruen  8450  intgru  8452  ingru  8453  fseq1p1m1  10873  seqf1olem2  11102  hashf1lem1  11409  sswrd  11439  s1cl  11457  limsupgre  11971  abscn2  12088  recn2  12090  imcn2  12091  climabs  12093  climre  12095  climim  12096  rlimabs  12098  rlimre  12100  rlimim  12101  caucvgrlem  12161  caurcvgr  12162  caucvgrlem2  12163  caurcvg  12165  fsumre  12282  fsumim  12283  supcvg  12330  vdwlem8  13051  0ram  13083  ramub1  13091  ramcl  13092  isacs2  13571  funcres2b  13787  acsinfd  14299  acsdomd  14300  resmhm2  14453  gsumress  14470  gsumval1  14472  gsumwsubmcl  14477  gsumws1  14478  prdsgrpd  14620  prdsinvgd  14621  pj1ghm  15028  prdscmnd  15169  prdsabld  15170  gsumval3eu  15206  gsumval3  15207  gsumsubmcl  15217  gsumzadd  15220  gsumzoppg  15232  dprdsn  15287  pgpfaclem1  15332  prdsrngd  15411  prdscrngd  15412  abvf  15604  prdslmodd  15742  psrridm  16165  coe1fval3  16305  zntoslem  16526  frgpcyg  16543  pjdm2  16627  cnrest2  17030  cnprest2  17034  1stcelcls  17203  1stccnp  17204  1stckgen  17265  prdstps  17339  pthaus  17348  txcmplem2  17352  xkoptsub  17364  pt1hmeo  17513  ptcmpfi  17520  ptcmplem1  17762  ptcmpg  17767  prdstmdd  17822  prdstgpd  17823  tsmssubm  17841  ismet2  17914  prdsxmetlem  17948  imasdsf1olem  17953  prdsms  18093  isngp2  18135  metdscn  18376  cncfss  18419  ipcn  18689  lmmbr  18700  causs  18740  equivcau  18742  lmcau  18754  ovolfioo  18843  ovolficc  18844  ovolfsf  18847  elovolm  18850  ovollb  18854  ovolunlem1a  18871  ovolunlem1  18872  ovolicc2lem1  18892  ovolicc2lem2  18893  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2  18897  uniiccdif  18949  uniioovol  18950  uniiccvol  18951  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombl  18960  dyadmbl  18971  vitalilem3  18981  vitalilem4  18982  vitalilem5  18983  ismbf  19001  mbfid  19007  0plef  19043  i1f1  19061  i1faddlem  19064  i1fmulclem  19073  i1fres  19076  i1fsub  19079  itg1sub  19080  mbfi1fseqlem4  19089  itg2le  19110  itg2mulclem  19117  itg2mulc  19118  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq3  19128  itg2addlem  19129  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  limccnp  19257  dvcmulf  19310  dvcobr  19311  dvfre  19316  dvnfre  19317  dvcnvlem  19339  dvcnv  19340  dvef  19343  dvferm1  19348  dvferm2  19350  rolle  19353  dvgt0lem1  19365  dvivthlem1  19371  dvne0  19374  lhop1lem  19376  lhop2  19378  lhop  19379  dvcnvrelem1  19380  dvcnvre  19382  dvcvx  19383  dvfsumrlim  19394  tdeglem3  19461  elply2  19594  elplyr  19599  plyeq0lem  19608  plyaddlem  19613  plymullem  19614  dgrlem  19627  coeidlem  19635  taylthlem2  19769  taylth  19770  ulmcn  19792  iblulm  19799  efcvx  19841  dvrelog  20000  relogcn  20001  dvlog2  20016  leibpi  20254  efrlim  20280  jensenlem2  20298  jensen  20299  amgmlem  20300  amgm  20301  wilthlem2  20323  wilthlem3  20324  basellem7  20340  basellem9  20342  lgsfcl  20559  lgsdchr  20603  dchrvmasumlem1  20660  dchrisum0lem3  20684  0oo  21383  minvecolem3  21471  minvecolem4  21475  hhsscms  21872  occllem  21898  chscllem2  22233  chscllem4  22235  pjhf  22303  nlelchi  22657  hmopidmchi  22747  pjinvari  22787  lmlim  23386  rge0scvg  23388  lmdvg  23391  lmdvglim  23392  esumsn  23452  hashf2  23467  coinfliprv  23698  ptpcon  23779  umgra1  23893  eupa0  23913  eupap1  23915  fprb  24200  axlowdimlem4  24645  axlowdimlem7  24648  axlowdimlem10  24651  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  cbicp  25269  domrancur1c  25305  istopxc  25651  claddrvr  25751  rnegvex2  25764  negveudr  25772  clsmulrv  25786  divclrvd  25798  idsubfun  25961  1iskle  26092  phckle  26130  psckle  26131  pgapspf  26155  pgapspf2  26156  fdc  26558  heiborlem6  26643  heibor  26648  ralxpmap  26864  ismrc  26879  mapfzcons  26896  mzpexpmpt  26926  mzpresrename  26931  diophrw  26941  rabren3dioph  27001  pwssplit1  27291  pwssplit4  27294  dsmmsubg  27312  dsmmlss  27313  islinds2  27386  lindsmm  27401  lsslindf  27403  lnrfg  27426  symgtrinv  27516  seff  27641  sblpnf  27642  climreeq  27842  stoweidlem39  27891  stoweidlem44  27896  stoweidlem59  27911  stirlinglem8  27933  constr3trllem1  28396  constr3trllem3  28398  lfl0f  29881  dochpolN  32302
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275
  Copyright terms: Public domain W3C validator