![]() |
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 6501 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | fnssres 6625 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶) | |
3 | resss 5963 | . . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹 | |
4 | 3 | rnssi 5896 | . . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 |
5 | sstr 3953 | . . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) | |
6 | 4, 5 | mpan 689 | . . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) |
7 | 2, 6 | anim12i 614 | . . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
8 | 7 | an32s 651 | . . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
9 | 1, 8 | sylanb 582 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
10 | df-f 6501 | . 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) | |
11 | 9, 10 | sylibr 233 | 1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ⊆ wss 3911 ran crn 5635 ↾ cres 5636 Fn wfn 6492 ⟶wf 6493 |
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 2708 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
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 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-br 5107 df-opab 5169 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-fun 6499 df-fn 6500 df-f 6501 |
This theorem is referenced by: fssresd 6710 fssres2 6711 fresin 6712 fresaun 6714 f1ssres 6747 f2ndf 8053 elmapssres 8806 pmresg 8809 ralxpmap 8835 mapunen 9091 fofinf1o 9272 fseqenlem1 9961 inar1 10712 gruima 10739 addnqf 10885 mulnqf 10886 fseq1p1m1 13516 injresinj 13694 seqf1olem2 13949 wrdred1 14449 rlimres 15441 lo1res 15442 vdwnnlem1 16868 fsets 17042 resmhm 18632 resghm 19025 gsumzres 19687 gsumzadd 19700 gsum2dlem2 19749 dpjidcl 19838 ablfac1eu 19853 abvres 20301 znf1o 20961 islindf4 21247 kgencn 22910 ptrescn 22993 hmeores 23125 tsmsres 23498 tsmsmhm 23500 tsmsadd 23501 xrge0gsumle 24199 xrge0tsms 24200 ovolicc2lem4 24887 limcdif 25243 limcflf 25248 limcmo 25249 dvres 25278 dvres3a 25281 aannenlem1 25691 logcn 26005 dvlog 26009 dvlog2 26011 logtayl 26018 dvatan 26288 atancn 26289 efrlim 26322 amgm 26343 dchrelbas2 26588 redwlklem 28622 pthdivtx 28680 hhssabloilem 30206 hhssnv 30209 wrdres 31796 gsumpart 31900 xrge0tsmsd 31902 cntmeas 32828 eulerpartlemt 32974 eulerpartlemmf 32978 eulerpartlemgvv 32979 subiwrd 32988 sseqp1 32998 poimirlem4 36085 mbfresfi 36127 mbfposadd 36128 itg2gt0cn 36136 sdclem2 36204 mzpcompact2lem 41077 eldiophb 41083 eldioph2 41088 cncfiooicclem1 44141 fouriersw 44479 sge0tsms 44628 psmeasure 44719 sssmf 44986 resmgmhm 46099 lindslinindimp2lem2 46547 |
Copyright terms: Public domain | W3C validator |