Theorem funcocnv2

Description: Precomposition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	funcocnv2	|- ( Fun F -> ( F o. `' F ) = ( _I |` ran F ) )

Proof

Step	Hyp	Ref	Expression
1		df-fun	|- ( Fun F <-> ( Rel F /\ ( F o. `' F ) C_ _I ) )
2	1	simprbi	|- ( Fun F -> ( F o. `' F ) C_ _I )
3		iss	|- ( ( F o. `' F ) C_ _I <-> ( F o. `' F ) = ( _I |` dom ( F o. `' F ) ) )
4	2 3	sylib	|- ( Fun F -> ( F o. `' F ) = ( _I |` dom ( F o. `' F ) ) )
5		dmcocnv2	|- dom ( F o. `' F ) = ran F
6	5	reseq2i	|- ( _I |` dom ( F o. `' F ) ) = ( _I |` ran F )
7	4 6	eqtrdi	|- ( Fun F -> ( F o. `' F ) = ( _I |` ran F ) )