Theorem fss 6672

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3898  ran crn 5620   Fn wfn 6481  ⟶wf 6482

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3915  df-f 6490

This theorem is referenced by:  fssd  6673  f1ss  6729  fcdmssb  7061  fsn2  7075  fprb  7134  ofco  7641  ffoss  7884  issmo2  8275  smoiso  8288  ssdomg  8929  alephfplem4  10005  cofsmo  10167  fin23lem17  10236  hsmexlem1  10324  axdc3lem4  10351  ac6s  10382  gruen  10710  intgru  10712  ingru  10713  hashf1lem1  14364  sswrd  14431  repsdf2  14687  limsupgre  15390  abscn2  15508  recn2  15510  imcn2  15511  climabs  15513  climre  15515  climim  15516  rlimabs  15518  rlimre  15520  rlimim  15521  caucvgrlem  15582  caurcvgr  15583  caucvgrlem2  15584  caurcvg  15586  fsumre  15717  fsumim  15718  0ram  16934  ramub1  16942  ramcl  16943  acsinfd  18464  acsdomd  18465  gsumval1  18593  resmgmhm2  18622  resmhm2  18731  prdsgrpd  18965  prdsinvgd  18966  symgtrinv  19386  prdscmnd  19775  prdsabld  19776  pgpfaclem1  19997  prdsrngd  20096  prdsmulrcl  20240  prdsringd  20241  prdscrngd  20242  abvf  20732  prdslmodd  20904  zntoslem  21495  regsumsupp  21561  dsmmsubg  21682  dsmmlss  21683  islinds2  21752  lindsmm  21767  lsslindf  21769  psrridm  21901  coe1fval3  22122  1stccnp  23378  1stckgen  23470  prdstps  23545  pthaus  23554  txcmplem2  23558  ptcmpfi  23729  ptcmplem1  23968  ptcmpg  23973  prdstmdd  24040  prdstgpd  24041  ismet2  24249  prdsxmetlem  24284  imasdsf1olem  24289  prdsms  24447  isngp2  24513  metdscn  24773  lmmbr  25186  causs  25226  ovolfioo  25396  ovolficc  25397  ovolfsf  25400  elovolm  25404  ovollb  25408  ovolunlem1a  25425  ovolunlem1  25426  ovolicc2lem1  25446  ovolicc2lem2  25447  ovolicc2lem3  25448  ovolicc2lem4  25449  ovolicc2  25451  uniiccdif  25507  uniioovol  25508  uniiccvol  25509  uniioombllem2  25512  uniioombllem3a  25513  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  uniioombl  25518  dyadmbl  25529  vitalilem3  25539  vitalilem4  25540  vitalilem5  25541  ismbf  25557  mbfid  25564  0plef  25601  i1f1  25619  i1faddlem  25622  i1fsub  25637  itg1sub  25638  mbfi1fseqlem4  25647  itg2le  25668  itg2mulclem  25675  itg2mulc  25676  itg2monolem1  25679  itg2monolem2  25680  itg2monolem3  25681  itg2mono  25682  itg2i1fseq3  25686  itg2addlem  25687  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  dvfre  25883  dvnfre  25884  dvferm1  25917  dvferm2  25919  rolle  25922  dvgt0lem1  25935  dvivthlem1  25941  dvne0  25944  lhop1lem  25946  lhop2  25948  lhop  25949  dvcnvrelem1  25950  dvcnvre  25952  dvcvx  25953  dvfsumrlim  25966  tdeglem3  25992  elplyr  26134  taylthlem2  26310  taylthlem2OLD  26311  taylth  26312  ulmcn  26336  iblulm  26344  efcvx  26387  dvrelog  26574  relogcn  26575  dvlog2  26590  leibpi  26880  efrlim  26907  efrlimOLD  26908  jensenlem2  26926  jensen  26927  amgmlem  26928  amgm  26929  wilthlem2  27007  wilthlem3  27008  basellem7  27025  basellem9  27027  lgsfcl  27244  lgsdchr  27294  dchrvmasumlem1  27434  dchrisum0lem3  27458  axlowdimlem4  28925  axlowdimlem7  28928  axlowdimlem10  28931  upgruhgr  29082  konigsbergssiedgw  30232  pliguhgr  30468  0oo  30771  hhsscms  31260  nlelchi  32043  hmopidmchi  32133  pjinvari  32173  padct  32705  smatrcl  33830  lmlim  33981  rge0scvg  33983  lmdvg  33987  lmdvglim  33988  rrhre  34055  esumfsupre  34105  hashf2  34118  eulerpartlems  34394  eulerpartlemgs2  34414  coinfliprv  34517  fdvposlt  34633  fdvposle  34635  breprexpnat  34668  circlemethnat  34675  circlevma  34676  tgoldbachgtde  34694  lfuhgr  35183  subgrwlk  35197  ptpconn  35298  poimirlem8  37688  poimirlem18  37698  poimirlem21  37701  poimirlem22  37702  mblfinlem2  37718  mbfresfi  37726  itg2addnclem  37731  itg2addnclem2  37732  itg2addnc  37734  itg2gt0cn  37735  ftc1anclem8  37760  fdc  37805  heiborlem6  37876  heibor  37881  lfl0f  39188  intlewftc  42174  sticksstones3  42261  sticksstones9  42267  sticksstones11  42269  sticksstones17  42276  sticksstones18  42277  aks6d1c6lem5  42290  mzpexpmpt  42862  mzpresrename  42867  diophrw  42876  rabren3dioph  42932  lnrfg  43236  seff  44426  sblpnf  44427  binomcxplemnotnn0  44473  stoweidlem44  46166  stirlinglem8  46203  fourierdlem62  46290  fouriersw  46353  nnsum3primes4  47912  grtriclwlk3  48069  zlmodzxzldeplem1  48625  aacllem  49926  amgmwlem  49927