Theorem fss 5744

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

Proof of Theorem fss

Step	Hyp	Ref	Expression
1		sstr2 3510	. . . . 5
2	1	com12 31	. . . 4
3	2	anim2d 565	. . 3
4		df-f 5597	. . 3
5		df-f 5597	. . 3
6	3, 4, 5	3imtr4g 270	. 2
7	6	impcom 430	1

Syntax hints:  ->wi 4  /\wa 369  C_wss 3475  rancrn 5005  Fnwfn 5588  -->wf 5589

This theorem is referenced by:  fssd  5745  f1ss  5791  fsn2  6071  ofco  6560  ffoss  6761  issmo2  7039  smoiso  7052  mapsn  7480  ssdomg  7581  alephfplem4  8509  cofsmo  8670  fin23lem17  8739  hsmexlem1  8827  axdc3lem4  8854  ac6s  8885  gruen  9211  intgru  9213  ingru  9214  1fv  11821  hashf1lem1  12504  sswrd  12555  repsdf2  12750  limsupgre  13304  abscn2  13421  recn2  13423  imcn2  13424  climabs  13426  climre  13428  climim  13429  rlimabs  13431  rlimre  13433  rlimim  13434  caucvgrlem  13495  caurcvgr  13496  caucvgrlem2  13497  caurcvg  13499  fsumre  13622  fsumim  13623  0ram  14538  ramub1  14546  ramcl  14547  acsinfd  15810  acsdomd  15811  gsumval1  15904  resmhm2  15991  prdsgrpd  16179  prdsinvgd  16180  symgtrinv  16497  prdscmnd  16867  prdsabld  16868  gsumval3OLD  16908  gsumsubmclOLD  16931  gsumzaddOLD  16937  gsumzoppgOLD  16968  pgpfaclem1  17132  prdsringd  17261  prdscrngd  17262  abvf  17472  prdslmodd  17615  psrridm  18058  psrridmOLD  18059  coe1fval3  18247  zntoslem  18595  frgpcyg  18612  regsumsupp  18658  dsmmsubg  18774  dsmmlss  18775  islinds2  18848  lindsmm  18863  lsslindf  18865  1stccnp  19963  1stckgen  20055  prdstps  20130  pthaus  20139  txcmplem2  20143  ptcmpfi  20314  ptcmplem1  20552  ptcmpg  20557  prdstmdd  20622  prdstgpd  20623  ismet2  20836  prdsxmetlem  20871  imasdsf1olem  20876  prdsms  21034  isngp2  21117  metdscn  21360  lmmbr  21697  causs  21737  ovolfioo  21879  ovolficc  21880  ovolfsf  21883  elovolm  21886  ovollb  21890  ovolunlem1a  21907  ovolunlem1  21908  ovolicc2lem1  21928  ovolicc2lem2  21929  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2  21933  uniiccdif  21987  uniioovol  21988  uniiccvol  21989  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombl  21998  dyadmbl  22009  vitalilem3  22019  vitalilem4  22020  vitalilem5  22021  ismbf  22037  mbfid  22043  0plef  22079  i1f1  22097  i1faddlem  22100  i1fsub  22115  itg1sub  22116  mbfi1fseqlem4  22125  itg2le  22146  itg2mulclem  22153  itg2mulc  22154  itg2monolem1  22157  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  itg2i1fseqle  22161  itg2i1fseq3  22164  itg2addlem  22165  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  dvfre  22354  dvnfre  22355  dvferm1  22386  dvferm2  22388  rolle  22391  dvgt0lem1  22403  dvivthlem1  22409  dvne0  22412  lhop1lem  22414  lhop2  22416  lhop  22417  dvcnvrelem1  22418  dvcnvre  22420  dvcvx  22421  dvfsumrlim  22432  tdeglem3  22457  elplyr  22598  taylthlem2  22769  taylth  22770  ulmcn  22794  iblulm  22802  efcvx  22844  dvrelog  23018  relogcn  23019  dvlog2  23034  leibpi  23273  efrlim  23299  jensenlem2  23317  jensen  23318  amgmlem  23319  amgm  23320  wilthlem2  23343  wilthlem3  23344  basellem7  23360  basellem9  23362  lgsfcl  23579  lgsdchr  23623  dchrvmasumlem1  23680  dchrisum0lem3  23704  axlowdimlem4  24248  axlowdimlem7  24251  axlowdimlem10  24254  umisuhgra  24327  2trllemG  24560  constr3trllem1  24650  0oo  25704  hhsscms  26195  nlelchi  26980  hmopidmchi  27070  pjinvari  27110  lmlim  27929  rge0scvg  27931  lmdvg  27935  lmdvglim  27936  rrhre  27999  esumfsupre  28077  hashf2  28090  eulerpartlems  28299  eulerpartlemgs2  28319  coinfliprv  28421  ptpcon  28678  fprb  29203  mblfinlem2  30052  mbfresfi  30061  itg2addnclem  30066  itg2addnclem2  30067  itg2addnc  30069  itg2gt0cn  30070  ftc1anclem8  30097  fdc  30238  heiborlem6  30312  heibor  30317  mzpexpmpt  30677  mzpresrename  30683  diophrw  30692  rabren3dioph  30749  lnrfg  31068  seff  31189  sblpnf  31190  binomcxplemnotnn0  31261  stoweidlem44  31826  stirlinglem8  31863  fourierdlem62  31951  fouriersw  32014  resmgmhm2  32487  zlmodzxzldeplem1  33101  aacllem  33216  lfl0f  34794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597