Theorem fss 6527

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

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3936  ran crn 5556   Fn wfn 6350  ⟶wf 6351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-f 6359

This theorem is referenced by:  fssd  6528  f1ss  6580  frnssb  6885  fsn2  6898  fprb  6956  ofco  7429  ffoss  7647  issmo2  7986  smoiso  7999  ssdomg  8555  alephfplem4  9533  cofsmo  9691  fin23lem17  9760  hsmexlem1  9848  axdc3lem4  9875  ac6s  9906  gruen  10234  intgru  10236  ingru  10237  hashf1lem1  13814  sswrd  13870  repsdf2  14140  limsupgre  14838  abscn2  14955  recn2  14957  imcn2  14958  climabs  14960  climre  14962  climim  14963  rlimabs  14965  rlimre  14967  rlimim  14968  caucvgrlem  15029  caurcvgr  15030  caucvgrlem2  15031  caurcvg  15033  fsumre  15163  fsumim  15164  0ram  16356  ramub1  16364  ramcl  16365  acsinfd  17790  acsdomd  17791  gsumval1  17893  resmhm2  17986  prdsgrpd  18209  prdsinvgd  18210  symgtrinv  18600  prdscmnd  18981  prdsabld  18982  pgpfaclem1  19203  prdsringd  19362  prdscrngd  19363  abvf  19594  prdslmodd  19741  psrridm  20184  coe1fval3  20376  zntoslem  20703  regsumsupp  20766  dsmmsubg  20887  dsmmlss  20888  islinds2  20957  lindsmm  20972  lsslindf  20974  1stccnp  22070  1stckgen  22162  prdstps  22237  pthaus  22246  txcmplem2  22250  ptcmpfi  22421  ptcmplem1  22660  ptcmpg  22665  prdstmdd  22732  prdstgpd  22733  ismet2  22943  prdsxmetlem  22978  imasdsf1olem  22983  prdsms  23141  isngp2  23206  metdscn  23464  lmmbr  23861  causs  23901  ovolfioo  24068  ovolficc  24069  ovolfsf  24072  elovolm  24076  ovollb  24080  ovolunlem1a  24097  ovolunlem1  24098  ovolicc2lem1  24118  ovolicc2lem2  24119  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2  24123  uniiccdif  24179  uniioovol  24180  uniiccvol  24181  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombl  24190  dyadmbl  24201  vitalilem3  24211  vitalilem4  24212  vitalilem5  24213  ismbf  24229  mbfid  24236  0plef  24273  i1f1  24291  i1faddlem  24294  i1fsub  24309  itg1sub  24310  mbfi1fseqlem4  24319  itg2le  24340  itg2mulclem  24347  itg2mulc  24348  itg2monolem1  24351  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  itg2i1fseq3  24358  itg2addlem  24359  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  dvfre  24548  dvnfre  24549  dvferm1  24582  dvferm2  24584  rolle  24587  dvgt0lem1  24599  dvivthlem1  24605  dvne0  24608  lhop1lem  24610  lhop2  24612  lhop  24613  dvcnvrelem1  24614  dvcnvre  24616  dvcvx  24617  dvfsumrlim  24628  tdeglem3  24653  elplyr  24791  taylthlem2  24962  taylth  24963  ulmcn  24987  iblulm  24995  efcvx  25037  dvrelog  25220  relogcn  25221  dvlog2  25236  leibpi  25520  efrlim  25547  jensenlem2  25565  jensen  25566  amgmlem  25567  amgm  25568  wilthlem2  25646  wilthlem3  25647  basellem7  25664  basellem9  25666  lgsfcl  25881  lgsdchr  25931  dchrvmasumlem1  26071  dchrisum0lem3  26095  axlowdimlem4  26731  axlowdimlem7  26734  axlowdimlem10  26737  upgruhgr  26887  konigsbergssiedgw  28029  pliguhgr  28263  0oo  28566  hhsscms  29055  nlelchi  29838  hmopidmchi  29928  pjinvari  29968  padct  30455  smatrcl  31061  lmlim  31190  rge0scvg  31192  lmdvg  31196  lmdvglim  31197  rrhre  31262  esumfsupre  31330  hashf2  31343  eulerpartlems  31618  eulerpartlemgs2  31638  coinfliprv  31740  fdvposlt  31870  fdvposle  31872  breprexpnat  31905  circlemethnat  31912  circlevma  31913  tgoldbachgtde  31931  lfuhgr  32364  subgrwlk  32379  ptpconn  32480  poimirlem8  34915  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  mblfinlem2  34945  mbfresfi  34953  itg2addnclem  34958  itg2addnclem2  34959  itg2addnc  34961  itg2gt0cn  34962  ftc1anclem8  34989  fdc  35035  heiborlem6  35109  heibor  35114  lfl0f  36220  mzpexpmpt  39391  mzpresrename  39396  diophrw  39405  rabren3dioph  39461  lnrfg  39768  seff  40690  sblpnf  40691  binomcxplemnotnn0  40737  stoweidlem44  42378  stirlinglem8  42415  fourierdlem62  42502  fouriersw  42565  nnsum3primes4  44002  resmgmhm2  44115  zlmodzxzldeplem1  44604  aacllem  44951  amgmwlem  44952