Metamath Proof Explorer

Theorem fss

Description: Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion fss 
|- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )

Proof

Step Hyp Ref Expression
1 sstr2 
 |-  ( ran F C_ B -> ( B C_ C -> ran F C_ C ) )
2 1 com12 
 |-  ( B C_ C -> ( ran F C_ B -> ran F C_ C ) )
3 2 anim2d 
 |-  ( B C_ C -> ( ( F Fn A /\ ran F C_ B ) -> ( F Fn A /\ ran F C_ C ) ) )
4 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5 df-f 
 |-  ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
6 3 4 5 3imtr4g 
 |-  ( B C_ C -> ( F : A --> B -> F : A --> C ) )
7 6 impcom 
 |-  ( ( F : A --> B /\ B C_ C ) -> F : A --> C )