Theorem fss 6686

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3920  df-f 6504

This theorem is referenced by:  fssd  6687  f1ss  6743  fcdmssb  7076  fsn2  7091  fprb  7150  ofco  7657  ffoss  7900  issmo2  8291  smoiso  8304  ssdomg  8949  alephfplem4  10029  cofsmo  10191  fin23lem17  10260  hsmexlem1  10348  axdc3lem4  10375  ac6s  10406  gruen  10735  intgru  10737  ingru  10738  hashf1lem1  14390  sswrd  14457  repsdf2  14713  limsupgre  15416  abscn2  15534  recn2  15536  imcn2  15537  climabs  15539  climre  15541  climim  15542  rlimabs  15544  rlimre  15546  rlimim  15547  caucvgrlem  15608  caurcvgr  15609  caucvgrlem2  15610  caurcvg  15612  fsumre  15743  fsumim  15744  0ram  16960  ramub1  16968  ramcl  16969  acsinfd  18491  acsdomd  18492  gsumval1  18620  resmgmhm2  18649  resmhm2  18758  prdsgrpd  18992  prdsinvgd  18993  symgtrinv  19413  prdscmnd  19802  prdsabld  19803  pgpfaclem1  20024  prdsrngd  20123  prdsmulrcl  20267  prdsringd  20268  prdscrngd  20269  abvf  20760  prdslmodd  20932  zntoslem  21523  regsumsupp  21589  dsmmsubg  21710  dsmmlss  21711  islinds2  21780  lindsmm  21795  lsslindf  21797  psrridm  21930  coe1fval3  22161  1stccnp  23418  1stckgen  23510  prdstps  23585  pthaus  23594  txcmplem2  23598  ptcmpfi  23769  ptcmplem1  24008  ptcmpg  24013  prdstmdd  24080  prdstgpd  24081  ismet2  24289  prdsxmetlem  24324  imasdsf1olem  24329  prdsms  24487  isngp2  24553  metdscn  24813  lmmbr  25226  causs  25266  ovolfioo  25436  ovolficc  25437  ovolfsf  25440  elovolm  25444  ovollb  25448  ovolunlem1a  25465  ovolunlem1  25466  ovolicc2lem1  25486  ovolicc2lem2  25487  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2  25491  uniiccdif  25547  uniioovol  25548  uniiccvol  25549  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  uniioombl  25558  dyadmbl  25569  vitalilem3  25579  vitalilem4  25580  vitalilem5  25581  ismbf  25597  mbfid  25604  0plef  25641  i1f1  25659  i1faddlem  25662  i1fsub  25677  itg1sub  25678  mbfi1fseqlem4  25687  itg2le  25708  itg2mulclem  25715  itg2mulc  25716  itg2monolem1  25719  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2i1fseq3  25726  itg2addlem  25727  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  dvfre  25923  dvnfre  25924  dvferm1  25957  dvferm2  25959  rolle  25962  dvgt0lem1  25975  dvivthlem1  25981  dvne0  25984  lhop1lem  25986  lhop2  25988  lhop  25989  dvcnvrelem1  25990  dvcnvre  25992  dvcvx  25993  dvfsumrlim  26006  tdeglem3  26032  elplyr  26174  taylthlem2  26350  taylthlem2OLD  26351  taylth  26352  ulmcn  26376  iblulm  26384  efcvx  26427  dvrelog  26614  relogcn  26615  dvlog2  26630  leibpi  26920  efrlim  26947  efrlimOLD  26948  jensenlem2  26966  jensen  26967  amgmlem  26968  amgm  26969  wilthlem2  27047  wilthlem3  27048  basellem7  27065  basellem9  27067  lgsfcl  27284  lgsdchr  27334  dchrvmasumlem1  27474  dchrisum0lem3  27498  axlowdimlem4  29030  axlowdimlem7  29033  axlowdimlem10  29036  upgruhgr  29187  konigsbergssiedgw  30337  pliguhgr  30573  0oo  30876  hhsscms  31365  nlelchi  32148  hmopidmchi  32238  pjinvari  32278  padct  32807  smatrcl  33973  lmlim  34124  rge0scvg  34126  lmdvg  34130  lmdvglim  34131  rrhre  34198  esumfsupre  34248  hashf2  34261  eulerpartlems  34537  eulerpartlemgs2  34557  coinfliprv  34660  fdvposlt  34776  fdvposle  34778  breprexpnat  34811  circlemethnat  34818  circlevma  34819  tgoldbachgtde  34837  lfuhgr  35331  subgrwlk  35345  ptpconn  35446  poimirlem8  37873  poimirlem18  37883  poimirlem21  37886  poimirlem22  37887  mblfinlem2  37903  mbfresfi  37911  itg2addnclem  37916  itg2addnclem2  37917  itg2addnc  37919  itg2gt0cn  37920  ftc1anclem8  37945  fdc  37990  heiborlem6  38061  heibor  38066  lfl0f  39439  intlewftc  42425  sticksstones3  42512  sticksstones9  42518  sticksstones11  42520  sticksstones17  42527  sticksstones18  42528  aks6d1c6lem5  42541  mzpexpmpt  43096  mzpresrename  43101  diophrw  43110  rabren3dioph  43166  lnrfg  43470  seff  44659  sblpnf  44660  binomcxplemnotnn0  44706  stoweidlem44  46396  stirlinglem8  46433  fourierdlem62  46520  fouriersw  46583  nnsum3primes4  48142  grtriclwlk3  48299  zlmodzxzldeplem1  48854  aacllem  50154  amgmwlem  50155