Theorem fss 6667

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3902  ran crn 5617   Fn wfn 6476  ⟶wf 6477

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 3919  df-f 6485

This theorem is referenced by:  fssd  6668  f1ss  6724  fcdmssb  7055  fsn2  7069  fprb  7128  ofco  7635  ffoss  7878  issmo2  8269  smoiso  8282  ssdomg  8922  alephfplem4  9995  cofsmo  10157  fin23lem17  10226  hsmexlem1  10314  axdc3lem4  10341  ac6s  10372  gruen  10700  intgru  10702  ingru  10703  hashf1lem1  14359  sswrd  14426  repsdf2  14682  limsupgre  15385  abscn2  15503  recn2  15505  imcn2  15506  climabs  15508  climre  15510  climim  15511  rlimabs  15513  rlimre  15515  rlimim  15516  caucvgrlem  15577  caurcvgr  15578  caucvgrlem2  15579  caurcvg  15581  fsumre  15712  fsumim  15713  0ram  16929  ramub1  16937  ramcl  16938  acsinfd  18459  acsdomd  18460  gsumval1  18588  resmgmhm2  18617  resmhm2  18726  prdsgrpd  18960  prdsinvgd  18961  symgtrinv  19382  prdscmnd  19771  prdsabld  19772  pgpfaclem1  19993  prdsrngd  20092  prdsmulrcl  20236  prdsringd  20237  prdscrngd  20238  abvf  20728  prdslmodd  20900  zntoslem  21491  regsumsupp  21557  dsmmsubg  21678  dsmmlss  21679  islinds2  21748  lindsmm  21763  lsslindf  21765  psrridm  21898  coe1fval3  22119  1stccnp  23375  1stckgen  23467  prdstps  23542  pthaus  23551  txcmplem2  23555  ptcmpfi  23726  ptcmplem1  23965  ptcmpg  23970  prdstmdd  24037  prdstgpd  24038  ismet2  24246  prdsxmetlem  24281  imasdsf1olem  24286  prdsms  24444  isngp2  24510  metdscn  24770  lmmbr  25183  causs  25223  ovolfioo  25393  ovolficc  25394  ovolfsf  25397  elovolm  25401  ovollb  25405  ovolunlem1a  25422  ovolunlem1  25423  ovolicc2lem1  25443  ovolicc2lem2  25444  ovolicc2lem3  25445  ovolicc2lem4  25446  ovolicc2  25448  uniiccdif  25504  uniioovol  25505  uniiccvol  25506  uniioombllem2  25509  uniioombllem3a  25510  uniioombllem3  25511  uniioombllem4  25512  uniioombllem5  25513  uniioombl  25515  dyadmbl  25526  vitalilem3  25536  vitalilem4  25537  vitalilem5  25538  ismbf  25554  mbfid  25561  0plef  25598  i1f1  25616  i1faddlem  25619  i1fsub  25634  itg1sub  25635  mbfi1fseqlem4  25644  itg2le  25665  itg2mulclem  25672  itg2mulc  25673  itg2monolem1  25676  itg2monolem2  25677  itg2monolem3  25678  itg2mono  25679  itg2i1fseq3  25683  itg2addlem  25684  itg2gt0  25686  itg2cnlem1  25687  itg2cnlem2  25688  dvfre  25880  dvnfre  25881  dvferm1  25914  dvferm2  25916  rolle  25919  dvgt0lem1  25932  dvivthlem1  25938  dvne0  25941  lhop1lem  25943  lhop2  25945  lhop  25946  dvcnvrelem1  25947  dvcnvre  25949  dvcvx  25950  dvfsumrlim  25963  tdeglem3  25989  elplyr  26131  taylthlem2  26307  taylthlem2OLD  26308  taylth  26309  ulmcn  26333  iblulm  26341  efcvx  26384  dvrelog  26571  relogcn  26572  dvlog2  26587  leibpi  26877  efrlim  26904  efrlimOLD  26905  jensenlem2  26923  jensen  26924  amgmlem  26925  amgm  26926  wilthlem2  27004  wilthlem3  27005  basellem7  27022  basellem9  27024  lgsfcl  27241  lgsdchr  27291  dchrvmasumlem1  27431  dchrisum0lem3  27455  axlowdimlem4  28921  axlowdimlem7  28924  axlowdimlem10  28927  upgruhgr  29078  konigsbergssiedgw  30225  pliguhgr  30461  0oo  30764  hhsscms  31253  nlelchi  32036  hmopidmchi  32126  pjinvari  32166  padct  32696  smatrcl  33804  lmlim  33955  rge0scvg  33957  lmdvg  33961  lmdvglim  33962  rrhre  34029  esumfsupre  34079  hashf2  34092  eulerpartlems  34368  eulerpartlemgs2  34388  coinfliprv  34491  fdvposlt  34607  fdvposle  34609  breprexpnat  34642  circlemethnat  34649  circlevma  34650  tgoldbachgtde  34668  lfuhgr  35150  subgrwlk  35164  ptpconn  35265  poimirlem8  37667  poimirlem18  37677  poimirlem21  37680  poimirlem22  37681  mblfinlem2  37697  mbfresfi  37705  itg2addnclem  37710  itg2addnclem2  37711  itg2addnc  37713  itg2gt0cn  37714  ftc1anclem8  37739  fdc  37784  heiborlem6  37855  heibor  37860  lfl0f  39107  intlewftc  42093  sticksstones3  42180  sticksstones9  42186  sticksstones11  42188  sticksstones17  42195  sticksstones18  42196  aks6d1c6lem5  42209  mzpexpmpt  42777  mzpresrename  42782  diophrw  42791  rabren3dioph  42847  lnrfg  43151  seff  44341  sblpnf  44342  binomcxplemnotnn0  44388  stoweidlem44  46081  stirlinglem8  46118  fourierdlem62  46205  fouriersw  46268  nnsum3primes4  47818  grtriclwlk3  47975  zlmodzxzldeplem1  48531  aacllem  49832  amgmwlem  49833