Metamath Proof Explorer

Theorem f1cocnv2

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

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

Proof

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