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 5808 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | fnssres 5918 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶) | |
3 | resss 5342 | . . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹 | |
4 | rnss 5275 | . . . . . . 7 ⊢ ((𝐹 ↾ 𝐶) ⊆ 𝐹 → ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹) | |
5 | 3, 4 | ax-mp 5 | . . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 |
6 | sstr 3576 | . . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) | |
7 | 5, 6 | mpan 702 | . . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵) |
8 | 2, 7 | anim12i 588 | . . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
9 | 8 | an32s 842 | . . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
10 | 1, 9 | sylanb 488 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) |
11 | df-f 5808 | . 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵)) | |
12 | 10, 11 | sylibr 223 | 1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊆ wss 3540 ran crn 5039 ↾ cres 5040 Fn wfn 5799 ⟶wf 5800 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-fun 5806 df-fn 5807 df-f 5808 |
This theorem is referenced by: fssresd 5984 fssres2 5985 fresin 5986 fresaun 5988 f1ssres 6021 f2ndf 7170 elmapssres 7768 pmresg 7771 ralxpmap 7793 mapunen 8014 fofinf1o 8126 fseqenlem1 8730 inar1 9476 gruima 9503 addnqf 9649 mulnqf 9650 fseq1p1m1 12283 injresinj 12451 seqf1olem2 12703 rlimres 14137 lo1res 14138 vdwnnlem1 15537 fsets 15723 resmhm 17182 resghm 17499 gsumzres 18133 gsumzadd 18145 gsum2dlem2 18193 dpjidcl 18280 ablfac1eu 18295 abvres 18662 znf1o 19719 islindf4 19996 kgencn 21169 ptrescn 21252 hmeores 21384 tsmsres 21757 tsmsmhm 21759 tsmsadd 21760 xrge0gsumle 22444 xrge0tsms 22445 ovolicc2lem4 23095 limcdif 23446 limcflf 23451 limcmo 23452 dvres 23481 dvres3a 23484 aannenlem1 23887 logcn 24193 dvlog 24197 dvlog2 24199 logtayl 24206 dvatan 24462 atancn 24463 efrlim 24496 amgm 24517 dchrelbas2 24762 redwlk 26136 hhssabloilem 27502 hhssnv 27505 xrge0tsmsd 29116 cntmeas 29616 eulerpartlemt 29760 eulerpartlemmf 29764 eulerpartlemgvv 29765 subiwrd 29774 sseqp1 29784 wrdres 29943 poimirlem4 32583 mbfresfi 32626 mbfposadd 32627 itg2gt0cn 32635 sdclem2 32708 mzpcompact2lem 36332 eldiophb 36338 eldioph2 36343 cncfiooicclem1 38779 fouriersw 39124 sge0tsms 39273 psmeasure 39364 sssmf 39625 wrdred1 40240 red1wlklem 40880 pthdivtx 40935 resmgmhm 41588 lindslinindimp2lem2 42042 |
Copyright terms: Public domain | W3C validator |