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

Theorem fss 5562
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 3358 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 31 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 565 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5417 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5417 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 270 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 430 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3323   ran crn 4836    Fn wfn 5408   -->wf 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337  df-f 5417
This theorem is referenced by:  fconst6g  5594  f1ss  5606  fsn2  5878  ofco  6335  ffoss  6533  tposf2  6764  issmo2  6802  smoiso  6815  mapsn  7246  mapss  7247  ralxpmap  7254  ssdomg  7347  ac6sfi  7548  infpwfien  8224  alephfplem4  8269  infmap2  8379  cofsmo  8430  fin23lem17  8499  fin23lem32  8505  hsmexlem1  8587  axdc3lem4  8614  ac6s  8645  pwfseqlem4a  8820  gruen  8971  intgru  8973  ingru  8974  1fv  11524  fseq1p1m1  11526  seqf1olem2  11838  hashf1lem1  12200  sswrd  12234  snopiswrd  12235  repsdf2  12408  wrdlen2i  12538  limsupgre  12951  abscn2  13068  recn2  13070  imcn2  13071  climabs  13073  climre  13075  climim  13076  rlimabs  13078  rlimre  13080  rlimim  13081  caucvgrlem  13142  caurcvgr  13143  caucvgrlem2  13144  caurcvg  13146  fsumre  13263  fsumim  13264  supcvg  13310  vdwlem8  14041  0ram  14073  ramub1  14081  ramcl  14082  isacs2  14583  funcres2b  14799  acsinfd  15342  acsdomd  15343  resmhm2  15479  gsumress  15498  gsumval1  15500  gsumwsubmcl  15507  gsumws1  15508  prdsgrpd  15655  prdsinvgd  15656  symgtrinv  15969  pj1ghm  16191  prdscmnd  16334  prdsabld  16335  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumsubmcl  16395  gsumsubmclOLD  16396  gsumzadd  16400  gsumzaddOLD  16402  gsumzoppg  16430  gsumzoppgOLD  16431  dprdsn  16521  pgpfaclem1  16570  prdsrngd  16692  prdscrngd  16693  abvf  16886  prdslmodd  17027  pwssplit1  17117  psrridm  17453  psrridmOLD  17454  coe1fval3  17639  zntoslem  17964  frgpcyg  17981  regsumsupp  18027  pjdm2  18111  dsmmsubg  18143  dsmmlss  18144  islinds2  18217  lindsmm  18232  lsslindf  18234  cnrest2  18865  cnprest2  18869  1stcelcls  19040  1stccnp  19041  1stckgen  19102  prdstps  19177  pthaus  19186  txcmplem2  19190  xkoptsub  19202  pt1hmeo  19354  ptcmpfi  19361  ptcmplem1  19599  ptcmpg  19604  prdstmdd  19669  prdstgpd  19670  tsmssubm  19691  ismet2  19883  prdsxmetlem  19918  imasdsf1olem  19923  prdsms  20081  isngp2  20164  metdscn  20407  cncfss  20450  ipcn  20733  lmmbr  20744  causs  20784  equivcau  20786  lmcau  20798  ovolfioo  20926  ovolficc  20927  ovolfsf  20930  elovolm  20933  ovollb  20937  ovolunlem1a  20954  ovolunlem1  20955  ovolicc2lem1  20975  ovolicc2lem2  20976  ovolicc2lem3  20977  ovolicc2lem4  20978  ovolicc2  20980  uniiccdif  21033  uniioovol  21034  uniiccvol  21035  uniioombllem2  21038  uniioombllem3a  21039  uniioombllem3  21040  uniioombllem4  21041  uniioombllem5  21042  uniioombl  21044  dyadmbl  21055  vitalilem3  21065  vitalilem4  21066  vitalilem5  21067  ismbf  21083  mbfid  21089  0plef  21125  i1f1  21143  i1faddlem  21146  i1fmulclem  21155  i1fres  21158  i1fsub  21161  itg1sub  21162  mbfi1fseqlem4  21171  itg2le  21192  itg2mulclem  21199  itg2mulc  21200  itg2monolem1  21203  itg2monolem2  21204  itg2monolem3  21205  itg2mono  21206  itg2i1fseqle  21207  itg2i1fseq3  21210  itg2addlem  21211  itg2gt0  21213  itg2cnlem1  21214  itg2cnlem2  21215  limccnp  21341  dvcmulf  21394  dvcobr  21395  dvfre  21400  dvnfre  21401  dvcnvlem  21423  dvcnv  21424  dvef  21427  dvferm1  21432  dvferm2  21434  rolle  21437  dvgt0lem1  21449  dvivthlem1  21455  dvne0  21458  lhop1lem  21460  lhop2  21462  lhop  21463  dvcnvrelem1  21464  dvcnvre  21466  dvcvx  21467  dvfsumrlim  21478  tdeglem3  21503  elply2  21639  elplyr  21644  plyeq0lem  21653  plyaddlem  21658  plymullem  21659  dgrlem  21672  coeidlem  21680  taylthlem2  21814  taylth  21815  ulmcn  21839  iblulm  21847  efcvx  21889  dvrelog  22057  relogcn  22058  dvlog2  22073  leibpi  22312  efrlim  22338  jensenlem2  22356  jensen  22357  amgmlem  22358  amgm  22359  wilthlem2  22382  wilthlem3  22383  basellem7  22399  basellem9  22401  lgsfcl  22618  lgsdchr  22662  dchrvmasumlem1  22719  dchrisum0lem3  22743  axlowdimlem4  23142  axlowdimlem7  23145  axlowdimlem10  23148  umgra1  23211  umisuhgra  23212  2trllemH  23402  2trllemG  23408  constr1trl  23438  constr3trllem1  23487  constr3trllem3  23489  eupa0  23546  eupap1  23548  0oo  24140  minvecolem3  24228  minvecolem4  24232  hhsscms  24631  occllem  24657  chscllem2  24992  chscllem4  24994  pjhf  25062  nlelchi  25416  hmopidmchi  25506  pjinvari  25546  resf1o  25981  lmlim  26329  rge0scvg  26331  lmdvg  26335  lmdvglim  26336  rrhre  26399  esumsn  26467  esumfsupre  26472  hashf2  26485  eulerpartlems  26695  eulerpartlemgs2  26715  coinfliprv  26817  ptpcon  27074  fprb  27535  mblfinlem2  28382  mbfresfi  28391  itg2addnclem  28396  itg2addnclem2  28397  itg2addnc  28399  itg2gt0cn  28400  ftc1anclem8  28427  fdc  28594  heiborlem6  28668  heibor  28673  ismrc  28990  mapfzcons  29005  mzpexpmpt  29034  mzpresrename  29040  diophrw  29050  rabren3dioph  29107  pwssplit4  29395  lnrfg  29428  seff  29548  sblpnf  29549  climreeq  29739  stoweidlem39  29787  stoweidlem44  29792  stoweidlem59  29807  stirlinglem8  29829  mapsnop  30687  mapprop  30688  zlmodzxzel  30703  mat1dimelbas  30790  mat1dimmul  30795  snlindsntorlem  30893  zlmodzxzldeplem1  30931  lfl0f  32554  dochpolN  34975
  Copyright terms: Public domain W3C validator