# Metamath Proof Explorer

## Theorem fssres

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004)

Ref Expression
Assertion fssres ${⊢}\left({F}:{A}⟶{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}⟶{B}$

### Proof

Step Hyp Ref Expression
1 df-f ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)$
2 fnssres ${⊢}\left({F}Fn{A}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right)Fn{C}$
3 resss ${⊢}{{F}↾}_{{C}}\subseteq {F}$
4 3 rnssi ${⊢}\mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq \mathrm{ran}{F}$
5 sstr ${⊢}\left(\mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq \mathrm{ran}{F}\wedge \mathrm{ran}{F}\subseteq {B}\right)\to \mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq {B}$
6 4 5 mpan ${⊢}\mathrm{ran}{F}\subseteq {B}\to \mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq {B}$
7 2 6 anim12i ${⊢}\left(\left({F}Fn{A}\wedge {C}\subseteq {A}\right)\wedge \mathrm{ran}{F}\subseteq {B}\right)\to \left(\left({{F}↾}_{{C}}\right)Fn{C}\wedge \mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq {B}\right)$
8 7 an32s ${⊢}\left(\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)\wedge {C}\subseteq {A}\right)\to \left(\left({{F}↾}_{{C}}\right)Fn{C}\wedge \mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq {B}\right)$
9 1 8 sylanb ${⊢}\left({F}:{A}⟶{B}\wedge {C}\subseteq {A}\right)\to \left(\left({{F}↾}_{{C}}\right)Fn{C}\wedge \mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq {B}\right)$
10 df-f ${⊢}\left({{F}↾}_{{C}}\right):{C}⟶{B}↔\left(\left({{F}↾}_{{C}}\right)Fn{C}\wedge \mathrm{ran}\left({{F}↾}_{{C}}\right)\subseteq {B}\right)$
11 9 10 sylibr ${⊢}\left({F}:{A}⟶{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}⟶{B}$