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 ) )