Theorem fss 6704

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507

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 3931  df-f 6515

This theorem is referenced by:  fssd  6705  f1ss  6761  fcdmssb  7094  fsn2  7108  fprb  7168  ofco  7678  ffoss  7924  issmo2  8318  smoiso  8331  ssdomg  8971  alephfplem4  10060  cofsmo  10222  fin23lem17  10291  hsmexlem1  10379  axdc3lem4  10406  ac6s  10437  gruen  10765  intgru  10767  ingru  10768  hashf1lem1  14420  sswrd  14487  repsdf2  14743  limsupgre  15447  abscn2  15565  recn2  15567  imcn2  15568  climabs  15570  climre  15572  climim  15573  rlimabs  15575  rlimre  15577  rlimim  15578  caucvgrlem  15639  caurcvgr  15640  caucvgrlem2  15641  caurcvg  15643  fsumre  15774  fsumim  15775  0ram  16991  ramub1  16999  ramcl  17000  acsinfd  18515  acsdomd  18516  gsumval1  18610  resmgmhm2  18639  resmhm2  18748  prdsgrpd  18982  prdsinvgd  18983  symgtrinv  19402  prdscmnd  19791  prdsabld  19792  pgpfaclem1  20013  prdsrngd  20085  prdsmulrcl  20229  prdsringd  20230  prdscrngd  20231  abvf  20724  prdslmodd  20875  zntoslem  21466  regsumsupp  21531  dsmmsubg  21652  dsmmlss  21653  islinds2  21722  lindsmm  21737  lsslindf  21739  psrridm  21872  coe1fval3  22093  1stccnp  23349  1stckgen  23441  prdstps  23516  pthaus  23525  txcmplem2  23529  ptcmpfi  23700  ptcmplem1  23939  ptcmpg  23944  prdstmdd  24011  prdstgpd  24012  ismet2  24221  prdsxmetlem  24256  imasdsf1olem  24261  prdsms  24419  isngp2  24485  metdscn  24745  lmmbr  25158  causs  25198  ovolfioo  25368  ovolficc  25369  ovolfsf  25372  elovolm  25376  ovollb  25380  ovolunlem1a  25397  ovolunlem1  25398  ovolicc2lem1  25418  ovolicc2lem2  25419  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2  25423  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  uniioombl  25490  dyadmbl  25501  vitalilem3  25511  vitalilem4  25512  vitalilem5  25513  ismbf  25529  mbfid  25536  0plef  25573  i1f1  25591  i1faddlem  25594  i1fsub  25609  itg1sub  25610  mbfi1fseqlem4  25619  itg2le  25640  itg2mulclem  25647  itg2mulc  25648  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2i1fseq3  25658  itg2addlem  25659  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  dvfre  25855  dvnfre  25856  dvferm1  25889  dvferm2  25891  rolle  25894  dvgt0lem1  25907  dvivthlem1  25913  dvne0  25916  lhop1lem  25918  lhop2  25920  lhop  25921  dvcnvrelem1  25922  dvcnvre  25924  dvcvx  25925  dvfsumrlim  25938  tdeglem3  25964  elplyr  26106  taylthlem2  26282  taylthlem2OLD  26283  taylth  26284  ulmcn  26308  iblulm  26316  efcvx  26359  dvrelog  26546  relogcn  26547  dvlog2  26562  leibpi  26852  efrlim  26879  efrlimOLD  26880  jensenlem2  26898  jensen  26899  amgmlem  26900  amgm  26901  wilthlem2  26979  wilthlem3  26980  basellem7  26997  basellem9  26999  lgsfcl  27216  lgsdchr  27266  dchrvmasumlem1  27406  dchrisum0lem3  27430  axlowdimlem4  28872  axlowdimlem7  28875  axlowdimlem10  28878  upgruhgr  29029  konigsbergssiedgw  30179  pliguhgr  30415  0oo  30718  hhsscms  31207  nlelchi  31990  hmopidmchi  32080  pjinvari  32120  padct  32643  smatrcl  33786  lmlim  33937  rge0scvg  33939  lmdvg  33943  lmdvglim  33944  rrhre  34011  esumfsupre  34061  hashf2  34074  eulerpartlems  34351  eulerpartlemgs2  34371  coinfliprv  34474  fdvposlt  34590  fdvposle  34592  breprexpnat  34625  circlemethnat  34632  circlevma  34633  tgoldbachgtde  34651  lfuhgr  35105  subgrwlk  35119  ptpconn  35220  poimirlem8  37622  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  mblfinlem2  37652  mbfresfi  37660  itg2addnclem  37665  itg2addnclem2  37666  itg2addnc  37668  itg2gt0cn  37669  ftc1anclem8  37694  fdc  37739  heiborlem6  37810  heibor  37815  lfl0f  39062  intlewftc  42049  sticksstones3  42136  sticksstones9  42142  sticksstones11  42144  sticksstones17  42151  sticksstones18  42152  aks6d1c6lem5  42165  mzpexpmpt  42733  mzpresrename  42738  diophrw  42747  rabren3dioph  42803  lnrfg  43108  seff  44298  sblpnf  44299  binomcxplemnotnn0  44345  stoweidlem44  46042  stirlinglem8  46079  fourierdlem62  46166  fouriersw  46229  nnsum3primes4  47789  grtriclwlk3  47944  zlmodzxzldeplem1  48489  aacllem  49790  amgmwlem  49791