Theorem fss 6236

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 3768	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 605	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6072	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6072	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 287	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 396	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 384   ⊆ wss 3732  ran crn 5278   Fn wfn 6063  ⟶wf 6064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3739  df-ss 3746  df-f 6072

This theorem is referenced by:  fssd  6237  f1ss  6288  frnssb  6581  fsn2  6594  fsnex  6730  ofco  7115  ffoss  7325  issmo2  7650  smoiso  7663  mapsnd  8102  ssdomg  8206  alephfplem4  9181  cofsmo  9344  fin23lem17  9413  hsmexlem1  9501  axdc3lem4  9528  ac6s  9559  gruen  9887  intgru  9889  ingru  9890  hashf1lem1  13440  sswrd  13494  wrdv  13501  repsdf2  13802  limsupgre  14499  abscn2  14616  recn2  14618  imcn2  14619  climabs  14621  climre  14623  climim  14624  rlimabs  14626  rlimre  14628  rlimim  14629  caucvgrlem  14690  caurcvgr  14691  caucvgrlem2  14692  caurcvg  14694  fsumre  14826  fsumim  14827  0ram  16005  ramub1  16013  ramcl  16014  acsinfd  17448  acsdomd  17449  gsumval1  17545  resmhm2  17628  prdsgrpd  17794  prdsinvgd  17795  symgtrinv  18157  prdscmnd  18530  prdsabld  18531  pgpfaclem1  18747  prdsringd  18879  prdscrngd  18880  abvf  19092  prdslmodd  19241  psrridm  19678  coe1fval3  19851  zntoslem  20177  regsumsupp  20242  dsmmsubg  20363  dsmmlss  20364  islinds2  20428  lindsmm  20443  lsslindf  20445  1stccnp  21545  1stckgen  21637  prdstps  21712  pthaus  21721  txcmplem2  21725  ptcmpfi  21896  ptcmplem1  22135  ptcmpg  22140  prdstmdd  22206  prdstgpd  22207  ismet2  22417  prdsxmetlem  22452  imasdsf1olem  22457  prdsms  22615  isngp2  22680  metdscn  22938  lmmbr  23335  causs  23375  ovolfioo  23525  ovolficc  23526  ovolfsf  23529  elovolm  23533  ovollb  23537  ovolunlem1a  23554  ovolunlem1  23555  ovolicc2lem1  23575  ovolicc2lem2  23576  ovolicc2lem3  23577  ovolicc2lem4  23578  ovolicc2  23580  uniiccdif  23636  uniioovol  23637  uniiccvol  23638  uniioombllem2  23641  uniioombllem3a  23642  uniioombllem3  23643  uniioombllem4  23644  uniioombllem5  23645  uniioombl  23647  dyadmbl  23658  vitalilem3  23668  vitalilem4  23669  vitalilem5  23670  ismbf  23686  mbfid  23693  0plef  23730  i1f1  23748  i1faddlem  23751  i1fsub  23766  itg1sub  23767  mbfi1fseqlem4  23776  itg2le  23797  itg2mulclem  23804  itg2mulc  23805  itg2monolem1  23808  itg2monolem2  23809  itg2monolem3  23810  itg2mono  23811  itg2i1fseq3  23815  itg2addlem  23816  itg2gt0  23818  itg2cnlem1  23819  itg2cnlem2  23820  dvfre  24005  dvnfre  24006  dvferm1  24039  dvferm2  24041  rolle  24044  dvgt0lem1  24056  dvivthlem1  24062  dvne0  24065  lhop1lem  24067  lhop2  24069  lhop  24070  dvcnvrelem1  24071  dvcnvre  24073  dvcvx  24074  dvfsumrlim  24085  tdeglem3  24110  elplyr  24248  taylthlem2  24419  taylth  24420  ulmcn  24444  iblulm  24452  efcvx  24494  dvrelog  24674  relogcn  24675  dvlog2  24690  leibpi  24960  efrlim  24987  jensenlem2  25005  jensen  25006  amgmlem  25007  amgm  25008  wilthlem2  25086  wilthlem3  25087  basellem7  25104  basellem9  25106  lgsfcl  25321  lgsdchr  25371  dchrvmasumlem1  25475  dchrisum0lem3  25499  axlowdimlem4  26116  axlowdimlem7  26119  axlowdimlem10  26122  upgruhgr  26274  konigsbergssiedgw  27486  pliguhgr  27732  0oo  28035  hhsscms  28527  nlelchi  29311  hmopidmchi  29401  pjinvari  29441  padct  29881  smatrcl  30244  lmlim  30375  rge0scvg  30377  lmdvg  30381  lmdvglim  30382  rrhre  30447  esumfsupre  30515  hashf2  30528  eulerpartlems  30804  eulerpartlemgs2  30824  coinfliprv  30927  fdvposlt  31060  fdvposle  31062  breprexpnat  31095  circlemethnat  31102  circlevma  31103  tgoldbachgtde  31121  ptpconn  31595  fprb  32046  poimirlem8  33773  poimirlem18  33783  poimirlem21  33786  poimirlem22  33787  mblfinlem2  33803  mbfresfi  33811  itg2addnclem  33816  itg2addnclem2  33817  itg2addnc  33819  itg2gt0cn  33820  ftc1anclem8  33847  fdc  33895  heiborlem6  33969  heibor  33974  lfl0f  34957  mzpexpmpt  37918  mzpresrename  37923  diophrw  37932  rabren3dioph  37989  lnrfg  38298  seff  39114  sblpnf  39115  binomcxplemnotnn0  39161  stoweidlem44  40830  stirlinglem8  40867  fourierdlem62  40954  fouriersw  41017  nnsum3primes4  42284  resmgmhm2  42400  zlmodzxzldeplem1  42890  aacllem  43151  amgmwlem  43152