Theorem relcoi1

Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011) (Proof shortened by OpenAI, 3-Jul-2020)

	Ref	Expression
Assertion	relcoi1	$$⊢\mathrm{Rel}R\to R\circ \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)=R$$

Proof

Step	Hyp	Ref	Expression
1		coires1	$$⊢R\circ \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)={R\upharpoonright }_{\bigcup \bigcup R}$$
2		relresfld	$$⊢\mathrm{Rel}R\to {R\upharpoonright }_{\bigcup \bigcup R}=R$$
3	1 2	syl5eq	$$⊢\mathrm{Rel}R\to R\circ \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)=R$$