Metamath Proof Explorer

Theorem f1ssr

Description: A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Stefan O'Rear, 20-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 f1fn 
 |-  ( F : A -1-1-> B -> F Fn A )
2 1 adantr 
 |-  ( ( F : A -1-1-> B /\ ran F C_ C ) -> F Fn A )
3 simpr 
 |-  ( ( F : A -1-1-> B /\ ran F C_ C ) -> ran F C_ C )
4 df-f 
 |-  ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
5 2 3 4 sylanbrc 
 |-  ( ( F : A -1-1-> B /\ ran F C_ C ) -> F : A --> C )
6 df-f1 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
7 6 simprbi 
 |-  ( F : A -1-1-> B -> Fun `' F )
8 7 adantr 
 |-  ( ( F : A -1-1-> B /\ ran F C_ C ) -> Fun `' F )
9 df-f1 
 |-  ( F : A -1-1-> C <-> ( F : A --> C /\ Fun `' F ) )
10 5 8 9 sylanbrc 
 |-  ( ( F : A -1-1-> B /\ ran F C_ C ) -> F : A -1-1-> C )