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

Theorem fss 5678
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 3474 . . . . 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 5533 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5533 . . 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 3439   ran crn 4952    Fn wfn 5524   -->wf 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3446  df-ss 3453  df-f 5533
This theorem is referenced by:  fconst6g  5710  f1ss  5722  fsn2  5995  ofco  6453  ffoss  6651  tposf2  6882  issmo2  6923  smoiso  6936  mapsn  7367  mapss  7368  ralxpmap  7375  ssdomg  7468  ac6sfi  7670  infpwfien  8346  alephfplem4  8391  infmap2  8501  cofsmo  8552  fin23lem17  8621  fin23lem32  8627  hsmexlem1  8709  axdc3lem4  8736  ac6s  8767  pwfseqlem4a  8942  gruen  9093  intgru  9095  ingru  9096  1fv  11652  fseq1p1m1  11654  seqf1olem2  11966  hashf1lem1  12329  sswrd  12363  snopiswrd  12364  repsdf2  12537  wrdlen2i  12667  limsupgre  13080  abscn2  13197  recn2  13199  imcn2  13200  climabs  13202  climre  13204  climim  13205  rlimabs  13207  rlimre  13209  rlimim  13210  caucvgrlem  13271  caurcvgr  13272  caucvgrlem2  13273  caurcvg  13275  fsumre  13392  fsumim  13393  supcvg  13439  vdwlem8  14170  0ram  14202  ramub1  14210  ramcl  14211  isacs2  14713  funcres2b  14929  acsinfd  15472  acsdomd  15473  resmhm2  15610  gsumress  15629  gsumval1  15631  gsumwsubmcl  15638  gsumws1  15639  prdsgrpd  15786  prdsinvgd  15787  symgtrinv  16100  pj1ghm  16324  prdscmnd  16467  prdsabld  16468  gsumval3eu  16505  gsumval3OLD  16506  gsumval3  16509  gsumsubmcl  16528  gsumsubmclOLD  16529  gsumzadd  16533  gsumzaddOLD  16535  gsumzoppg  16565  gsumzoppgOLD  16566  dprdsn  16658  pgpfaclem1  16707  prdsrngd  16830  prdscrngd  16831  abvf  17034  prdslmodd  17176  pwssplit1  17266  psrridm  17602  psrridmOLD  17603  coe1fval3  17791  zntoslem  18117  frgpcyg  18134  regsumsupp  18180  pjdm2  18264  dsmmsubg  18296  dsmmlss  18297  islinds2  18370  lindsmm  18385  lsslindf  18387  cnrest2  19025  cnprest2  19029  1stcelcls  19200  1stccnp  19201  1stckgen  19262  prdstps  19337  pthaus  19346  txcmplem2  19350  xkoptsub  19362  pt1hmeo  19514  ptcmpfi  19521  ptcmplem1  19759  ptcmpg  19764  prdstmdd  19829  prdstgpd  19830  tsmssubm  19851  ismet2  20043  prdsxmetlem  20078  imasdsf1olem  20083  prdsms  20241  isngp2  20324  metdscn  20567  cncfss  20610  ipcn  20893  lmmbr  20904  causs  20944  equivcau  20946  lmcau  20958  ovolfioo  21086  ovolficc  21087  ovolfsf  21090  elovolm  21093  ovollb  21097  ovolunlem1a  21114  ovolunlem1  21115  ovolicc2lem1  21135  ovolicc2lem2  21136  ovolicc2lem3  21137  ovolicc2lem4  21138  ovolicc2  21140  uniiccdif  21194  uniioovol  21195  uniiccvol  21196  uniioombllem2  21199  uniioombllem3a  21200  uniioombllem3  21201  uniioombllem4  21202  uniioombllem5  21203  uniioombl  21205  dyadmbl  21216  vitalilem3  21226  vitalilem4  21227  vitalilem5  21228  ismbf  21244  mbfid  21250  0plef  21286  i1f1  21304  i1faddlem  21307  i1fmulclem  21316  i1fres  21319  i1fsub  21322  itg1sub  21323  mbfi1fseqlem4  21332  itg2le  21353  itg2mulclem  21360  itg2mulc  21361  itg2monolem1  21364  itg2monolem2  21365  itg2monolem3  21366  itg2mono  21367  itg2i1fseqle  21368  itg2i1fseq3  21371  itg2addlem  21372  itg2gt0  21374  itg2cnlem1  21375  itg2cnlem2  21376  limccnp  21502  dvcmulf  21555  dvcobr  21556  dvfre  21561  dvnfre  21562  dvcnvlem  21584  dvcnv  21585  dvef  21588  dvferm1  21593  dvferm2  21595  rolle  21598  dvgt0lem1  21610  dvivthlem1  21616  dvne0  21619  lhop1lem  21621  lhop2  21623  lhop  21624  dvcnvrelem1  21625  dvcnvre  21627  dvcvx  21628  dvfsumrlim  21639  tdeglem3  21664  elply2  21800  elplyr  21805  plyeq0lem  21814  plyaddlem  21819  plymullem  21820  dgrlem  21833  coeidlem  21841  taylthlem2  21975  taylth  21976  ulmcn  22000  iblulm  22008  efcvx  22050  dvrelog  22218  relogcn  22219  dvlog2  22234  leibpi  22473  efrlim  22499  jensenlem2  22517  jensen  22518  amgmlem  22519  amgm  22520  wilthlem2  22543  wilthlem3  22544  basellem7  22560  basellem9  22562  lgsfcl  22779  lgsdchr  22823  dchrvmasumlem1  22880  dchrisum0lem3  22904  axlowdimlem4  23363  axlowdimlem7  23366  axlowdimlem10  23369  umgra1  23432  umisuhgra  23433  2trllemH  23623  2trllemG  23629  constr1trl  23659  constr3trllem1  23708  constr3trllem3  23710  eupa0  23767  eupap1  23769  0oo  24361  minvecolem3  24449  minvecolem4  24453  hhsscms  24852  occllem  24878  chscllem2  25213  chscllem4  25215  pjhf  25283  nlelchi  25637  hmopidmchi  25727  pjinvari  25767  resf1o  26201  lmlim  26542  rge0scvg  26544  lmdvg  26548  lmdvglim  26549  rrhre  26612  esumsn  26680  esumfsupre  26685  hashf2  26698  eulerpartlems  26907  eulerpartlemgs2  26927  coinfliprv  27029  ptpcon  27286  fprb  27748  mblfinlem2  28597  mbfresfi  28606  itg2addnclem  28611  itg2addnclem2  28612  itg2addnc  28614  itg2gt0cn  28615  ftc1anclem8  28642  fdc  28809  heiborlem6  28883  heibor  28888  ismrc  29205  mapfzcons  29220  mzpexpmpt  29249  mzpresrename  29255  diophrw  29265  rabren3dioph  29322  pwssplit4  29610  lnrfg  29643  seff  29763  sblpnf  29764  climreeq  29954  stoweidlem39  30002  stoweidlem44  30007  stoweidlem59  30022  stirlinglem8  30044  mapsnop  30903  mapprop  30904  zlmodzxzel  30920  mat1dimelbas  31053  mat1dimmul  31058  snlindsntorlem  31156  zlmodzxzldeplem1  31194  lfl0f  33072  dochpolN  35493
  Copyright terms: Public domain W3C validator