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

Theorem fssres 5965
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 5791 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 fnssres 5901 . . . . 5 ((𝐹 Fn 𝐴𝐶𝐴) → (𝐹𝐶) Fn 𝐶)
3 resss 5326 . . . . . . 7 (𝐹𝐶) ⊆ 𝐹
4 rnss 5259 . . . . . . 7 ((𝐹𝐶) ⊆ 𝐹 → ran (𝐹𝐶) ⊆ ran 𝐹)
53, 4ax-mp 5 . . . . . 6 ran (𝐹𝐶) ⊆ ran 𝐹
6 sstr 3572 . . . . . 6 ((ran (𝐹𝐶) ⊆ ran 𝐹 ∧ ran 𝐹𝐵) → ran (𝐹𝐶) ⊆ 𝐵)
75, 6mpan 701 . . . . 5 (ran 𝐹𝐵 → ran (𝐹𝐶) ⊆ 𝐵)
82, 7anim12i 587 . . . 4 (((𝐹 Fn 𝐴𝐶𝐴) ∧ ran 𝐹𝐵) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
98an32s 841 . . 3 (((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ∧ 𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
101, 9sylanb 487 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
11 df-f 5791 . 2 ((𝐹𝐶):𝐶𝐵 ↔ ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
1210, 11sylibr 222 1 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wss 3536  ran crn 5026  cres 5027   Fn wfn 5782  wf 5783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-fun 5789  df-fn 5790  df-f 5791
This theorem is referenced by:  fssresd  5966  fssres2  5967  fresin  5968  fresaun  5970  f1ssres  6003  f2ndf  7144  elmapssres  7742  pmresg  7745  ralxpmap  7767  mapunen  7988  fofinf1o  8100  fseqenlem1  8704  inar1  9450  gruima  9477  addnqf  9623  mulnqf  9624  fseq1p1m1  12235  injresinj  12403  seqf1olem2  12655  rlimres  14080  lo1res  14081  vdwnnlem1  15480  fsets  15666  resmhm  17125  resghm  17442  gsumzres  18076  gsumzadd  18088  gsum2dlem2  18136  dpjidcl  18223  ablfac1eu  18238  abvres  18605  znf1o  19661  islindf4  19935  kgencn  21108  ptrescn  21191  hmeores  21323  tsmsres  21696  tsmsmhm  21698  tsmsadd  21699  xrge0gsumle  22373  xrge0tsms  22374  ovolicc2lem4  23009  limcdif  23360  limcflf  23365  limcmo  23366  dvres  23395  dvres3a  23398  aannenlem1  23801  logcn  24107  dvlog  24111  dvlog2  24113  logtayl  24120  dvatan  24376  atancn  24377  efrlim  24410  amgm  24431  dchrelbas2  24676  redwlk  25899  hhssabloilem  27305  hhssnv  27308  xrge0tsmsd  28919  cntmeas  29419  eulerpartlemt  29563  eulerpartlemmf  29567  eulerpartlemgvv  29568  subiwrd  29577  sseqp1  29587  wrdres  29746  poimirlem4  32383  mbfresfi  32426  mbfposadd  32427  itg2gt0cn  32435  sdclem2  32508  mzpcompact2lem  36132  eldiophb  36138  eldioph2  36143  cncfiooicclem1  38580  fouriersw  38925  sge0tsms  39074  psmeasure  39165  sssmf  39426  wrdred1  40042  red1wlklem  40879  pthdivtx  40934  resmgmhm  41587  lindslinindimp2lem2  42041
  Copyright terms: Public domain W3C validator