Theorem fss 6712

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 3946	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 33	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 623	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6529	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6529	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 412	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3907  ran crn 5653   Fn wfn 6520  ⟶wf 6521

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3924  df-f 6529

This theorem is referenced by:  fssd  6713  f1ss  6771  fcdmssb  7107  fsn2  7122  fprb  7182  ofco  7689  ffoss  7931  issmo2  8324  smoiso  8337  ssdomg  8985  alephfplem4  10079  cofsmo  10241  fin23lem17  10310  hsmexlem1  10398  axdc3lem4  10425  ac6s  10456  gruen  10785  intgru  10787  ingru  10788  hashf1lem1  14482  sswrd  14549  repsdf2  14805  limsupgre  15522  abscn2  15640  recn2  15642  imcn2  15643  climabs  15645  climre  15647  climim  15648  rlimabs  15650  rlimre  15652  rlimim  15653  caucvgrlem  15714  caurcvgr  15715  caucvgrlem2  15716  caurcvg  15718  fsumre  15850  fsumim  15851  0ram  17070  ramub1  17078  ramcl  17079  acsinfd  18602  acsdomd  18603  gsumval1  18731  resmgmhm2  18760  resmhm2  18870  prdsgrpd  19107  prdsinvgd  19108  symgtrinv  19533  prdscmnd  19922  prdsabld  19923  pgpfaclem1  20144  prdsrngd  20245  prdsmulrcl  20392  prdsringd  20393  prdscrngd  20394  abvf  20887  prdslmodd  21059  zntoslem  21666  regsumsupp  21732  dsmmsubg  21853  dsmmlss  21854  islinds2  21923  lindsmm  21938  lsslindf  21940  psrridm  22072  coe1fval3  22328  1stccnp  23580  1stckgen  23672  prdstps  23747  pthaus  23756  txcmplem2  23760  ptcmpfi  23931  ptcmplem1  24170  ptcmpg  24175  prdstmdd  24242  prdstgpd  24243  ismet2  24451  prdsxmetlem  24486  imasdsf1olem  24491  prdsms  24649  isngp2  24715  metdscn  24975  lmmbr  25378  causs  25418  ovolfioo  25587  ovolficc  25588  ovolfsf  25591  elovolm  25595  ovollb  25599  ovolunlem1a  25616  ovolunlem1  25617  ovolicc2lem1  25637  ovolicc2lem2  25638  ovolicc2lem3  25639  ovolicc2lem4  25640  ovolicc2  25642  uniiccdif  25698  uniioovol  25699  uniiccvol  25700  uniioombllem2  25703  uniioombllem3a  25704  uniioombllem3  25705  uniioombllem4  25706  uniioombllem5  25707  uniioombl  25709  dyadmbl  25720  vitalilem3  25730  vitalilem4  25731  vitalilem5  25732  ismbf  25748  mbfid  25755  0plef  25792  i1f1  25810  i1faddlem  25813  i1fsub  25828  itg1sub  25829  mbfi1fseqlem4  25838  itg2le  25859  itg2mulclem  25866  itg2mulc  25867  itg2monolem1  25870  itg2monolem2  25871  itg2monolem3  25872  itg2mono  25873  itg2i1fseq3  25877  itg2addlem  25878  itg2gt0  25880  itg2cnlem1  25881  itg2cnlem2  25882  dvfre  26071  dvnfre  26072  dvferm1  26105  dvferm2  26107  rolle  26110  dvgt0lem1  26122  dvivthlem1  26128  dvne0  26131  lhop1lem  26133  lhop2  26135  lhop  26136  dvcnvrelem1  26137  dvcnvre  26139  dvcvx  26140  dvfsumrlim  26151  tdeglem3  26177  elplyr  26319  taylthlem2  26495  taylth  26496  ulmcn  26520  iblulm  26528  efcvx  26570  dvrelog  26760  relogcn  26761  dvlog2  26776  leibpi  27065  efrlim  27092  jensenlem2  27110  jensen  27111  amgmlem  27112  amgm  27113  wilthlem2  27191  wilthlem3  27192  basellem7  27209  basellem9  27211  lgsfcl  27427  lgsdchr  27477  dchrvmasumlem1  27617  dchrisum0lem3  27641  axlowdimlem4  29204  axlowdimlem7  29207  axlowdimlem10  29210  upgruhgr  29361  konigsbergssiedgw  30510  pliguhgr  30747  0oo  31050  hhsscms  31539  nlelchi  32322  hmopidmchi  32412  pjinvari  32452  padct  32975  smatrcl  34103  lmlim  34254  rge0scvg  34256  lmdvg  34260  lmdvglim  34261  rrhre  34328  esumfsupre  34378  hashf2  34391  eulerpartlems  34667  eulerpartlemgs2  34687  coinfliprv  34790  fdvposlt  34903  fdvposle  34905  breprexpnat  34938  circlemethnat  34945  circlevma  34946  tgoldbachgtde  34964  lfuhgr  35481  subgrwlk  35495  ptpconn  35596  poimirlem8  38139  poimirlem18  38149  poimirlem21  38152  poimirlem22  38153  mblfinlem2  38169  mbfresfi  38177  itg2addnclem  38182  itg2addnclem2  38183  itg2addnc  38185  itg2gt0cn  38186  ftc1anclem8  38211  fdc  38256  heiborlem6  38327  heibor  38332  lfl0f  39705  intlewftc  42690  sticksstones3  42777  sticksstones9  42783  sticksstones11  42785  sticksstones17  42792  sticksstones18  42793  aks6d1c6lem5  42806  mzpexpmpt  43338  mzpresrename  43343  diophrw  43352  rabren3dioph  43404  lnrfg  43708  seff  44883  sblpnf  44884  binomcxplemnotnn0  44930  stoweidlem44  46616  stirlinglem8  46653  fourierdlem62  46740  fouriersw  46803  nnsum3primes4  48408  grtriclwlk3  48565  zlmodzxzldeplem1  49131  aacllem  50430  amgmwlem  50431