![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fssres | Structured version Visualization version GIF version |
Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.) |
Ref | Expression |
---|---|
fssres | ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 6328 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | fnssres 6442 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶) | |
3 | resss 5843 | . . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹 | |
4 | 3 | rnssi 5774 | . . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 |
5 | sstr 3923 | . . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) | |
6 | 4, 5 | mpan 689 | . . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) |
7 | 2, 6 | anim12i 615 | . . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
8 | 7 | an32s 651 | . . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
9 | 1, 8 | sylanb 584 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
10 | df-f 6328 | . 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) | |
11 | 9, 10 | sylibr 237 | 1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ⊆ wss 3881 ran crn 5520 ↾ cres 5521 Fn wfn 6319 ⟶wf 6320 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-fun 6326 df-fn 6327 df-f 6328 |
This theorem is referenced by: fssresd 6519 fssres2 6520 fresin 6521 fresaun 6523 f1ssres 6557 f2ndf 7799 elmapssres 8414 pmresg 8417 ralxpmap 8443 mapunen 8670 fofinf1o 8783 fseqenlem1 9435 inar1 10186 gruima 10213 addnqf 10359 mulnqf 10360 fseq1p1m1 12976 injresinj 13153 seqf1olem2 13406 wrdred1 13903 rlimres 14907 lo1res 14908 vdwnnlem1 16321 fsets 16508 resmhm 17977 resghm 18366 gsumzres 19022 gsumzadd 19035 gsum2dlem2 19084 dpjidcl 19173 ablfac1eu 19188 abvres 19603 znf1o 20243 islindf4 20527 kgencn 22161 ptrescn 22244 hmeores 22376 tsmsres 22749 tsmsmhm 22751 tsmsadd 22752 xrge0gsumle 23438 xrge0tsms 23439 ovolicc2lem4 24124 limcdif 24479 limcflf 24484 limcmo 24485 dvres 24514 dvres3a 24517 aannenlem1 24924 logcn 25238 dvlog 25242 dvlog2 25244 logtayl 25251 dvatan 25521 atancn 25522 efrlim 25555 amgm 25576 dchrelbas2 25821 redwlklem 27461 pthdivtx 27518 hhssabloilem 29044 hhssnv 29047 wrdres 30639 gsumpart 30740 xrge0tsmsd 30742 cntmeas 31595 eulerpartlemt 31739 eulerpartlemmf 31743 eulerpartlemgvv 31744 subiwrd 31753 sseqp1 31763 poimirlem4 35061 mbfresfi 35103 mbfposadd 35104 itg2gt0cn 35112 sdclem2 35180 mzpcompact2lem 39692 eldiophb 39698 eldioph2 39703 cncfiooicclem1 42535 fouriersw 42873 sge0tsms 43019 psmeasure 43110 sssmf 43372 resmgmhm 44418 lindslinindimp2lem2 44868 |
Copyright terms: Public domain | W3C validator |