Metamath Proof Explorer

Theorem f1cocnv1

Description: Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011)

Ref Expression
Assertion f1cocnv1 
|- ( F : A -1-1-> B -> ( `' F o. F ) = ( _I |` A ) )

Proof

Step Hyp Ref Expression
1 f1f1orn 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
2 f1ococnv1 
 |-  ( F : A -1-1-onto-> ran F -> ( `' F o. F ) = ( _I |` A ) )
3 1 2 syl 
 |-  ( F : A -1-1-> B -> ( `' F o. F ) = ( _I |` A ) )