Theorem fss 6678

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488

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 3918  df-f 6496

This theorem is referenced by:  fssd  6679  f1ss  6735  fcdmssb  7067  fsn2  7081  fprb  7140  ofco  7647  ffoss  7890  issmo2  8281  smoiso  8294  ssdomg  8937  alephfplem4  10017  cofsmo  10179  fin23lem17  10248  hsmexlem1  10336  axdc3lem4  10363  ac6s  10394  gruen  10723  intgru  10725  ingru  10726  hashf1lem1  14378  sswrd  14445  repsdf2  14701  limsupgre  15404  abscn2  15522  recn2  15524  imcn2  15525  climabs  15527  climre  15529  climim  15530  rlimabs  15532  rlimre  15534  rlimim  15535  caucvgrlem  15596  caurcvgr  15597  caucvgrlem2  15598  caurcvg  15600  fsumre  15731  fsumim  15732  0ram  16948  ramub1  16956  ramcl  16957  acsinfd  18479  acsdomd  18480  gsumval1  18608  resmgmhm2  18637  resmhm2  18746  prdsgrpd  18980  prdsinvgd  18981  symgtrinv  19401  prdscmnd  19790  prdsabld  19791  pgpfaclem1  20012  prdsrngd  20111  prdsmulrcl  20255  prdsringd  20256  prdscrngd  20257  abvf  20748  prdslmodd  20920  zntoslem  21511  regsumsupp  21577  dsmmsubg  21698  dsmmlss  21699  islinds2  21768  lindsmm  21783  lsslindf  21785  psrridm  21918  coe1fval3  22149  1stccnp  23406  1stckgen  23498  prdstps  23573  pthaus  23582  txcmplem2  23586  ptcmpfi  23757  ptcmplem1  23996  ptcmpg  24001  prdstmdd  24068  prdstgpd  24069  ismet2  24277  prdsxmetlem  24312  imasdsf1olem  24317  prdsms  24475  isngp2  24541  metdscn  24801  lmmbr  25214  causs  25254  ovolfioo  25424  ovolficc  25425  ovolfsf  25428  elovolm  25432  ovollb  25436  ovolunlem1a  25453  ovolunlem1  25454  ovolicc2lem1  25474  ovolicc2lem2  25475  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2  25479  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  uniioombl  25546  dyadmbl  25557  vitalilem3  25567  vitalilem4  25568  vitalilem5  25569  ismbf  25585  mbfid  25592  0plef  25629  i1f1  25647  i1faddlem  25650  i1fsub  25665  itg1sub  25666  mbfi1fseqlem4  25675  itg2le  25696  itg2mulclem  25703  itg2mulc  25704  itg2monolem1  25707  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  itg2i1fseq3  25714  itg2addlem  25715  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  dvfre  25911  dvnfre  25912  dvferm1  25945  dvferm2  25947  rolle  25950  dvgt0lem1  25963  dvivthlem1  25969  dvne0  25972  lhop1lem  25974  lhop2  25976  lhop  25977  dvcnvrelem1  25978  dvcnvre  25980  dvcvx  25981  dvfsumrlim  25994  tdeglem3  26020  elplyr  26162  taylthlem2  26338  taylthlem2OLD  26339  taylth  26340  ulmcn  26364  iblulm  26372  efcvx  26415  dvrelog  26602  relogcn  26603  dvlog2  26618  leibpi  26908  efrlim  26935  efrlimOLD  26936  jensenlem2  26954  jensen  26955  amgmlem  26956  amgm  26957  wilthlem2  27035  wilthlem3  27036  basellem7  27053  basellem9  27055  lgsfcl  27272  lgsdchr  27322  dchrvmasumlem1  27462  dchrisum0lem3  27486  axlowdimlem4  29018  axlowdimlem7  29021  axlowdimlem10  29024  upgruhgr  29175  konigsbergssiedgw  30325  pliguhgr  30561  0oo  30864  hhsscms  31353  nlelchi  32136  hmopidmchi  32226  pjinvari  32266  padct  32797  smatrcl  33953  lmlim  34104  rge0scvg  34106  lmdvg  34110  lmdvglim  34111  rrhre  34178  esumfsupre  34228  hashf2  34241  eulerpartlems  34517  eulerpartlemgs2  34537  coinfliprv  34640  fdvposlt  34756  fdvposle  34758  breprexpnat  34791  circlemethnat  34798  circlevma  34799  tgoldbachgtde  34817  lfuhgr  35312  subgrwlk  35326  ptpconn  35427  poimirlem8  37825  poimirlem18  37835  poimirlem21  37838  poimirlem22  37839  mblfinlem2  37855  mbfresfi  37863  itg2addnclem  37868  itg2addnclem2  37869  itg2addnc  37871  itg2gt0cn  37872  ftc1anclem8  37897  fdc  37942  heiborlem6  38013  heibor  38018  lfl0f  39325  intlewftc  42311  sticksstones3  42398  sticksstones9  42404  sticksstones11  42406  sticksstones17  42413  sticksstones18  42414  aks6d1c6lem5  42427  mzpexpmpt  42983  mzpresrename  42988  diophrw  42997  rabren3dioph  43053  lnrfg  43357  seff  44546  sblpnf  44547  binomcxplemnotnn0  44593  stoweidlem44  46284  stirlinglem8  46321  fourierdlem62  46408  fouriersw  46471  nnsum3primes4  48030  grtriclwlk3  48187  zlmodzxzldeplem1  48742  aacllem  50042  amgmwlem  50043