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

Theorem fssres 6037
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 5861 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 fnssres 5972 . . . . 5 ((𝐹 Fn 𝐴𝐶𝐴) → (𝐹𝐶) Fn 𝐶)
3 resss 5391 . . . . . . 7 (𝐹𝐶) ⊆ 𝐹
4 rnss 5324 . . . . . . 7 ((𝐹𝐶) ⊆ 𝐹 → ran (𝐹𝐶) ⊆ ran 𝐹)
53, 4ax-mp 5 . . . . . 6 ran (𝐹𝐶) ⊆ ran 𝐹
6 sstr 3596 . . . . . 6 ((ran (𝐹𝐶) ⊆ ran 𝐹 ∧ ran 𝐹𝐵) → ran (𝐹𝐶) ⊆ 𝐵)
75, 6mpan 705 . . . . 5 (ran 𝐹𝐵 → ran (𝐹𝐶) ⊆ 𝐵)
82, 7anim12i 589 . . . 4 (((𝐹 Fn 𝐴𝐶𝐴) ∧ ran 𝐹𝐵) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
98an32s 845 . . 3 (((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ∧ 𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
101, 9sylanb 489 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
11 df-f 5861 . 2 ((𝐹𝐶):𝐶𝐵 ↔ ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
1210, 11sylibr 224 1 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wss 3560  ran crn 5085  cres 5086   Fn wfn 5852  wf 5853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-fun 5859  df-fn 5860  df-f 5861
This theorem is referenced by:  fssresd  6038  fssres2  6039  fresin  6040  fresaun  6042  f1ssres  6075  f2ndf  7243  elmapssres  7842  pmresg  7845  ralxpmap  7867  mapunen  8089  fofinf1o  8201  fseqenlem1  8807  inar1  9557  gruima  9584  addnqf  9730  mulnqf  9731  fseq1p1m1  12371  injresinj  12545  seqf1olem2  12797  wrdred1  13304  rlimres  14239  lo1res  14240  vdwnnlem1  15642  fsets  15831  resmhm  17299  resghm  17616  gsumzres  18250  gsumzadd  18262  gsum2dlem2  18310  dpjidcl  18397  ablfac1eu  18412  abvres  18779  znf1o  19840  islindf4  20117  kgencn  21299  ptrescn  21382  hmeores  21514  tsmsres  21887  tsmsmhm  21889  tsmsadd  21890  xrge0gsumle  22576  xrge0tsms  22577  ovolicc2lem4  23228  limcdif  23580  limcflf  23585  limcmo  23586  dvres  23615  dvres3a  23618  aannenlem1  24021  logcn  24327  dvlog  24331  dvlog2  24333  logtayl  24340  dvatan  24596  atancn  24597  efrlim  24630  amgm  24651  dchrelbas2  24896  redwlklem  26471  pthdivtx  26528  hhssabloilem  28006  hhssnv  28009  xrge0tsmsd  29612  cntmeas  30112  eulerpartlemt  30256  eulerpartlemmf  30260  eulerpartlemgvv  30261  subiwrd  30270  sseqp1  30280  wrdres  30439  poimirlem4  33084  mbfresfi  33127  mbfposadd  33128  itg2gt0cn  33136  sdclem2  33209  mzpcompact2lem  36833  eldiophb  36839  eldioph2  36844  cncfiooicclem1  39441  fouriersw  39785  sge0tsms  39934  psmeasure  40025  sssmf  40284  resmgmhm  41116  lindslinindimp2lem2  41566
  Copyright terms: Public domain W3C validator