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

Metamath Proof Explorer

Theorem relcoi2

Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011)

Ref Expression
Assertion relcoi2 
|- ( Rel R -> ( ( _I |` U. U. R ) o. R ) = R )

Proof

Step Hyp Ref Expression
1 dmrnssfld 
 |-  ( dom R u. ran R ) C_ U. U. R
2 unss 
 |-  ( ( dom R C_ U. U. R /\ ran R C_ U. U. R ) <-> ( dom R u. ran R ) C_ U. U. R )
3 simpr 
 |-  ( ( dom R C_ U. U. R /\ ran R C_ U. U. R ) -> ran R C_ U. U. R )
4 2 3 sylbir 
 |-  ( ( dom R u. ran R ) C_ U. U. R -> ran R C_ U. U. R )
5 cores 
 |-  ( ran R C_ U. U. R -> ( ( _I |` U. U. R ) o. R ) = ( _I o. R ) )
6 1 4 5 mp2b 
 |-  ( ( _I |` U. U. R ) o. R ) = ( _I o. R )
7 coi2 
 |-  ( Rel R -> ( _I o. R ) = R )
8 6 7 eqtrid 
 |-  ( Rel R -> ( ( _I |` U. U. R ) o. R ) = R )