Theorem fss 6752

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3951  ran crn 5686   Fn wfn 6556  ⟶wf 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3968  df-f 6565

This theorem is referenced by:  fssd  6753  f1ss  6809  fcdmssb  7142  fsn2  7156  fprb  7214  ofco  7722  ffoss  7970  issmo2  8389  smoiso  8402  ssdomg  9040  alephfplem4  10147  cofsmo  10309  fin23lem17  10378  hsmexlem1  10466  axdc3lem4  10493  ac6s  10524  gruen  10852  intgru  10854  ingru  10855  hashf1lem1  14494  sswrd  14560  repsdf2  14816  limsupgre  15517  abscn2  15635  recn2  15637  imcn2  15638  climabs  15640  climre  15642  climim  15643  rlimabs  15645  rlimre  15647  rlimim  15648  caucvgrlem  15709  caurcvgr  15710  caucvgrlem2  15711  caurcvg  15713  fsumre  15844  fsumim  15845  0ram  17058  ramub1  17066  ramcl  17067  acsinfd  18601  acsdomd  18602  gsumval1  18696  resmgmhm2  18725  resmhm2  18834  prdsgrpd  19068  prdsinvgd  19069  symgtrinv  19490  prdscmnd  19879  prdsabld  19880  pgpfaclem1  20101  prdsrngd  20173  prdsmulrcl  20317  prdsringd  20318  prdscrngd  20319  abvf  20816  prdslmodd  20967  zntoslem  21575  regsumsupp  21640  dsmmsubg  21763  dsmmlss  21764  islinds2  21833  lindsmm  21848  lsslindf  21850  psrridm  21983  coe1fval3  22210  1stccnp  23470  1stckgen  23562  prdstps  23637  pthaus  23646  txcmplem2  23650  ptcmpfi  23821  ptcmplem1  24060  ptcmpg  24065  prdstmdd  24132  prdstgpd  24133  ismet2  24343  prdsxmetlem  24378  imasdsf1olem  24383  prdsms  24544  isngp2  24610  metdscn  24878  lmmbr  25292  causs  25332  ovolfioo  25502  ovolficc  25503  ovolfsf  25506  elovolm  25510  ovollb  25514  ovolunlem1a  25531  ovolunlem1  25532  ovolicc2lem1  25552  ovolicc2lem2  25553  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2  25557  uniiccdif  25613  uniioovol  25614  uniiccvol  25615  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  uniioombl  25624  dyadmbl  25635  vitalilem3  25645  vitalilem4  25646  vitalilem5  25647  ismbf  25663  mbfid  25670  0plef  25707  i1f1  25725  i1faddlem  25728  i1fsub  25743  itg1sub  25744  mbfi1fseqlem4  25753  itg2le  25774  itg2mulclem  25781  itg2mulc  25782  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2i1fseq3  25792  itg2addlem  25793  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  dvfre  25989  dvnfre  25990  dvferm1  26023  dvferm2  26025  rolle  26028  dvgt0lem1  26041  dvivthlem1  26047  dvne0  26050  lhop1lem  26052  lhop2  26054  lhop  26055  dvcnvrelem1  26056  dvcnvre  26058  dvcvx  26059  dvfsumrlim  26072  tdeglem3  26098  elplyr  26240  taylthlem2  26416  taylthlem2OLD  26417  taylth  26418  ulmcn  26442  iblulm  26450  efcvx  26493  dvrelog  26679  relogcn  26680  dvlog2  26695  leibpi  26985  efrlim  27012  efrlimOLD  27013  jensenlem2  27031  jensen  27032  amgmlem  27033  amgm  27034  wilthlem2  27112  wilthlem3  27113  basellem7  27130  basellem9  27132  lgsfcl  27349  lgsdchr  27399  dchrvmasumlem1  27539  dchrisum0lem3  27563  axlowdimlem4  28960  axlowdimlem7  28963  axlowdimlem10  28966  upgruhgr  29119  konigsbergssiedgw  30269  pliguhgr  30505  0oo  30808  hhsscms  31297  nlelchi  32080  hmopidmchi  32170  pjinvari  32210  padct  32731  smatrcl  33795  lmlim  33946  rge0scvg  33948  lmdvg  33952  lmdvglim  33953  rrhre  34022  esumfsupre  34072  hashf2  34085  eulerpartlems  34362  eulerpartlemgs2  34382  coinfliprv  34485  fdvposlt  34614  fdvposle  34616  breprexpnat  34649  circlemethnat  34656  circlevma  34657  tgoldbachgtde  34675  lfuhgr  35123  subgrwlk  35137  ptpconn  35238  poimirlem8  37635  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  mblfinlem2  37665  mbfresfi  37673  itg2addnclem  37678  itg2addnclem2  37679  itg2addnc  37681  itg2gt0cn  37682  ftc1anclem8  37707  fdc  37752  heiborlem6  37823  heibor  37828  lfl0f  39070  intlewftc  42062  sticksstones3  42149  sticksstones9  42155  sticksstones11  42157  sticksstones17  42164  sticksstones18  42165  aks6d1c6lem5  42178  mzpexpmpt  42756  mzpresrename  42761  diophrw  42770  rabren3dioph  42826  lnrfg  43131  seff  44328  sblpnf  44329  binomcxplemnotnn0  44375  stoweidlem44  46059  stirlinglem8  46096  fourierdlem62  46183  fouriersw  46246  nnsum3primes4  47775  grtriclwlk3  47912  zlmodzxzldeplem1  48417  aacllem  49320  amgmwlem  49321