Metamath Proof Explorer

Theorem f1ores

Description: The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998)

Ref Expression
Assertion f1ores 
|- ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )

Proof

Step Hyp Ref Expression
1 f1ssres 
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-> B )
2 f1f1orn 
 |-  ( ( F |` C ) : C -1-1-> B -> ( F |` C ) : C -1-1-onto-> ran ( F |` C ) )
3 1 2 syl 
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ran ( F |` C ) )
4 df-ima 
 |-  ( F " C ) = ran ( F |` C )
5 f1oeq3 
 |-  ( ( F " C ) = ran ( F |` C ) -> ( ( F |` C ) : C -1-1-onto-> ( F " C ) <-> ( F |` C ) : C -1-1-onto-> ran ( F |` C ) ) )
6 4 5 ax-mp 
 |-  ( ( F |` C ) : C -1-1-onto-> ( F " C ) <-> ( F |` C ) : C -1-1-onto-> ran ( F |` C ) )
7 3 6 sylibr 
 |-  ( ( F : A -1-1-> B /\ C C_ A ) -> ( F |` C ) : C -1-1-onto-> ( F " C ) )