Theorem relcoi2

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

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

Proof

Step	Hyp	Ref	Expression
1		dmrnssfld	$$⊢\mathrm{dom}R\cup \mathrm{ran}R\subseteq \bigcup \bigcup R$$
2		unss	$$⊢\left(\mathrm{dom}R\subseteq \bigcup \bigcup R\wedge \mathrm{ran}R\subseteq \bigcup \bigcup R\right)\leftrightarrow \mathrm{dom}R\cup \mathrm{ran}R\subseteq \bigcup \bigcup R$$
3		simpr	$$⊢\left(\mathrm{dom}R\subseteq \bigcup \bigcup R\wedge \mathrm{ran}R\subseteq \bigcup \bigcup R\right)\to \mathrm{ran}R\subseteq \bigcup \bigcup R$$
4	2 3	sylbir	$$⊢\mathrm{dom}R\cup \mathrm{ran}R\subseteq \bigcup \bigcup R\to \mathrm{ran}R\subseteq \bigcup \bigcup R$$
5		cores	$$⊢\mathrm{ran}R\subseteq \bigcup \bigcup R\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)\circ R=\mathrm{I}\circ R$$
6	1 4 5	mp2b	$$⊢\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)\circ R=\mathrm{I}\circ R$$
7		coi2	$$⊢\mathrm{Rel}R\to \mathrm{I}\circ R=R$$
8	6 7	syl5eq	$$⊢\mathrm{Rel}R\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\right)\circ R=R$$