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

Theorem fssres 6747
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 6539 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 fnssres 6663 . . . . 5 ((𝐹 Fn 𝐴𝐶𝐴) → (𝐹𝐶) Fn 𝐶)
3 resss 6001 . . . . . . 7 (𝐹𝐶) ⊆ 𝐹
43rnssi 5934 . . . . . 6 ran (𝐹𝐶) ⊆ ran 𝐹
5 sstr 3988 . . . . . 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 6539 . 2 ((𝐹𝐶):𝐶𝐵 ↔ ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
119, 10sylibr 233 1 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wss 3946  ran crn 5673  cres 5674   Fn wfn 6530  wf 6531
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  ax-sep 5295  ax-nul 5302  ax-pr 5423
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 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5145  df-opab 5207  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-fun 6537  df-fn 6538  df-f 6539
This theorem is referenced by:  fssresd  6748  fssres2  6749  fresin  6750  fresaun  6752  f1ssres  6785  f2ndf  8093  elmapssres  8849  pmresg  8852  ralxpmap  8878  mapunen  9134  fofinf1o  9315  fseqenlem1  10006  inar1  10757  gruima  10784  addnqf  10930  mulnqf  10931  fseq1p1m1  13562  injresinj  13740  seqf1olem2  13995  wrdred1  14497  rlimres  15489  lo1res  15490  vdwnnlem1  16915  fsets  17089  resmhm  18688  resghm  19093  gsumzres  19760  gsumzadd  19773  gsum2dlem2  19822  dpjidcl  19911  ablfac1eu  19926  abvres  20424  znf1o  21080  islindf4  21366  kgencn  23029  ptrescn  23112  hmeores  23244  tsmsres  23617  tsmsmhm  23619  tsmsadd  23620  xrge0gsumle  24318  xrge0tsms  24319  ovolicc2lem4  25006  limcdif  25362  limcflf  25367  limcmo  25368  dvres  25397  dvres3a  25400  aannenlem1  25810  logcn  26124  dvlog  26128  dvlog2  26130  logtayl  26137  dvatan  26407  atancn  26408  efrlim  26441  amgm  26462  dchrelbas2  26707  redwlklem  28895  pthdivtx  28953  hhssabloilem  30479  hhssnv  30482  wrdres  32074  gsumpart  32178  xrge0tsmsd  32180  cntmeas  33155  eulerpartlemt  33301  eulerpartlemmf  33305  eulerpartlemgvv  33306  subiwrd  33315  sseqp1  33325  poimirlem4  36397  mbfresfi  36439  mbfposadd  36440  itg2gt0cn  36448  sdclem2  36516  mzpcompact2lem  41360  eldiophb  41366  eldioph2  41371  cncfiooicclem1  44482  fouriersw  44820  sge0tsms  44969  psmeasure  45060  sssmf  45327  resmgmhm  46441  lindslinindimp2lem2  46980
  Copyright terms: Public domain W3C validator