Theorem fss 6718

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 3938	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 33	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 624	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6535	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6535	. . 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 3899  ran crn 5652   Fn wfn 6526  ⟶wf 6527

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 3916  df-f 6535

This theorem is used by:  fssd  6719  f1ss  6777  fcdmssb  7114  fsn2  7129  fprb  7191  ofco  7707  ffoss  7947  issmo2  8341  smoiso  8354  ssdomg  9011  alephfplem4  10167  cofsmo  10328  fin23lem17  10397  hsmexlem1  10485  axdc3lem4  10512  ac6s  10543  gruen  10878  intgru  10880  ingru  10881  hashf1lem1  14580  sswrd  14647  repsdf2  14909  limsupgre  15628  abscn2  15746  recn2  15748  imcn2  15749  climabs  15751  climre  15753  climim  15754  rlimabs  15756  rlimre  15758  rlimim  15759  caucvgrlem  15820  caurcvgr  15821  caucvgrlem2  15822  caurcvg  15824  fsumre  15955  fsumim  15956  0ram  17178  ramub1  17186  ramcl  17187  acsinfd  18710  acsdomd  18711  gsumval1  18852  resmgmhm2  18881  resmhm2  18997  prdsgrpd  19240  prdsinvgd  19241  symgtrinv  19666  prdscmnd  20055  prdsabld  20056  pgpfaclem1  20277  prdsrngd  20378  prdsmulrcl  20529  prdsringd  20530  prdscrngd  20531  abvf  21052  prdslmodd  21224  zntoslem  21842  regsumsupp  21908  dsmmsubg  22029  dsmmlss  22030  islinds2  22099  lindsmm  22114  lsslindf  22116  psrridm  22250  coe1fval3  22506  1stccnp  23761  1stckgen  23853  prdstps  23928  pthaus  23937  txcmplem2  23941  ptcmpfi  24112  ptcmplem1  24351  ptcmpg  24356  prdstmdd  24423  prdstgpd  24424  ismet2  24632  prdsxmetlem  24667  imasdsf1olem  24672  prdsms  24830  isngp2  24896  metdscn  25156  lmmbr  25559  causs  25599  ovolfioo  25768  ovolficc  25769  ovolfsf  25772  elovolm  25776  ovollb  25780  ovolunlem1a  25797  ovolunlem1  25798  ovolicc2lem1  25818  ovolicc2lem2  25819  ovolicc2lem3  25820  ovolicc2lem4  25821  ovolicc2  25823  uniiccdif  25879  uniioovol  25880  uniiccvol  25881  uniioombllem2  25884  uniioombllem3a  25885  uniioombllem3  25886  uniioombllem4  25887  uniioombllem5  25888  uniioombl  25890  dyadmbl  25901  vitalilem3  25911  vitalilem4  25912  vitalilem5  25913  ismbf  25929  mbfid  25936  0plef  25973  i1f1  25991  i1faddlem  25994  i1fsub  26009  itg1sub  26010  mbfi1fseqlem4  26019  itg2le  26040  itg2mulclem  26047  itg2mulc  26048  itg2monolem1  26051  itg2monolem2  26052  itg2monolem3  26053  itg2mono  26054  itg2i1fseq3  26058  itg2addlem  26059  itg2gt0  26061  itg2cnlem1  26062  itg2cnlem2  26063  dvfre  26251  dvnfre  26252  dvferm1  26285  dvferm2  26287  rolle  26290  dvgt0lem1  26302  dvivthlem1  26308  dvne0  26311  lhop1lem  26313  lhop2  26315  lhop  26316  dvcnvrelem1  26317  dvcnvre  26319  dvcvx  26320  dvfsumrlim  26331  tdeglem3  26357  elplyr  26499  taylthlem2  26683  taylth  26684  ulmcn  26708  iblulm  26716  efcvx  26758  dvrelog  26947  relogcn  26948  dvlog2  26963  leibpi  27252  efrlim  27279  jensenlem2  27297  jensen  27298  amgmlem  27299  amgm  27300  wilthlem2  27378  wilthlem3  27379  basellem7  27396  basellem9  27398  lgsfcl  27614  lgsdchr  27664  dchrvmasumlem1  27804  dchrisum0lem3  27828  axlowdimlem4  29505  axlowdimlem7  29508  axlowdimlem10  29511  upgruhgr  29662  lfuhgr  29708  subgrwlk  30251  konigsbergssiedgw  30833  pliguhgr  31070  0oo  31373  hhsscms  31862  nlelchi  32645  hmopidmchi  32735  pjinvari  32775  padct  33292  smatrcl  34410  lmlim  34561  rge0scvg  34563  lmdvg  34567  lmdvglim  34568  rrhre  34635  esumfsupre  34685  hashf2  34698  eulerpartlems  34975  eulerpartlemgs2  34995  coinfliprv  35098  fdvposlt  35211  fdvposle  35213  breprexpnat  35246  circlemethnat  35253  circlevma  35254  tgoldbachgtde  35272  ptpconn  35967  poimirlem8  38514  poimirlem18  38524  poimirlem21  38527  poimirlem22  38528  mblfinlem2  38544  mbfresfi  38552  itg2addnclem  38557  itg2addnclem2  38558  itg2addnc  38560  itg2gt0cn  38561  ftc1anclem8  38586  fdc  38647  heiborlem6  38718  heibor  38723  lfl0f  40094  intlewftc  43079  sticksstones3  43166  sticksstones9  43172  sticksstones11  43174  sticksstones17  43181  sticksstones18  43182  aks6d1c6lem5  43195  mzpexpmpt  43709  mzpresrename  43714  diophrw  43723  rabren3dioph  43775  lnrfg  44079  seff  45252  sblpnf  45253  binomcxplemnotnn0  45299  stoweidlem44  46998  stirlinglem8  47035  fourierdlem62  47122  fouriersw  47185  nnsum3primes4  48830  grtriclwlk3  48987  zlmodzxzldeplem1  49556  aacllem  50883  amgmwlem  50931