Theorem fss 5969

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 3575	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 587	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 5808	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 5808	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 284	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 445	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 383   ⊆ wss 3540  ran crn 5039   Fn wfn 5799  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808

This theorem is referenced by:  fssd  5970  f1ss  6019  frnssb  6298  fsn2  6309  fsnex  6438  ofco  6815  ffoss  7020  issmo2  7333  smoiso  7346  mapsn  7785  ssdomg  7887  alephfplem4  8813  cofsmo  8974  fin23lem17  9043  hsmexlem1  9131  axdc3lem4  9158  ac6s  9189  gruen  9513  intgru  9515  ingru  9516  hashf1lem1  13096  sswrd  13168  wrdv  13175  repsdf2  13376  limsupgre  14060  abscn2  14177  recn2  14179  imcn2  14180  climabs  14182  climre  14184  climim  14185  rlimabs  14187  rlimre  14189  rlimim  14190  caucvgrlem  14251  caurcvgr  14252  caucvgrlem2  14253  caurcvg  14255  fsumre  14381  fsumim  14382  0ram  15562  ramub1  15570  ramcl  15571  acsinfd  17003  acsdomd  17004  gsumval1  17100  resmhm2  17183  prdsgrpd  17348  prdsinvgd  17349  symgtrinv  17715  prdscmnd  18087  prdsabld  18088  pgpfaclem1  18303  prdsringd  18435  prdscrngd  18436  abvf  18646  prdslmodd  18790  psrridm  19225  coe1fval3  19399  zntoslem  19724  regsumsupp  19787  dsmmsubg  19906  dsmmlss  19907  islinds2  19971  lindsmm  19986  lsslindf  19988  1stccnp  21075  1stckgen  21167  prdstps  21242  pthaus  21251  txcmplem2  21255  ptcmpfi  21426  ptcmplem1  21666  ptcmpg  21671  prdstmdd  21737  prdstgpd  21738  ismet2  21948  prdsxmetlem  21983  imasdsf1olem  21988  prdsms  22146  isngp2  22211  metdscn  22467  lmmbr  22864  causs  22904  ovolfioo  23043  ovolficc  23044  ovolfsf  23047  elovolm  23050  ovollb  23054  ovolunlem1a  23071  ovolunlem1  23072  ovolicc2lem1  23092  ovolicc2lem2  23093  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2  23097  uniiccdif  23152  uniioovol  23153  uniiccvol  23154  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombl  23163  dyadmbl  23174  vitalilem3  23185  vitalilem4  23186  vitalilem5  23187  ismbf  23203  mbfid  23209  0plef  23245  i1f1  23263  i1faddlem  23266  i1fsub  23281  itg1sub  23282  mbfi1fseqlem4  23291  itg2le  23312  itg2mulclem  23319  itg2mulc  23320  itg2monolem1  23323  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq3  23330  itg2addlem  23331  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  dvfre  23520  dvnfre  23521  dvferm1  23552  dvferm2  23554  rolle  23557  dvgt0lem1  23569  dvivthlem1  23575  dvne0  23578  lhop1lem  23580  lhop2  23582  lhop  23583  dvcnvrelem1  23584  dvcnvre  23586  dvcvx  23587  dvfsumrlim  23598  tdeglem3  23623  elplyr  23761  taylthlem2  23932  taylth  23933  ulmcn  23957  iblulm  23965  efcvx  24007  dvrelog  24183  relogcn  24184  dvlog2  24199  leibpi  24469  efrlim  24496  jensenlem2  24514  jensen  24515  amgmlem  24516  amgm  24517  wilthlem2  24595  wilthlem3  24596  basellem7  24613  basellem9  24615  lgsfcl  24830  lgsdchr  24880  dchrvmasumlem1  24984  dchrisum0lem3  25008  axlowdimlem4  25625  axlowdimlem7  25628  axlowdimlem10  25631  upgruhgr  25768  umisuhgra  25856  2trllemG  26088  constr3trllem1  26178  0oo  27028  hhsscms  27520  nlelchi  28304  hmopidmchi  28394  pjinvari  28434  padct  28885  smatrcl  29190  lmlim  29321  rge0scvg  29323  lmdvg  29327  lmdvglim  29328  rrhre  29393  esumfsupre  29460  hashf2  29473  eulerpartlems  29749  eulerpartlemgs2  29769  coinfliprv  29871  ptpcon  30469  fprb  30916  poimirlem8  32587  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  mblfinlem2  32617  mbfresfi  32626  itg2addnclem  32631  itg2addnclem2  32632  itg2addnc  32634  itg2gt0cn  32635  ftc1anclem8  32662  fdc  32711  heiborlem6  32785  heibor  32790  lfl0f  33374  mzpexpmpt  36326  mzpresrename  36331  diophrw  36340  rabren3dioph  36397  lnrfg  36708  seff  37530  sblpnf  37531  binomcxplemnotnn0  37577  mapsnd  38383  stoweidlem44  38937  stirlinglem8  38974  fourierdlem62  39061  fouriersw  39124  nnsum3primes4  40204  konigsbergssiedgw  41419  resmgmhm2  41589  zlmodzxzldeplem1  42083  aacllem  42356  amgmwlem  42357