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

Theorem fssres 6546
 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 6361 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
2 fnssres 6472 . . . . 5 ((𝐹 Fn 𝐴𝐶𝐴) → (𝐹𝐶) Fn 𝐶)
3 resss 5880 . . . . . . 7 (𝐹𝐶) ⊆ 𝐹
43rnssi 5812 . . . . . 6 ran (𝐹𝐶) ⊆ ran 𝐹
5 sstr 3977 . . . . . 6 ((ran (𝐹𝐶) ⊆ ran 𝐹 ∧ ran 𝐹𝐵) → ran (𝐹𝐶) ⊆ 𝐵)
64, 5mpan 688 . . . . 5 (ran 𝐹𝐵 → ran (𝐹𝐶) ⊆ 𝐵)
72, 6anim12i 614 . . . 4 (((𝐹 Fn 𝐴𝐶𝐴) ∧ ran 𝐹𝐵) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
87an32s 650 . . 3 (((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ∧ 𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
91, 8sylanb 583 . 2 ((𝐹:𝐴𝐵𝐶𝐴) → ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
10 df-f 6361 . 2 ((𝐹𝐶):𝐶𝐵 ↔ ((𝐹𝐶) Fn 𝐶 ∧ ran (𝐹𝐶) ⊆ 𝐵))
119, 10sylibr 236 1 ((𝐹:𝐴𝐵𝐶𝐴) → (𝐹𝐶):𝐶𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3938  ran crn 5558   ↾ cres 5559   Fn wfn 6352  ⟶wf 6353 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 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-fun 6359  df-fn 6360  df-f 6361 This theorem is referenced by:  fssresd  6547  fssres2  6548  fresin  6549  fresaun  6551  f1ssres  6584  f2ndf  7818  elmapssres  8433  pmresg  8436  ralxpmap  8462  mapunen  8688  fofinf1o  8801  fseqenlem1  9452  inar1  10199  gruima  10226  addnqf  10372  mulnqf  10373  fseq1p1m1  12984  injresinj  13161  seqf1olem2  13413  wrdred1  13914  rlimres  14917  lo1res  14918  vdwnnlem1  16333  fsets  16518  resmhm  17987  resghm  18376  gsumzres  19031  gsumzadd  19044  gsum2dlem2  19093  dpjidcl  19182  ablfac1eu  19197  abvres  19612  znf1o  20700  islindf4  20984  kgencn  22166  ptrescn  22249  hmeores  22381  tsmsres  22754  tsmsmhm  22756  tsmsadd  22757  xrge0gsumle  23443  xrge0tsms  23444  ovolicc2lem4  24123  limcdif  24476  limcflf  24481  limcmo  24482  dvres  24511  dvres3a  24514  aannenlem1  24919  logcn  25232  dvlog  25236  dvlog2  25238  logtayl  25245  dvatan  25515  atancn  25516  efrlim  25549  amgm  25570  dchrelbas2  25815  redwlklem  27455  pthdivtx  27512  hhssabloilem  29040  hhssnv  29043  wrdres  30615  xrge0tsmsd  30694  cntmeas  31487  eulerpartlemt  31631  eulerpartlemmf  31635  eulerpartlemgvv  31636  subiwrd  31645  sseqp1  31655  poimirlem4  34898  mbfresfi  34940  mbfposadd  34941  itg2gt0cn  34949  sdclem2  35019  mzpcompact2lem  39355  eldiophb  39361  eldioph2  39366  cncfiooicclem1  42183  fouriersw  42523  sge0tsms  42669  psmeasure  42760  sssmf  43022  resmgmhm  44072  lindslinindimp2lem2  44521
 Copyright terms: Public domain W3C validator