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

Theorem fss 5591
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 3347 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 29 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 549 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5450 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5450 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 262 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 420 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    C_ wss 3312   ran crn 4871    Fn wfn 5441   -->wf 5442
This theorem is referenced by:  fconst6g  5624  f1ss  5636  ffoss  5699  fsn2  5900  ofco  6316  tposf2  6495  issmo2  6603  smoiso  6616  mapsn  7047  mapss  7048  ssdomg  7145  ac6sfi  7343  infpwfien  7935  alephfplem4  7980  infmap2  8090  cofsmo  8141  fin23lem17  8210  fin23lem32  8216  hsmexlem1  8298  axdc3lem4  8325  ac6s  8356  pwfseqlem4a  8528  gruen  8679  intgru  8681  ingru  8682  1fv  11112  fseq1p1m1  11114  seqf1olem2  11355  hashf1lem1  11696  sswrd  11729  s1cl  11747  limsupgre  12267  abscn2  12384  recn2  12386  imcn2  12387  climabs  12389  climre  12391  climim  12392  rlimabs  12394  rlimre  12396  rlimim  12397  caucvgrlem  12458  caurcvgr  12459  caucvgrlem2  12460  caurcvg  12462  fsumre  12579  fsumim  12580  supcvg  12627  vdwlem8  13348  0ram  13380  ramub1  13388  ramcl  13389  isacs2  13870  funcres2b  14086  acsinfd  14598  acsdomd  14599  resmhm2  14752  gsumress  14769  gsumval1  14771  gsumwsubmcl  14776  gsumws1  14777  prdsgrpd  14919  prdsinvgd  14920  pj1ghm  15327  prdscmnd  15468  prdsabld  15469  gsumval3eu  15505  gsumval3  15506  gsumsubmcl  15516  gsumzadd  15519  gsumzoppg  15531  dprdsn  15586  pgpfaclem1  15631  prdsrngd  15710  prdscrngd  15711  abvf  15903  prdslmodd  16037  psrridm  16460  coe1fval3  16598  zntoslem  16829  frgpcyg  16846  pjdm2  16930  cnrest2  17342  cnprest2  17346  1stcelcls  17516  1stccnp  17517  1stckgen  17578  prdstps  17653  pthaus  17662  txcmplem2  17666  xkoptsub  17678  pt1hmeo  17830  ptcmpfi  17837  ptcmplem1  18075  ptcmpg  18080  prdstmdd  18145  prdstgpd  18146  tsmssubm  18164  ismet2  18355  prdsxmetlem  18390  imasdsf1olem  18395  prdsms  18553  isngp2  18636  metdscn  18878  cncfss  18921  ipcn  19192  lmmbr  19203  causs  19243  equivcau  19245  lmcau  19257  ovolfioo  19356  ovolficc  19357  ovolfsf  19360  elovolm  19363  ovollb  19367  ovolunlem1a  19384  ovolunlem1  19385  ovolicc2lem1  19405  ovolicc2lem2  19406  ovolicc2lem3  19407  ovolicc2lem4  19408  ovolicc2  19410  uniiccdif  19462  uniioovol  19463  uniiccvol  19464  uniioombllem2  19467  uniioombllem3a  19468  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  uniioombl  19473  dyadmbl  19484  vitalilem3  19494  vitalilem4  19495  vitalilem5  19496  ismbf  19514  mbfid  19520  0plef  19556  i1f1  19574  i1faddlem  19577  i1fmulclem  19586  i1fres  19589  i1fsub  19592  itg1sub  19593  mbfi1fseqlem4  19602  itg2le  19623  itg2mulclem  19630  itg2mulc  19631  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2i1fseqle  19638  itg2i1fseq3  19641  itg2addlem  19642  itg2gt0  19644  itg2cnlem1  19645  itg2cnlem2  19646  limccnp  19770  dvcmulf  19823  dvcobr  19824  dvfre  19829  dvnfre  19830  dvcnvlem  19852  dvcnv  19853  dvef  19856  dvferm1  19861  dvferm2  19863  rolle  19866  dvgt0lem1  19878  dvivthlem1  19884  dvne0  19887  lhop1lem  19889  lhop2  19891  lhop  19892  dvcnvrelem1  19893  dvcnvre  19895  dvcvx  19896  dvfsumrlim  19907  tdeglem3  19974  elply2  20107  elplyr  20112  plyeq0lem  20121  plyaddlem  20126  plymullem  20127  dgrlem  20140  coeidlem  20148  taylthlem2  20282  taylth  20283  ulmcn  20307  iblulm  20315  efcvx  20357  dvrelog  20520  relogcn  20521  dvlog2  20536  leibpi  20774  efrlim  20800  jensenlem2  20818  jensen  20819  amgmlem  20820  amgm  20821  wilthlem2  20844  wilthlem3  20845  basellem7  20861  basellem9  20863  lgsfcl  21080  lgsdchr  21124  dchrvmasumlem1  21181  dchrisum0lem3  21205  umgra1  21353  umisuhgra  21354  2trllemH  21544  2trllemG  21550  constr1trl  21580  constr3trllem1  21629  constr3trllem3  21631  eupa0  21688  eupap1  21690  0oo  22282  minvecolem3  22370  minvecolem4  22374  hhsscms  22771  occllem  22797  chscllem2  23132  chscllem4  23134  pjhf  23202  nlelchi  23556  hmopidmchi  23646  pjinvari  23686  lmlim  24325  rge0scvg  24327  lmdvg  24330  lmdvglim  24331  rrhre  24379  esumsn  24448  esumfsupre  24453  hashf2  24466  coinfliprv  24732  ptpcon  24912  fprb  25389  axlowdimlem4  25876  axlowdimlem7  25879  axlowdimlem10  25882  mblfinlem  26234  mbfresfi  26243  itg2addnclem  26246  itg2addnclem2  26247  itg2addnc  26249  itg2gt0cn  26250  ftc1anclem8  26277  fdc  26440  heiborlem6  26516  heibor  26521  ralxpmap  26733  ismrc  26746  mapfzcons  26763  mzpexpmpt  26793  mzpresrename  26798  diophrw  26808  rabren3dioph  26867  pwssplit1  27156  pwssplit4  27159  dsmmsubg  27177  dsmmlss  27178  islinds2  27251  lindsmm  27266  lsslindf  27268  lnrfg  27291  symgtrinv  27381  seff  27506  sblpnf  27507  climreeq  27706  stoweidlem39  27755  stoweidlem44  27760  stoweidlem59  27775  stirlinglem8  27797  lfl0f  29804  dochpolN  32225
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326  df-f 5450
  Copyright terms: Public domain W3C validator