This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1ococnv1

Description: The composition of a one-to-one onto function's converse and itself equals the identity relation restricted to the function's domain. (Contributed by NM, 13-Dec-2003)

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

Proof

Step Hyp Ref Expression
1 f1orel 
 |-  ( F : A -1-1-onto-> B -> Rel F )
2 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
3 1 2 sylib 
 |-  ( F : A -1-1-onto-> B -> `' `' F = F )
4 3 coeq2d 
 |-  ( F : A -1-1-onto-> B -> ( `' F o. `' `' F ) = ( `' F o. F ) )
5 f1ocnv 
 |-  ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
6 f1ococnv2 
 |-  ( `' F : B -1-1-onto-> A -> ( `' F o. `' `' F ) = ( _I |` A ) )
7 5 6 syl 
 |-  ( F : A -1-1-onto-> B -> ( `' F o. `' `' F ) = ( _I |` A ) )
8 4 7 eqtr3d 
 |-  ( F : A -1-1-onto-> B -> ( `' F o. F ) = ( _I |` A ) )