Metamath Proof Explorer


Theorem fococnv2

Description: The composition of an onto function and its converse. (Contributed by Stefan O'Rear, 12-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 fofun
 |-  ( F : A -onto-> B -> Fun F )
2 funcocnv2
 |-  ( Fun F -> ( F o. `' F ) = ( _I |` ran F ) )
3 1 2 syl
 |-  ( F : A -onto-> B -> ( F o. `' F ) = ( _I |` ran F ) )
4 forn
 |-  ( F : A -onto-> B -> ran F = B )
5 4 reseq2d
 |-  ( F : A -onto-> B -> ( _I |` ran F ) = ( _I |` B ) )
6 3 5 eqtrd
 |-  ( F : A -onto-> B -> ( F o. `' F ) = ( _I |` B ) )