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 )