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 3944	. . . . 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 3905  ran crn 5624   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 1795  ax-4 1809

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

This theorem is referenced by:  fssd  6673  f1ss  6729  fcdmssb  7060  fsn2  7074  fprb  7134  ofco  7642  ffoss  7888  issmo2  8279  smoiso  8292  ssdomg  8932  alephfplem4  10020  cofsmo  10182  fin23lem17  10251  hsmexlem1  10339  axdc3lem4  10366  ac6s  10397  gruen  10725  intgru  10727  ingru  10728  hashf1lem1  14380  sswrd  14447  repsdf2  14702  limsupgre  15406  abscn2  15524  recn2  15526  imcn2  15527  climabs  15529  climre  15531  climim  15532  rlimabs  15534  rlimre  15536  rlimim  15537  caucvgrlem  15598  caurcvgr  15599  caucvgrlem2  15600  caurcvg  15602  fsumre  15733  fsumim  15734  0ram  16950  ramub1  16958  ramcl  16959  acsinfd  18480  acsdomd  18481  gsumval1  18575  resmgmhm2  18604  resmhm2  18713  prdsgrpd  18947  prdsinvgd  18948  symgtrinv  19369  prdscmnd  19758  prdsabld  19759  pgpfaclem1  19980  prdsrngd  20079  prdsmulrcl  20223  prdsringd  20224  prdscrngd  20225  abvf  20718  prdslmodd  20890  zntoslem  21481  regsumsupp  21547  dsmmsubg  21668  dsmmlss  21669  islinds2  21738  lindsmm  21753  lsslindf  21755  psrridm  21888  coe1fval3  22109  1stccnp  23365  1stckgen  23457  prdstps  23532  pthaus  23541  txcmplem2  23545  ptcmpfi  23716  ptcmplem1  23955  ptcmpg  23960  prdstmdd  24027  prdstgpd  24028  ismet2  24237  prdsxmetlem  24272  imasdsf1olem  24277  prdsms  24435  isngp2  24501  metdscn  24761  lmmbr  25174  causs  25214  ovolfioo  25384  ovolficc  25385  ovolfsf  25388  elovolm  25392  ovollb  25396  ovolunlem1a  25413  ovolunlem1  25414  ovolicc2lem1  25434  ovolicc2lem2  25435  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2  25439  uniiccdif  25495  uniioovol  25496  uniiccvol  25497  uniioombllem2  25500  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  uniioombl  25506  dyadmbl  25517  vitalilem3  25527  vitalilem4  25528  vitalilem5  25529  ismbf  25545  mbfid  25552  0plef  25589  i1f1  25607  i1faddlem  25610  i1fsub  25625  itg1sub  25626  mbfi1fseqlem4  25635  itg2le  25656  itg2mulclem  25663  itg2mulc  25664  itg2monolem1  25667  itg2monolem2  25668  itg2monolem3  25669  itg2mono  25670  itg2i1fseq3  25674  itg2addlem  25675  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  dvfre  25871  dvnfre  25872  dvferm1  25905  dvferm2  25907  rolle  25910  dvgt0lem1  25923  dvivthlem1  25929  dvne0  25932  lhop1lem  25934  lhop2  25936  lhop  25937  dvcnvrelem1  25938  dvcnvre  25940  dvcvx  25941  dvfsumrlim  25954  tdeglem3  25980  elplyr  26122  taylthlem2  26298  taylthlem2OLD  26299  taylth  26300  ulmcn  26324  iblulm  26332  efcvx  26375  dvrelog  26562  relogcn  26563  dvlog2  26578  leibpi  26868  efrlim  26895  efrlimOLD  26896  jensenlem2  26914  jensen  26915  amgmlem  26916  amgm  26917  wilthlem2  26995  wilthlem3  26996  basellem7  27013  basellem9  27015  lgsfcl  27232  lgsdchr  27282  dchrvmasumlem1  27422  dchrisum0lem3  27446  axlowdimlem4  28908  axlowdimlem7  28911  axlowdimlem10  28914  upgruhgr  29065  konigsbergssiedgw  30212  pliguhgr  30448  0oo  30751  hhsscms  31240  nlelchi  32023  hmopidmchi  32113  pjinvari  32153  padct  32676  smatrcl  33762  lmlim  33913  rge0scvg  33915  lmdvg  33919  lmdvglim  33920  rrhre  33987  esumfsupre  34037  hashf2  34050  eulerpartlems  34327  eulerpartlemgs2  34347  coinfliprv  34450  fdvposlt  34566  fdvposle  34568  breprexpnat  34601  circlemethnat  34608  circlevma  34609  tgoldbachgtde  34627  lfuhgr  35090  subgrwlk  35104  ptpconn  35205  poimirlem8  37607  poimirlem18  37617  poimirlem21  37620  poimirlem22  37621  mblfinlem2  37637  mbfresfi  37645  itg2addnclem  37650  itg2addnclem2  37651  itg2addnc  37653  itg2gt0cn  37654  ftc1anclem8  37679  fdc  37724  heiborlem6  37795  heibor  37800  lfl0f  39047  intlewftc  42034  sticksstones3  42121  sticksstones9  42127  sticksstones11  42129  sticksstones17  42136  sticksstones18  42137  aks6d1c6lem5  42150  mzpexpmpt  42718  mzpresrename  42723  diophrw  42732  rabren3dioph  42788  lnrfg  43092  seff  44282  sblpnf  44283  binomcxplemnotnn0  44329  stoweidlem44  46026  stirlinglem8  46063  fourierdlem62  46150  fouriersw  46213  nnsum3primes4  47773  grtriclwlk3  47930  zlmodzxzldeplem1  48486  aacllem  49787  amgmwlem  49788