Theorem fss 6729

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 3947	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 33	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 624	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6547	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6547	. . 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 3908  ran crn 5667   Fn wfn 6538  ⟶wf 6539

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3925  df-f 6547

This theorem is used by:  fssd  6730  f1ss  6788  fcdmssb  7124  fsn2  7139  fprb  7199  ofco  7712  ffoss  7952  issmo2  8345  smoiso  8358  ssdomg  9006  alephfplem4  10110  cofsmo  10271  fin23lem17  10340  hsmexlem1  10428  axdc3lem4  10455  ac6s  10486  gruen  10815  intgru  10817  ingru  10818  hashf1lem1  14512  sswrd  14579  repsdf2  14841  limsupgre  15558  abscn2  15676  recn2  15678  imcn2  15679  climabs  15681  climre  15683  climim  15684  rlimabs  15686  rlimre  15688  rlimim  15689  caucvgrlem  15750  caurcvgr  15751  caucvgrlem2  15752  caurcvg  15754  fsumre  15886  fsumim  15887  0ram  17105  ramub1  17113  ramcl  17114  acsinfd  18637  acsdomd  18638  gsumval1  18770  resmgmhm2  18799  resmhm2  18911  prdsgrpd  19147  prdsinvgd  19148  symgtrinv  19573  prdscmnd  19962  prdsabld  19963  pgpfaclem1  20184  prdsrngd  20285  prdsmulrcl  20434  prdsringd  20435  prdscrngd  20436  abvf  20955  prdslmodd  21127  zntoslem  21743  regsumsupp  21809  dsmmsubg  21930  dsmmlss  21931  islinds2  22000  lindsmm  22015  lsslindf  22017  psrridm  22149  coe1fval3  22405  1stccnp  23656  1stckgen  23748  prdstps  23823  pthaus  23832  txcmplem2  23836  ptcmpfi  24007  ptcmplem1  24246  ptcmpg  24251  prdstmdd  24318  prdstgpd  24319  ismet2  24527  prdsxmetlem  24562  imasdsf1olem  24567  prdsms  24725  isngp2  24791  metdscn  25051  lmmbr  25454  causs  25494  ovolfioo  25663  ovolficc  25664  ovolfsf  25667  elovolm  25671  ovollb  25675  ovolunlem1a  25692  ovolunlem1  25693  ovolicc2lem1  25713  ovolicc2lem2  25714  ovolicc2lem3  25715  ovolicc2lem4  25716  ovolicc2  25718  uniiccdif  25774  uniioovol  25775  uniiccvol  25776  uniioombllem2  25779  uniioombllem3a  25780  uniioombllem3  25781  uniioombllem4  25782  uniioombllem5  25783  uniioombl  25785  dyadmbl  25796  vitalilem3  25806  vitalilem4  25807  vitalilem5  25808  ismbf  25824  mbfid  25831  0plef  25868  i1f1  25886  i1faddlem  25889  i1fsub  25904  itg1sub  25905  mbfi1fseqlem4  25914  itg2le  25935  itg2mulclem  25942  itg2mulc  25943  itg2monolem1  25946  itg2monolem2  25947  itg2monolem3  25948  itg2mono  25949  itg2i1fseq3  25953  itg2addlem  25954  itg2gt0  25956  itg2cnlem1  25957  itg2cnlem2  25958  dvfre  26147  dvnfre  26148  dvferm1  26181  dvferm2  26183  rolle  26186  dvgt0lem1  26198  dvivthlem1  26204  dvne0  26207  lhop1lem  26209  lhop2  26211  lhop  26212  dvcnvrelem1  26213  dvcnvre  26215  dvcvx  26216  dvfsumrlim  26227  tdeglem3  26253  elplyr  26395  taylthlem2  26574  taylth  26575  ulmcn  26599  iblulm  26607  efcvx  26649  dvrelog  26839  relogcn  26840  dvlog2  26855  leibpi  27144  efrlim  27171  jensenlem2  27189  jensen  27190  amgmlem  27191  amgm  27192  wilthlem2  27270  wilthlem3  27271  basellem7  27288  basellem9  27290  lgsfcl  27506  lgsdchr  27556  dchrvmasumlem1  27696  dchrisum0lem3  27720  axlowdimlem4  29332  axlowdimlem7  29335  axlowdimlem10  29338  upgruhgr  29489  konigsbergssiedgw  30638  pliguhgr  30875  0oo  31178  hhsscms  31667  nlelchi  32450  hmopidmchi  32540  pjinvari  32580  padct  33100  smatrcl  34217  lmlim  34368  rge0scvg  34370  lmdvg  34374  lmdvglim  34375  rrhre  34442  esumfsupre  34492  hashf2  34505  eulerpartlems  34781  eulerpartlemgs2  34801  coinfliprv  34904  fdvposlt  35017  fdvposle  35019  breprexpnat  35052  circlemethnat  35059  circlevma  35060  tgoldbachgtde  35078  lfuhgr  35630  subgrwlk  35644  ptpconn  35745  poimirlem8  38319  poimirlem18  38329  poimirlem21  38332  poimirlem22  38333  mblfinlem2  38349  mbfresfi  38357  itg2addnclem  38362  itg2addnclem2  38363  itg2addnc  38365  itg2gt0cn  38366  ftc1anclem8  38391  fdc  38436  heiborlem6  38507  heibor  38512  lfl0f  39883  intlewftc  42868  sticksstones3  42955  sticksstones9  42961  sticksstones11  42963  sticksstones17  42970  sticksstones18  42971  aks6d1c6lem5  42984  mzpexpmpt  43516  mzpresrename  43521  diophrw  43530  rabren3dioph  43582  lnrfg  43886  seff  45059  sblpnf  45060  binomcxplemnotnn0  45106  stoweidlem44  46798  stirlinglem8  46835  fourierdlem62  46922  fouriersw  46985  nnsum3primes4  48593  grtriclwlk3  48750  zlmodzxzldeplem1  49320  aacllem  50661  amgmwlem  50690