MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fssres Structured version   Visualization version   GIF version

Theorem fssres 6709
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)
Assertion
Ref Expression
fssres ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)

Proof of Theorem fssres
StepHypRef Expression
1 df-f 6501 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 fnssres 6625 . . . . 5 ((𝐹 Fn 𝐴𝐶𝐴) → (𝐹𝐶) Fn 𝐶)
3 resss 5963 . . . . . . 7 (𝐹𝐶) ⊆ 𝐹
43rnssi 5896 . . . . . 6 ran (𝐹𝐶) ⊆ ran 𝐹
5 sstr 3953 . . . . . 6 ((ran (𝐹𝐶) ⊆ ran 𝐹 ∧ ran 𝐹𝐵) → ran (𝐹𝐶) ⊆ 𝐵)
64, 5mpan 689 . . . . 5 (ran 𝐹𝐵 → ran (𝐹𝐶) ⊆ 𝐵)
72, 6anim12i 614 . . . 4 (((𝐹 Fn 𝐴𝐶𝐴) ∧ ran 𝐹𝐵) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
87an32s 651 . . 3 (((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ∧ 𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
91, 8sylanb 582 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
10 df-f 6501 . 2 ((𝐹𝐶):𝐶𝐵 ↔ ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
119, 10sylibr 233 1 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wss 3911  ran crn 5635  cres 5636   Fn wfn 6492  wf 6493
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 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  fssresd  6710  fssres2  6711  fresin  6712  fresaun  6714  f1ssres  6747  f2ndf  8053  elmapssres  8806  pmresg  8809  ralxpmap  8835  mapunen  9091  fofinf1o  9272  fseqenlem1  9961  inar1  10712  gruima  10739  addnqf  10885  mulnqf  10886  fseq1p1m1  13516  injresinj  13694  seqf1olem2  13949  wrdred1  14449  rlimres  15441  lo1res  15442  vdwnnlem1  16868  fsets  17042  resmhm  18632  resghm  19025  gsumzres  19687  gsumzadd  19700  gsum2dlem2  19749  dpjidcl  19838  ablfac1eu  19853  abvres  20301  znf1o  20961  islindf4  21247  kgencn  22910  ptrescn  22993  hmeores  23125  tsmsres  23498  tsmsmhm  23500  tsmsadd  23501  xrge0gsumle  24199  xrge0tsms  24200  ovolicc2lem4  24887  limcdif  25243  limcflf  25248  limcmo  25249  dvres  25278  dvres3a  25281  aannenlem1  25691  logcn  26005  dvlog  26009  dvlog2  26011  logtayl  26018  dvatan  26288  atancn  26289  efrlim  26322  amgm  26343  dchrelbas2  26588  redwlklem  28622  pthdivtx  28680  hhssabloilem  30206  hhssnv  30209  wrdres  31796  gsumpart  31900  xrge0tsmsd  31902  cntmeas  32828  eulerpartlemt  32974  eulerpartlemmf  32978  eulerpartlemgvv  32979  subiwrd  32988  sseqp1  32998  poimirlem4  36085  mbfresfi  36127  mbfposadd  36128  itg2gt0cn  36136  sdclem2  36204  mzpcompact2lem  41077  eldiophb  41083  eldioph2  41088  cncfiooicclem1  44141  fouriersw  44479  sge0tsms  44628  psmeasure  44719  sssmf  44986  resmgmhm  46099  lindslinindimp2lem2  46547
  Copyright terms: Public domain W3C validator