Theorem fss 6707

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 3956	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 612	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6518	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6518	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 407	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3934  df-f 6518

This theorem is referenced by:  fssd  6708  f1ss  6764  fcdmssb  7097  fsn2  7111  fprb  7171  ofco  7681  ffoss  7927  issmo2  8321  smoiso  8334  ssdomg  8974  alephfplem4  10067  cofsmo  10229  fin23lem17  10298  hsmexlem1  10386  axdc3lem4  10413  ac6s  10444  gruen  10772  intgru  10774  ingru  10775  hashf1lem1  14427  sswrd  14494  repsdf2  14750  limsupgre  15454  abscn2  15572  recn2  15574  imcn2  15575  climabs  15577  climre  15579  climim  15580  rlimabs  15582  rlimre  15584  rlimim  15585  caucvgrlem  15646  caurcvgr  15647  caucvgrlem2  15648  caurcvg  15650  fsumre  15781  fsumim  15782  0ram  16998  ramub1  17006  ramcl  17007  acsinfd  18522  acsdomd  18523  gsumval1  18617  resmgmhm2  18646  resmhm2  18755  prdsgrpd  18989  prdsinvgd  18990  symgtrinv  19409  prdscmnd  19798  prdsabld  19799  pgpfaclem1  20020  prdsrngd  20092  prdsmulrcl  20236  prdsringd  20237  prdscrngd  20238  abvf  20731  prdslmodd  20882  zntoslem  21473  regsumsupp  21538  dsmmsubg  21659  dsmmlss  21660  islinds2  21729  lindsmm  21744  lsslindf  21746  psrridm  21879  coe1fval3  22100  1stccnp  23356  1stckgen  23448  prdstps  23523  pthaus  23532  txcmplem2  23536  ptcmpfi  23707  ptcmplem1  23946  ptcmpg  23951  prdstmdd  24018  prdstgpd  24019  ismet2  24228  prdsxmetlem  24263  imasdsf1olem  24268  prdsms  24426  isngp2  24492  metdscn  24752  lmmbr  25165  causs  25205  ovolfioo  25375  ovolficc  25376  ovolfsf  25379  elovolm  25383  ovollb  25387  ovolunlem1a  25404  ovolunlem1  25405  ovolicc2lem1  25425  ovolicc2lem2  25426  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2  25430  uniiccdif  25486  uniioovol  25487  uniiccvol  25488  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  uniioombl  25497  dyadmbl  25508  vitalilem3  25518  vitalilem4  25519  vitalilem5  25520  ismbf  25536  mbfid  25543  0plef  25580  i1f1  25598  i1faddlem  25601  i1fsub  25616  itg1sub  25617  mbfi1fseqlem4  25626  itg2le  25647  itg2mulclem  25654  itg2mulc  25655  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2i1fseq3  25665  itg2addlem  25666  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  dvfre  25862  dvnfre  25863  dvferm1  25896  dvferm2  25898  rolle  25901  dvgt0lem1  25914  dvivthlem1  25920  dvne0  25923  lhop1lem  25925  lhop2  25927  lhop  25928  dvcnvrelem1  25929  dvcnvre  25931  dvcvx  25932  dvfsumrlim  25945  tdeglem3  25971  elplyr  26113  taylthlem2  26289  taylthlem2OLD  26290  taylth  26291  ulmcn  26315  iblulm  26323  efcvx  26366  dvrelog  26553  relogcn  26554  dvlog2  26569  leibpi  26859  efrlim  26886  efrlimOLD  26887  jensenlem2  26905  jensen  26906  amgmlem  26907  amgm  26908  wilthlem2  26986  wilthlem3  26987  basellem7  27004  basellem9  27006  lgsfcl  27223  lgsdchr  27273  dchrvmasumlem1  27413  dchrisum0lem3  27437  axlowdimlem4  28879  axlowdimlem7  28882  axlowdimlem10  28885  upgruhgr  29036  konigsbergssiedgw  30186  pliguhgr  30422  0oo  30725  hhsscms  31214  nlelchi  31997  hmopidmchi  32087  pjinvari  32127  padct  32650  smatrcl  33793  lmlim  33944  rge0scvg  33946  lmdvg  33950  lmdvglim  33951  rrhre  34018  esumfsupre  34068  hashf2  34081  eulerpartlems  34358  eulerpartlemgs2  34378  coinfliprv  34481  fdvposlt  34597  fdvposle  34599  breprexpnat  34632  circlemethnat  34639  circlevma  34640  tgoldbachgtde  34658  lfuhgr  35112  subgrwlk  35126  ptpconn  35227  poimirlem8  37629  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  mblfinlem2  37659  mbfresfi  37667  itg2addnclem  37672  itg2addnclem2  37673  itg2addnc  37675  itg2gt0cn  37676  ftc1anclem8  37701  fdc  37746  heiborlem6  37817  heibor  37822  lfl0f  39069  intlewftc  42056  sticksstones3  42143  sticksstones9  42149  sticksstones11  42151  sticksstones17  42158  sticksstones18  42159  aks6d1c6lem5  42172  mzpexpmpt  42740  mzpresrename  42745  diophrw  42754  rabren3dioph  42810  lnrfg  43115  seff  44305  sblpnf  44306  binomcxplemnotnn0  44352  stoweidlem44  46049  stirlinglem8  46086  fourierdlem62  46173  fouriersw  46236  nnsum3primes4  47793  grtriclwlk3  47948  zlmodzxzldeplem1  48493  aacllem  49794  amgmwlem  49795