Theorem fss 6673

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3897  ran crn 5620   Fn wfn 6482  ⟶wf 6483

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 3914  df-f 6491

This theorem is referenced by:  fssd  6674  f1ss  6730  fcdmssb  7061  fsn2  7075  fprb  7134  ofco  7641  ffoss  7884  issmo2  8275  smoiso  8288  ssdomg  8928  alephfplem4  10004  cofsmo  10166  fin23lem17  10235  hsmexlem1  10323  axdc3lem4  10350  ac6s  10381  gruen  10709  intgru  10711  ingru  10712  hashf1lem1  14368  sswrd  14435  repsdf2  14691  limsupgre  15394  abscn2  15512  recn2  15514  imcn2  15515  climabs  15517  climre  15519  climim  15520  rlimabs  15522  rlimre  15524  rlimim  15525  caucvgrlem  15586  caurcvgr  15587  caucvgrlem2  15588  caurcvg  15590  fsumre  15721  fsumim  15722  0ram  16938  ramub1  16946  ramcl  16947  acsinfd  18468  acsdomd  18469  gsumval1  18597  resmgmhm2  18626  resmhm2  18735  prdsgrpd  18969  prdsinvgd  18970  symgtrinv  19390  prdscmnd  19779  prdsabld  19780  pgpfaclem1  20001  prdsrngd  20100  prdsmulrcl  20244  prdsringd  20245  prdscrngd  20246  abvf  20736  prdslmodd  20908  zntoslem  21499  regsumsupp  21565  dsmmsubg  21686  dsmmlss  21687  islinds2  21756  lindsmm  21771  lsslindf  21773  psrridm  21906  coe1fval3  22127  1stccnp  23383  1stckgen  23475  prdstps  23550  pthaus  23559  txcmplem2  23563  ptcmpfi  23734  ptcmplem1  23973  ptcmpg  23978  prdstmdd  24045  prdstgpd  24046  ismet2  24254  prdsxmetlem  24289  imasdsf1olem  24294  prdsms  24452  isngp2  24518  metdscn  24778  lmmbr  25191  causs  25231  ovolfioo  25401  ovolficc  25402  ovolfsf  25405  elovolm  25409  ovollb  25413  ovolunlem1a  25430  ovolunlem1  25431  ovolicc2lem1  25451  ovolicc2lem2  25452  ovolicc2lem3  25453  ovolicc2lem4  25454  ovolicc2  25456  uniiccdif  25512  uniioovol  25513  uniiccvol  25514  uniioombllem2  25517  uniioombllem3a  25518  uniioombllem3  25519  uniioombllem4  25520  uniioombllem5  25521  uniioombl  25523  dyadmbl  25534  vitalilem3  25544  vitalilem4  25545  vitalilem5  25546  ismbf  25562  mbfid  25569  0plef  25606  i1f1  25624  i1faddlem  25627  i1fsub  25642  itg1sub  25643  mbfi1fseqlem4  25652  itg2le  25673  itg2mulclem  25680  itg2mulc  25681  itg2monolem1  25684  itg2monolem2  25685  itg2monolem3  25686  itg2mono  25687  itg2i1fseq3  25691  itg2addlem  25692  itg2gt0  25694  itg2cnlem1  25695  itg2cnlem2  25696  dvfre  25888  dvnfre  25889  dvferm1  25922  dvferm2  25924  rolle  25927  dvgt0lem1  25940  dvivthlem1  25946  dvne0  25949  lhop1lem  25951  lhop2  25953  lhop  25954  dvcnvrelem1  25955  dvcnvre  25957  dvcvx  25958  dvfsumrlim  25971  tdeglem3  25997  elplyr  26139  taylthlem2  26315  taylthlem2OLD  26316  taylth  26317  ulmcn  26341  iblulm  26349  efcvx  26392  dvrelog  26579  relogcn  26580  dvlog2  26595  leibpi  26885  efrlim  26912  efrlimOLD  26913  jensenlem2  26931  jensen  26932  amgmlem  26933  amgm  26934  wilthlem2  27012  wilthlem3  27013  basellem7  27030  basellem9  27032  lgsfcl  27249  lgsdchr  27299  dchrvmasumlem1  27439  dchrisum0lem3  27463  axlowdimlem4  28930  axlowdimlem7  28933  axlowdimlem10  28936  upgruhgr  29087  konigsbergssiedgw  30237  pliguhgr  30473  0oo  30776  hhsscms  31265  nlelchi  32048  hmopidmchi  32138  pjinvari  32178  padct  32708  smatrcl  33816  lmlim  33967  rge0scvg  33969  lmdvg  33973  lmdvglim  33974  rrhre  34041  esumfsupre  34091  hashf2  34104  eulerpartlems  34380  eulerpartlemgs2  34400  coinfliprv  34503  fdvposlt  34619  fdvposle  34621  breprexpnat  34654  circlemethnat  34661  circlevma  34662  tgoldbachgtde  34680  lfuhgr  35169  subgrwlk  35183  ptpconn  35284  poimirlem8  37674  poimirlem18  37684  poimirlem21  37687  poimirlem22  37688  mblfinlem2  37704  mbfresfi  37712  itg2addnclem  37717  itg2addnclem2  37718  itg2addnc  37720  itg2gt0cn  37721  ftc1anclem8  37746  fdc  37791  heiborlem6  37862  heibor  37867  lfl0f  39174  intlewftc  42160  sticksstones3  42247  sticksstones9  42253  sticksstones11  42255  sticksstones17  42262  sticksstones18  42263  aks6d1c6lem5  42276  mzpexpmpt  42843  mzpresrename  42848  diophrw  42857  rabren3dioph  42913  lnrfg  43217  seff  44407  sblpnf  44408  binomcxplemnotnn0  44454  stoweidlem44  46147  stirlinglem8  46184  fourierdlem62  46271  fouriersw  46334  nnsum3primes4  47893  grtriclwlk3  48050  zlmodzxzldeplem1  48606  aacllem  49907  amgmwlem  49908