| 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 6565 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
| 2 | fnssres 6691 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶) | |
| 3 | resss 6019 | . . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹 | |
| 4 | 3 | rnssi 5951 | . . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 |
| 5 | sstr 3992 | . . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) | |
| 6 | 4, 5 | mpan 690 | . . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) |
| 7 | 2, 6 | anim12i 613 | . . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
| 8 | 7 | an32s 652 | . . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
| 9 | 1, 8 | sylanb 581 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
| 10 | df-f 6565 | . 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) | |
| 11 | 9, 10 | sylibr 234 | 1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3951 ran crn 5686 ↾ cres 5687 Fn wfn 6556 ⟶wf 6557 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-fun 6563 df-fn 6564 df-f 6565 |
| This theorem is referenced by: fssresd 6775 fssres2 6776 fresin 6777 fresaun 6779 f1ssres 6811 resf1extb 7956 resf1ext2b 7957 f2ndf 8145 elmapssres 8907 pmresg 8910 ralxpmap 8936 mapunen 9186 fofinf1o 9372 fseqenlem1 10064 inar1 10815 gruima 10842 addnqf 10988 mulnqf 10989 fseq1p1m1 13638 injresinj 13827 seqf1olem2 14083 wrdred1 14598 rlimres 15594 lo1res 15595 vdwnnlem1 17033 fsets 17206 resmgmhm 18724 resmhm 18833 resghm 19250 gsumzres 19927 gsumzadd 19940 gsum2dlem2 19989 dpjidcl 20078 ablfac1eu 20093 abvres 20832 znf1o 21570 islindf4 21858 kgencn 23564 ptrescn 23647 hmeores 23779 tsmsres 24152 tsmsmhm 24154 tsmsadd 24155 xrge0gsumle 24855 xrge0tsms 24856 ovolicc2lem4 25555 limcdif 25911 limcflf 25916 limcmo 25917 dvres 25946 dvres3a 25949 aannenlem1 26370 logcn 26689 dvlog 26693 dvlog2 26695 logtayl 26702 dvatan 26978 atancn 26979 efrlim 27012 efrlimOLD 27013 amgm 27034 dchrelbas2 27281 redwlklem 29689 pthdivtx 29747 hhssabloilem 31280 hhssnv 31283 wrdres 32919 gsumpart 33060 xrge0tsmsd 33065 cntmeas 34227 eulerpartlemt 34373 eulerpartlemmf 34377 eulerpartlemgvv 34378 subiwrd 34387 sseqp1 34397 poimirlem4 37631 mbfresfi 37673 mbfposadd 37674 itg2gt0cn 37682 sdclem2 37749 mzpcompact2lem 42762 eldiophb 42768 eldioph2 42773 cncfiooicclem1 45908 fouriersw 46246 sge0tsms 46395 psmeasure 46486 sssmf 46753 lindslinindimp2lem2 48376 |
| Copyright terms: Public domain | W3C validator |