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 3943	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 621	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6521	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6521	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 298	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 411	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3904  ran crn 5646   Fn wfn 6512  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3921  df-f 6521

This theorem is referenced by:  fssd  6705  f1ss  6763  fcdmssb  7099  fsn2  7114  fprb  7174  ofco  7681  ffoss  7923  issmo2  8315  smoiso  8328  ssdomg  8977  alephfplem4  10060  cofsmo  10223  fin23lem17  10292  hsmexlem1  10380  axdc3lem4  10407  ac6s  10438  gruen  10767  intgru  10769  ingru  10770  hashf1lem1  14465  sswrd  14532  repsdf2  14788  limsupgre  15491  abscn2  15609  recn2  15611  imcn2  15612  climabs  15614  climre  15616  climim  15617  rlimabs  15619  rlimre  15621  rlimim  15622  caucvgrlem  15683  caurcvgr  15684  caucvgrlem2  15685  caurcvg  15687  fsumre  15819  fsumim  15820  0ram  17039  ramub1  17047  ramcl  17048  acsinfd  18571  acsdomd  18572  gsumval1  18700  resmgmhm2  18729  resmhm2  18838  prdsgrpd  19075  prdsinvgd  19076  symgtrinv  19495  prdscmnd  19884  prdsabld  19885  pgpfaclem1  20106  prdsrngd  20205  prdsmulrcl  20347  prdsringd  20348  prdscrngd  20349  abvf  20844  prdslmodd  21016  zntoslem  21588  regsumsupp  21654  dsmmsubg  21775  dsmmlss  21776  islinds2  21845  lindsmm  21860  lsslindf  21862  psrridm  21994  coe1fval3  22250  1stccnp  23502  1stckgen  23594  prdstps  23669  pthaus  23678  txcmplem2  23682  ptcmpfi  23853  ptcmplem1  24092  ptcmpg  24097  prdstmdd  24164  prdstgpd  24165  ismet2  24373  prdsxmetlem  24408  imasdsf1olem  24413  prdsms  24571  isngp2  24637  metdscn  24897  lmmbr  25300  causs  25340  ovolfioo  25509  ovolficc  25510  ovolfsf  25513  elovolm  25517  ovollb  25521  ovolunlem1a  25538  ovolunlem1  25539  ovolicc2lem1  25559  ovolicc2lem2  25560  ovolicc2lem3  25561  ovolicc2lem4  25562  ovolicc2  25564  uniiccdif  25620  uniioovol  25621  uniiccvol  25622  uniioombllem2  25625  uniioombllem3a  25626  uniioombllem3  25627  uniioombllem4  25628  uniioombllem5  25629  uniioombl  25631  dyadmbl  25642  vitalilem3  25652  vitalilem4  25653  vitalilem5  25654  ismbf  25670  mbfid  25677  0plef  25714  i1f1  25732  i1faddlem  25735  i1fsub  25750  itg1sub  25751  mbfi1fseqlem4  25760  itg2le  25781  itg2mulclem  25788  itg2mulc  25789  itg2monolem1  25792  itg2monolem2  25793  itg2monolem3  25794  itg2mono  25795  itg2i1fseq3  25799  itg2addlem  25800  itg2gt0  25802  itg2cnlem1  25803  itg2cnlem2  25804  dvfre  25993  dvnfre  25994  dvferm1  26027  dvferm2  26029  rolle  26032  dvgt0lem1  26044  dvivthlem1  26050  dvne0  26053  lhop1lem  26055  lhop2  26057  lhop  26058  dvcnvrelem1  26059  dvcnvre  26061  dvcvx  26062  dvfsumrlim  26073  tdeglem3  26099  elplyr  26241  taylthlem2  26414  taylth  26415  ulmcn  26439  iblulm  26447  efcvx  26489  dvrelog  26679  relogcn  26680  dvlog2  26695  leibpi  26984  efrlim  27011  jensenlem2  27029  jensen  27030  amgmlem  27031  amgm  27032  wilthlem2  27110  wilthlem3  27111  basellem7  27128  basellem9  27130  lgsfcl  27346  lgsdchr  27396  dchrvmasumlem1  27536  dchrisum0lem3  27560  axlowdimlem4  29092  axlowdimlem7  29095  axlowdimlem10  29098  upgruhgr  29249  konigsbergssiedgw  30398  pliguhgr  30635  0oo  30938  hhsscms  31427  nlelchi  32210  hmopidmchi  32300  pjinvari  32340  padct  32870  smatrcl  34054  lmlim  34205  rge0scvg  34207  lmdvg  34211  lmdvglim  34212  rrhre  34279  esumfsupre  34329  hashf2  34342  eulerpartlems  34618  eulerpartlemgs2  34638  coinfliprv  34741  fdvposlt  34857  fdvposle  34859  breprexpnat  34892  circlemethnat  34899  circlevma  34900  tgoldbachgtde  34918  lfuhgr  35432  subgrwlk  35446  ptpconn  35547  poimirlem8  38091  poimirlem18  38101  poimirlem21  38104  poimirlem22  38105  mblfinlem2  38121  mbfresfi  38129  itg2addnclem  38134  itg2addnclem2  38135  itg2addnc  38137  itg2gt0cn  38138  ftc1anclem8  38163  fdc  38208  heiborlem6  38279  heibor  38284  lfl0f  39657  intlewftc  42642  sticksstones3  42729  sticksstones9  42735  sticksstones11  42737  sticksstones17  42744  sticksstones18  42745  aks6d1c6lem5  42758  mzpexpmpt  43290  mzpresrename  43295  diophrw  43304  rabren3dioph  43356  lnrfg  43660  seff  44849  sblpnf  44850  binomcxplemnotnn0  44896  stoweidlem44  46582  stirlinglem8  46619  fourierdlem62  46706  fouriersw  46769  nnsum3primes4  48374  grtriclwlk3  48531  zlmodzxzldeplem1  49086  aacllem  50386  amgmwlem  50387