Metamath Proof Explorer

Theorem f1ss

Description: A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
2 fss 
 |-  ( ( F : A --> B /\ B C_ C ) -> F : A --> C )
3 1 2 sylan 
 |-  ( ( F : A -1-1-> B /\ B C_ C ) -> F : A --> C )
4 df-f1 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
5 4 simprbi 
 |-  ( F : A -1-1-> B -> Fun `' F )
6 5 adantr 
 |-  ( ( F : A -1-1-> B /\ B C_ C ) -> Fun `' F )
7 df-f1 
 |-  ( F : A -1-1-> C <-> ( F : A --> C /\ Fun `' F ) )
8 3 6 7 sylanbrc 
 |-  ( ( F : A -1-1-> B /\ B C_ C ) -> F : A -1-1-> C )