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