Theorem fss 6684

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

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 3906  df-f 6502

This theorem is referenced by:  fssd  6685  f1ss  6741  fcdmssb  7074  fsn2  7089  fprb  7149  ofco  7656  ffoss  7899  issmo2  8289  smoiso  8302  ssdomg  8947  alephfplem4  10029  cofsmo  10191  fin23lem17  10260  hsmexlem1  10348  axdc3lem4  10375  ac6s  10406  gruen  10735  intgru  10737  ingru  10738  hashf1lem1  14417  sswrd  14484  repsdf2  14740  limsupgre  15443  abscn2  15561  recn2  15563  imcn2  15564  climabs  15566  climre  15568  climim  15569  rlimabs  15571  rlimre  15573  rlimim  15574  caucvgrlem  15635  caurcvgr  15636  caucvgrlem2  15637  caurcvg  15639  fsumre  15771  fsumim  15772  0ram  16991  ramub1  16999  ramcl  17000  acsinfd  18522  acsdomd  18523  gsumval1  18651  resmgmhm2  18680  resmhm2  18789  prdsgrpd  19026  prdsinvgd  19027  symgtrinv  19447  prdscmnd  19836  prdsabld  19837  pgpfaclem1  20058  prdsrngd  20157  prdsmulrcl  20299  prdsringd  20300  prdscrngd  20301  abvf  20792  prdslmodd  20964  zntoslem  21536  regsumsupp  21602  dsmmsubg  21723  dsmmlss  21724  islinds2  21793  lindsmm  21808  lsslindf  21810  psrridm  21941  coe1fval3  22172  1stccnp  23427  1stckgen  23519  prdstps  23594  pthaus  23603  txcmplem2  23607  ptcmpfi  23778  ptcmplem1  24017  ptcmpg  24022  prdstmdd  24089  prdstgpd  24090  ismet2  24298  prdsxmetlem  24333  imasdsf1olem  24338  prdsms  24496  isngp2  24562  metdscn  24822  lmmbr  25225  causs  25265  ovolfioo  25434  ovolficc  25435  ovolfsf  25438  elovolm  25442  ovollb  25446  ovolunlem1a  25463  ovolunlem1  25464  ovolicc2lem1  25484  ovolicc2lem2  25485  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2  25489  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombl  25556  dyadmbl  25567  vitalilem3  25577  vitalilem4  25578  vitalilem5  25579  ismbf  25595  mbfid  25602  0plef  25639  i1f1  25657  i1faddlem  25660  i1fsub  25675  itg1sub  25676  mbfi1fseqlem4  25685  itg2le  25706  itg2mulclem  25713  itg2mulc  25714  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2i1fseq3  25724  itg2addlem  25725  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  dvfre  25918  dvnfre  25919  dvferm1  25952  dvferm2  25954  rolle  25957  dvgt0lem1  25969  dvivthlem1  25975  dvne0  25978  lhop1lem  25980  lhop2  25982  lhop  25983  dvcnvrelem1  25984  dvcnvre  25986  dvcvx  25987  dvfsumrlim  25998  tdeglem3  26024  elplyr  26166  taylthlem2  26339  taylth  26340  ulmcn  26364  iblulm  26372  efcvx  26414  dvrelog  26601  relogcn  26602  dvlog2  26617  leibpi  26906  efrlim  26933  jensenlem2  26951  jensen  26952  amgmlem  26953  amgm  26954  wilthlem2  27032  wilthlem3  27033  basellem7  27050  basellem9  27052  lgsfcl  27268  lgsdchr  27318  dchrvmasumlem1  27458  dchrisum0lem3  27482  axlowdimlem4  29014  axlowdimlem7  29017  axlowdimlem10  29020  upgruhgr  29171  konigsbergssiedgw  30320  pliguhgr  30557  0oo  30860  hhsscms  31349  nlelchi  32132  hmopidmchi  32222  pjinvari  32262  padct  32791  smatrcl  33940  lmlim  34091  rge0scvg  34093  lmdvg  34097  lmdvglim  34098  rrhre  34165  esumfsupre  34215  hashf2  34228  eulerpartlems  34504  eulerpartlemgs2  34524  coinfliprv  34627  fdvposlt  34743  fdvposle  34745  breprexpnat  34778  circlemethnat  34785  circlevma  34786  tgoldbachgtde  34804  lfuhgr  35300  subgrwlk  35314  ptpconn  35415  poimirlem8  37949  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  mblfinlem2  37979  mbfresfi  37987  itg2addnclem  37992  itg2addnclem2  37993  itg2addnc  37995  itg2gt0cn  37996  ftc1anclem8  38021  fdc  38066  heiborlem6  38137  heibor  38142  lfl0f  39515  intlewftc  42500  sticksstones3  42587  sticksstones9  42593  sticksstones11  42595  sticksstones17  42602  sticksstones18  42603  aks6d1c6lem5  42616  mzpexpmpt  43177  mzpresrename  43182  diophrw  43191  rabren3dioph  43243  lnrfg  43547  seff  44736  sblpnf  44737  binomcxplemnotnn0  44783  stoweidlem44  46472  stirlinglem8  46509  fourierdlem62  46596  fouriersw  46659  nnsum3primes4  48264  grtriclwlk3  48421  zlmodzxzldeplem1  48976  aacllem  50276  amgmwlem  50277