Theorem fss 6647

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

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3892  ran crn 5601   Fn wfn 6453  ⟶wf 6454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909  df-f 6462

This theorem is referenced by:  fssd  6648  f1ss  6706  fcdmssb  7027  fsn2  7040  fprb  7101  ofco  7588  ffoss  7820  issmo2  8211  smoiso  8224  ssdomg  8821  alephfplem4  9909  cofsmo  10071  fin23lem17  10140  hsmexlem1  10228  axdc3lem4  10255  ac6s  10286  gruen  10614  intgru  10616  ingru  10617  hashf1lem1  14213  hashf1lem1OLD  14214  sswrd  14270  repsdf2  14536  limsupgre  15235  abscn2  15353  recn2  15355  imcn2  15356  climabs  15358  climre  15360  climim  15361  rlimabs  15363  rlimre  15365  rlimim  15366  caucvgrlem  15429  caurcvgr  15430  caucvgrlem2  15431  caurcvg  15433  fsumre  15565  fsumim  15566  0ram  16766  ramub1  16774  ramcl  16775  acsinfd  18319  acsdomd  18320  gsumval1  18412  resmhm2  18505  prdsgrpd  18730  prdsinvgd  18731  symgtrinv  19125  prdscmnd  19507  prdsabld  19508  pgpfaclem1  19729  prdsringd  19896  prdscrngd  19897  abvf  20128  prdslmodd  20276  zntoslem  20809  regsumsupp  20872  dsmmsubg  20995  dsmmlss  20996  islinds2  21065  lindsmm  21080  lsslindf  21082  psrridm  21218  coe1fval3  21424  1stccnp  22658  1stckgen  22750  prdstps  22825  pthaus  22834  txcmplem2  22838  ptcmpfi  23009  ptcmplem1  23248  ptcmpg  23253  prdstmdd  23320  prdstgpd  23321  ismet2  23531  prdsxmetlem  23566  imasdsf1olem  23571  prdsms  23732  isngp2  23798  metdscn  24064  lmmbr  24467  causs  24507  ovolfioo  24676  ovolficc  24677  ovolfsf  24680  elovolm  24684  ovollb  24688  ovolunlem1a  24705  ovolunlem1  24706  ovolicc2lem1  24726  ovolicc2lem2  24727  ovolicc2lem3  24728  ovolicc2lem4  24729  ovolicc2  24731  uniiccdif  24787  uniioovol  24788  uniiccvol  24789  uniioombllem2  24792  uniioombllem3a  24793  uniioombllem3  24794  uniioombllem4  24795  uniioombllem5  24796  uniioombl  24798  dyadmbl  24809  vitalilem3  24819  vitalilem4  24820  vitalilem5  24821  ismbf  24837  mbfid  24844  0plef  24881  i1f1  24899  i1faddlem  24902  i1fsub  24918  itg1sub  24919  mbfi1fseqlem4  24928  itg2le  24949  itg2mulclem  24956  itg2mulc  24957  itg2monolem1  24960  itg2monolem2  24961  itg2monolem3  24962  itg2mono  24963  itg2i1fseq3  24967  itg2addlem  24968  itg2gt0  24970  itg2cnlem1  24971  itg2cnlem2  24972  dvfre  25160  dvnfre  25161  dvferm1  25194  dvferm2  25196  rolle  25199  dvgt0lem1  25211  dvivthlem1  25217  dvne0  25220  lhop1lem  25222  lhop2  25224  lhop  25225  dvcnvrelem1  25226  dvcnvre  25228  dvcvx  25229  dvfsumrlim  25240  tdeglem3  25267  tdeglem3OLD  25268  elplyr  25407  taylthlem2  25578  taylth  25579  ulmcn  25603  iblulm  25611  efcvx  25653  dvrelog  25837  relogcn  25838  dvlog2  25853  leibpi  26137  efrlim  26164  jensenlem2  26182  jensen  26183  amgmlem  26184  amgm  26185  wilthlem2  26263  wilthlem3  26264  basellem7  26281  basellem9  26283  lgsfcl  26498  lgsdchr  26548  dchrvmasumlem1  26688  dchrisum0lem3  26712  axlowdimlem4  27358  axlowdimlem7  27361  axlowdimlem10  27364  upgruhgr  27517  konigsbergssiedgw  28659  pliguhgr  28893  0oo  29196  hhsscms  29685  nlelchi  30468  hmopidmchi  30558  pjinvari  30598  padct  31099  smatrcl  31791  lmlim  31942  rge0scvg  31944  lmdvg  31948  lmdvglim  31949  rrhre  32016  esumfsupre  32084  hashf2  32097  eulerpartlems  32372  eulerpartlemgs2  32392  coinfliprv  32494  fdvposlt  32624  fdvposle  32626  breprexpnat  32659  circlemethnat  32666  circlevma  32667  tgoldbachgtde  32685  lfuhgr  33124  subgrwlk  33139  ptpconn  33240  poimirlem8  35829  poimirlem18  35839  poimirlem21  35842  poimirlem22  35843  mblfinlem2  35859  mbfresfi  35867  itg2addnclem  35872  itg2addnclem2  35873  itg2addnc  35875  itg2gt0cn  35876  ftc1anclem8  35901  fdc  35947  heiborlem6  36018  heibor  36023  lfl0f  37125  intlewftc  40111  sticksstones3  40146  sticksstones9  40152  sticksstones11  40154  sticksstones17  40161  sticksstones18  40162  mzpexpmpt  40604  mzpresrename  40609  diophrw  40618  rabren3dioph  40674  lnrfg  40982  seff  41965  sblpnf  41966  binomcxplemnotnn0  42012  stoweidlem44  43634  stirlinglem8  43671  fourierdlem62  43758  fouriersw  43821  nnsum3primes4  45298  resmgmhm2  45411  zlmodzxzldeplem1  45899  aacllem  46563  amgmwlem  46564