# 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
`|- ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )`

### Proof

Step Hyp Ref Expression
1 df-f
` |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )`
2 fnssres
` |-  ( ( F Fn A /\ C C_ A ) -> ( F |` C ) Fn C )`
3 resss
` |-  ( F |` C ) C_ F`
4 3 rnssi
` |-  ran ( F |` C ) C_ ran F`
5 sstr
` |-  ( ( ran ( F |` C ) C_ ran F /\ ran F C_ B ) -> ran ( F |` C ) C_ B )`
6 4 5 mpan
` |-  ( ran F C_ B -> ran ( F |` C ) C_ B )`
7 2 6 anim12i
` |-  ( ( ( F Fn A /\ C C_ A ) /\ ran F C_ B ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )`
8 7 an32s
` |-  ( ( ( F Fn A /\ ran F C_ B ) /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )`
9 1 8 sylanb
` |-  ( ( F : A --> B /\ C C_ A ) -> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )`
10 df-f
` |-  ( ( F |` C ) : C --> B <-> ( ( F |` C ) Fn C /\ ran ( F |` C ) C_ B ) )`
11 9 10 sylibr
` |-  ( ( F : A --> B /\ C C_ A ) -> ( F |` C ) : C --> B )`