Metamath Proof Explorer


Theorem funcocnv2

Description: Composition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009)

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 dfdm4
 |-  dom F = ran `' F
5 dmcoeq
 |-  ( dom F = ran `' F -> dom ( F o. `' F ) = dom `' F )
6 4 5 ax-mp
 |-  dom ( F o. `' F ) = dom `' F
7 df-rn
 |-  ran F = dom `' F
8 6 7 eqtr4i
 |-  dom ( F o. `' F ) = ran F
9 8 reseq2i
 |-  ( _I |` dom ( F o. `' F ) ) = ( _I |` ran F )
10 9 eqeq2i
 |-  ( ( F o. `' F ) = ( _I |` dom ( F o. `' F ) ) <-> ( F o. `' F ) = ( _I |` ran F ) )
11 3 10 bitri
 |-  ( ( F o. `' F ) C_ _I <-> ( F o. `' F ) = ( _I |` ran F ) )
12 2 11 sylib
 |-  ( Fun F -> ( F o. `' F ) = ( _I |` ran F ) )