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 )