Theorem fss 6726

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3895  ran crn 5651   Fn wfn 6533  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3896  df-f 6542

This theorem is used by:  fssd  6727  f1ss  6785  fcdmssb  7122  fsn2  7137  fprb  7199  ofco  7718  ffoss  7958  issmo2  8360  smoiso  8373  ssdomg  9030  alephfplem4  10189  cofsmo  10350  fin23lem17  10419  hsmexlem1  10507  axdc3lem4  10534  ac6s  10565  gruen  10900  intgru  10902  ingru  10903  hashf1lem1  14603  sswrd  14670  repsdf2  14933  limsupgre  15653  abscn2  15771  recn2  15773  imcn2  15774  climabs  15776  climre  15778  climim  15779  rlimabs  15781  rlimre  15783  rlimim  15784  caucvgrlem  15845  caurcvgr  15846  caucvgrlem2  15847  caurcvg  15849  fsumre  15980  fsumim  15981  0ram  17203  ramub1  17211  ramcl  17212  acsinfd  18735  acsdomd  18736  gsumval1  18877  resmgmhm2  18906  resmhm2  19022  prdsgrpd  19265  prdsinvgd  19266  symgtrinv  19691  prdscmnd  20080  prdsabld  20081  pgpfaclem1  20302  prdsrngd  20403  prdsmulrcl  20554  prdsringd  20555  prdscrngd  20556  abvf  21077  prdslmodd  21249  zntoslem  21867  regsumsupp  21933  dsmmsubg  22054  dsmmlss  22055  islinds2  22124  lindsmm  22139  lsslindf  22141  psrridm  22275  coe1fval3  22531  1stccnp  23786  1stckgen  23878  prdstps  23953  pthaus  23962  txcmplem2  23966  ptcmpfi  24137  ptcmplem1  24376  ptcmpg  24381  prdstmdd  24448  prdstgpd  24449  ismet2  24657  prdsxmetlem  24692  imasdsf1olem  24697  prdsms  24855  isngp2  24921  metdscn  25181  lmmbr  25584  causs  25624  ovolfioo  25793  ovolficc  25794  ovolfsf  25797  elovolm  25801  ovollb  25805  ovolunlem1a  25822  ovolunlem1  25823  ovolicc2lem1  25843  ovolicc2lem2  25844  ovolicc2lem3  25845  ovolicc2lem4  25846  ovolicc2  25848  uniiccdif  25904  uniioovol  25905  uniiccvol  25906  uniioombllem2  25909  uniioombllem3a  25910  uniioombllem3  25911  uniioombllem4  25912  uniioombllem5  25913  uniioombl  25915  dyadmbl  25926  vitalilem3  25936  vitalilem4  25937  vitalilem5  25938  ismbf  25954  mbfid  25961  0plef  25998  i1f1  26016  i1faddlem  26019  i1fsub  26034  itg1sub  26035  mbfi1fseqlem4  26044  itg2le  26065  itg2mulclem  26072  itg2mulc  26073  itg2monolem1  26076  itg2monolem2  26077  itg2monolem3  26078  itg2mono  26079  itg2i1fseq3  26083  itg2addlem  26084  itg2gt0  26086  itg2cnlem1  26087  itg2cnlem2  26088  dvfre  26276  dvnfre  26277  dvferm1  26310  dvferm2  26312  rolle  26315  dvgt0lem1  26327  dvivthlem1  26333  dvne0  26336  lhop1lem  26338  lhop2  26340  lhop  26341  dvcnvrelem1  26342  dvcnvre  26344  dvcvx  26345  dvfsumrlim  26356  tdeglem3  26382  elplyr  26524  taylthlem2  26706  taylth  26707  ulmcn  26731  iblulm  26739  efcvx  26781  dvrelog  26970  relogcn  26971  dvlog2  26986  leibpi  27275  efrlim  27302  jensenlem2  27320  jensen  27321  amgmlem  27322  amgm  27323  wilthlem2  27401  wilthlem3  27402  basellem7  27419  basellem9  27421  lgsfcl  27637  lgsdchr  27687  dchrvmasumlem1  27827  dchrisum0lem3  27851  axlowdimlem4  29528  axlowdimlem7  29531  axlowdimlem10  29534  upgruhgr  29685  lfuhgr  29731  subgrwlk  30274  konigsbergssiedgw  30856  pliguhgr  31093  0oo  31396  hhsscms  31885  nlelchi  32668  hmopidmchi  32758  pjinvari  32798  padct  33357  smatrcl  34474  lmlim  34625  rge0scvg  34627  lmdvg  34631  lmdvglim  34632  rrhre  34699  esumfsupre  34749  hashf2  34762  eulerpartlems  35038  eulerpartlemgs2  35058  coinfliprv  35161  fdvposlt  35274  fdvposle  35276  breprexpnat  35309  circlemethnat  35316  circlevma  35317  tgoldbachgtde  35335  ptpconn  36084  poimirlem8  38639  poimirlem18  38649  poimirlem21  38652  poimirlem22  38653  mblfinlem2  38669  mbfresfi  38677  itg2addnclem  38682  itg2addnclem2  38683  itg2addnc  38685  itg2gt0cn  38686  ftc1anclem8  38711  fdc  38772  heiborlem6  38843  heibor  38848  lfl0f  40219  intlewftc  43204  sticksstones3  43291  sticksstones9  43297  sticksstones11  43299  sticksstones17  43306  sticksstones18  43307  aks6d1c6lem5  43320  mzpexpmpt  43849  mzpresrename  43854  diophrw  43863  rabren3dioph  43915  lnrfg  44214  seff  45386  sblpnf  45387  binomcxplemnotnn0  45433  stoweidlem44  47147  stirlinglem8  47184  fourierdlem62  47271  fouriersw  47334  nnsum3primes4  48979  grtriclwlk3  49136  zlmodzxzldeplem1  49705  aacllem  51107  amgmwlem  51155