Theorem fss 6735

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

Syntax hints:   → wi 4   ∧ wa 397   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548

This theorem is referenced by:  fssd  6736  f1ss  6794  fcdmssb  7121  fsn2  7134  fprb  7195  ofco  7693  ffoss  7932  issmo2  8349  smoiso  8362  ssdomg  8996  alephfplem4  10102  cofsmo  10264  fin23lem17  10333  hsmexlem1  10421  axdc3lem4  10448  ac6s  10479  gruen  10807  intgru  10809  ingru  10810  hashf1lem1  14415  hashf1lem1OLD  14416  sswrd  14472  repsdf2  14728  limsupgre  15425  abscn2  15543  recn2  15545  imcn2  15546  climabs  15548  climre  15550  climim  15551  rlimabs  15553  rlimre  15555  rlimim  15556  caucvgrlem  15619  caurcvgr  15620  caucvgrlem2  15621  caurcvg  15623  fsumre  15754  fsumim  15755  0ram  16953  ramub1  16961  ramcl  16962  acsinfd  18509  acsdomd  18510  gsumval1  18602  resmhm2  18702  prdsgrpd  18933  prdsinvgd  18934  symgtrinv  19340  prdscmnd  19729  prdsabld  19730  pgpfaclem1  19951  prdsringd  20134  prdscrngd  20135  abvf  20431  prdslmodd  20580  zntoslem  21112  regsumsupp  21175  dsmmsubg  21298  dsmmlss  21299  islinds2  21368  lindsmm  21383  lsslindf  21385  psrridm  21524  coe1fval3  21732  1stccnp  22966  1stckgen  23058  prdstps  23133  pthaus  23142  txcmplem2  23146  ptcmpfi  23317  ptcmplem1  23556  ptcmpg  23561  prdstmdd  23628  prdstgpd  23629  ismet2  23839  prdsxmetlem  23874  imasdsf1olem  23879  prdsms  24040  isngp2  24106  metdscn  24372  lmmbr  24775  causs  24815  ovolfioo  24984  ovolficc  24985  ovolfsf  24988  elovolm  24992  ovollb  24996  ovolunlem1a  25013  ovolunlem1  25014  ovolicc2lem1  25034  ovolicc2lem2  25035  ovolicc2lem3  25036  ovolicc2lem4  25037  ovolicc2  25039  uniiccdif  25095  uniioovol  25096  uniiccvol  25097  uniioombllem2  25100  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  uniioombl  25106  dyadmbl  25117  vitalilem3  25127  vitalilem4  25128  vitalilem5  25129  ismbf  25145  mbfid  25152  0plef  25189  i1f1  25207  i1faddlem  25210  i1fsub  25226  itg1sub  25227  mbfi1fseqlem4  25236  itg2le  25257  itg2mulclem  25264  itg2mulc  25265  itg2monolem1  25268  itg2monolem2  25269  itg2monolem3  25270  itg2mono  25271  itg2i1fseq3  25275  itg2addlem  25276  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  dvfre  25468  dvnfre  25469  dvferm1  25502  dvferm2  25504  rolle  25507  dvgt0lem1  25519  dvivthlem1  25525  dvne0  25528  lhop1lem  25530  lhop2  25532  lhop  25533  dvcnvrelem1  25534  dvcnvre  25536  dvcvx  25537  dvfsumrlim  25548  tdeglem3  25575  tdeglem3OLD  25576  elplyr  25715  taylthlem2  25886  taylth  25887  ulmcn  25911  iblulm  25919  efcvx  25961  dvrelog  26145  relogcn  26146  dvlog2  26161  leibpi  26447  efrlim  26474  jensenlem2  26492  jensen  26493  amgmlem  26494  amgm  26495  wilthlem2  26573  wilthlem3  26574  basellem7  26591  basellem9  26593  lgsfcl  26808  lgsdchr  26858  dchrvmasumlem1  26998  dchrisum0lem3  27022  axlowdimlem4  28203  axlowdimlem7  28206  axlowdimlem10  28209  upgruhgr  28362  konigsbergssiedgw  29503  pliguhgr  29739  0oo  30042  hhsscms  30531  nlelchi  31314  hmopidmchi  31404  pjinvari  31444  padct  31944  smatrcl  32776  lmlim  32927  rge0scvg  32929  lmdvg  32933  lmdvglim  32934  rrhre  33001  esumfsupre  33069  hashf2  33082  eulerpartlems  33359  eulerpartlemgs2  33379  coinfliprv  33481  fdvposlt  33611  fdvposle  33613  breprexpnat  33646  circlemethnat  33653  circlevma  33654  tgoldbachgtde  33672  lfuhgr  34108  subgrwlk  34123  ptpconn  34224  poimirlem8  36496  poimirlem18  36506  poimirlem21  36509  poimirlem22  36510  mblfinlem2  36526  mbfresfi  36534  itg2addnclem  36539  itg2addnclem2  36540  itg2addnc  36542  itg2gt0cn  36543  ftc1anclem8  36568  fdc  36613  heiborlem6  36684  heibor  36689  lfl0f  37939  intlewftc  40926  sticksstones3  40964  sticksstones9  40970  sticksstones11  40972  sticksstones17  40979  sticksstones18  40980  mzpexpmpt  41483  mzpresrename  41488  diophrw  41497  rabren3dioph  41553  lnrfg  41861  seff  43068  sblpnf  43069  binomcxplemnotnn0  43115  stoweidlem44  44760  stirlinglem8  44797  fourierdlem62  44884  fouriersw  44947  nnsum3primes4  46456  resmgmhm2  46569  prdsrngd  46677  zlmodzxzldeplem1  47181  aacllem  47848  amgmwlem  47849