Metamath Proof Explorer

Theorem f1f1orn

Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004)

Ref Expression
Assertion f1f1orn 
|- ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )

Proof

Step Hyp Ref Expression
1 f1fn 
 |-  ( F : A -1-1-> B -> F Fn A )
2 df-f1 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
3 2 simprbi 
 |-  ( F : A -1-1-> B -> Fun `' F )
4 f1orn 
 |-  ( F : A -1-1-onto-> ran F <-> ( F Fn A /\ Fun `' F ) )
5 1 3 4 sylanbrc 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )