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

Theorem fss 5697
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 3414 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 32 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 567 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 5548 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 5548 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 273 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 431 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    C_ wss 3379   ran crn 4797    Fn wfn 5539   -->wf 5540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3386  df-ss 3393  df-f 5548
This theorem is referenced by:  fssd  5698  f1ss  5744  fsn2  6021  fsnex  6140  ofco  6509  ffoss  6712  issmo2  7023  smoiso  7036  mapsn  7468  ssdomg  7569  alephfplem4  8489  cofsmo  8650  fin23lem17  8719  hsmexlem1  8807  axdc3lem4  8834  ac6s  8865  gruen  9188  intgru  9190  ingru  9191  1fv  11859  hashf1lem1  12566  sswrd  12627  sswrdOLD  12628  repsdf2  12827  limsupgre  13485  limsupgreOLD  13486  abscn2  13605  recn2  13607  imcn2  13608  climabs  13610  climre  13612  climim  13613  rlimabs  13615  rlimre  13617  rlimim  13618  caucvgrlem  13679  caucvgrlemOLD  13680  caurcvgr  13681  caurcvgrOLD  13682  caucvgrlem2  13683  caurcvg  13685  caurcvgOLD  13686  fsumre  13811  fsumim  13812  0ram  14921  ramub1  14929  ramcl  14930  acsinfd  16369  acsdomd  16370  gsumval1  16463  resmhm2  16550  prdsgrpd  16738  prdsinvgd  16739  symgtrinv  17056  prdscmnd  17442  prdsabld  17443  pgpfaclem1  17657  prdsringd  17783  prdscrngd  17784  abvf  17994  prdslmodd  18135  psrridm  18571  coe1fval3  18744  zntoslem  19069  frgpcyg  19086  regsumsupp  19132  dsmmsubg  19248  dsmmlss  19249  islinds2  19313  lindsmm  19328  lsslindf  19330  1stccnp  20419  1stckgen  20511  prdstps  20586  pthaus  20595  txcmplem2  20599  ptcmpfi  20770  ptcmplem1  21009  ptcmpg  21014  prdstmdd  21080  prdstgpd  21081  ismet2  21290  prdsxmetlem  21325  imasdsf1olem  21330  prdsms  21488  isngp2  21553  metdscn  21815  metdscnOLD  21830  lmmbr  22170  causs  22210  ovolfioo  22362  ovolficc  22363  ovolfsf  22366  elovolm  22370  ovollb  22374  ovolunlem1a  22391  ovolunlem1  22392  ovolicc2lem1  22412  ovolicc2lem2  22413  ovolicc2lem3  22414  ovolicc2lem4OLD  22415  ovolicc2lem4  22416  ovolicc2  22418  uniiccdif  22477  uniioovol  22478  uniiccvol  22479  uniioombllem2  22482  uniioombllem2OLD  22483  uniioombllem3a  22484  uniioombllem3  22485  uniioombllem4  22486  uniioombllem5  22487  uniioombl  22489  dyadmbl  22500  vitalilem3  22510  vitalilem4  22511  vitalilem5  22512  ismbf  22528  mbfid  22534  0plef  22572  i1f1  22590  i1faddlem  22593  i1fsub  22608  itg1sub  22609  mbfi1fseqlem4  22618  itg2le  22639  itg2mulclem  22646  itg2mulc  22647  itg2monolem1  22650  itg2monolem2  22651  itg2monolem3  22652  itg2mono  22653  itg2i1fseqle  22654  itg2i1fseq3  22657  itg2addlem  22658  itg2gt0  22660  itg2cnlem1  22661  itg2cnlem2  22662  dvfre  22847  dvnfre  22848  dvferm1  22879  dvferm2  22881  rolle  22884  dvgt0lem1  22896  dvivthlem1  22902  dvne0  22905  lhop1lem  22907  lhop2  22909  lhop  22910  dvcnvrelem1  22911  dvcnvre  22913  dvcvx  22914  dvfsumrlim  22925  tdeglem3  22950  elplyr  23097  taylthlem2  23271  taylth  23272  ulmcn  23296  iblulm  23304  efcvx  23346  dvrelog  23524  relogcn  23525  dvlog2  23540  leibpi  23810  efrlim  23837  jensenlem2  23855  jensen  23856  amgmlem  23857  amgm  23858  wilthlem2  23936  wilthlem3  23937  basellem7  23955  basellem9  23957  lgsfcl  24174  lgsdchr  24218  dchrvmasumlem1  24275  dchrisum0lem3  24299  axlowdimlem4  24917  axlowdimlem7  24920  axlowdimlem10  24923  umisuhgra  24996  2trllemG  25230  constr3trllem1  25320  0oo  26372  hhsscms  26872  nlelchi  27656  hmopidmchi  27746  pjinvari  27786  padct  28257  smatrcl  28574  lmlim  28705  rge0scvg  28707  lmdvg  28711  lmdvglim  28712  rrhre  28777  esumfsupre  28844  hashf2  28857  eulerpartlems  29145  eulerpartlemgs2  29165  coinfliprv  29267  ptpcon  29908  fprb  30364  poimirlem8  31855  poimirlem18  31865  poimirlem21  31868  poimirlem22  31869  mblfinlem2  31885  mbfresfi  31894  itg2addnclem  31900  itg2addnclem2  31901  itg2addnc  31903  itg2gt0cn  31904  ftc1anclem8  31931  fdc  31981  heiborlem6  32055  heibor  32060  lfl0f  32547  mzpexpmpt  35499  mzpresrename  35504  diophrw  35513  rabren3dioph  35570  lnrfg  35891  seff  36570  sblpnf  36571  binomcxplemnotnn0  36618  stoweidlem44  37788  stirlinglem8  37826  fourierdlem62  37915  fouriersw  37978  nnsum3primes4  38696  upgruhgr  38965  resmgmhm2  39390  zlmodzxzldeplem1  39886  aacllem  40133
  Copyright terms: Public domain W3C validator