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	syl5eq	|- ( Rel R -> ( ( _I |` U. U. R ) o. R ) = R )