Theorem relexp0

Description: A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020)

	Ref	Expression
Assertion	relexp0	$$⊢\left(R\in V\wedge \mathrm{Rel}R\right)\to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$

Proof

Step	Hyp	Ref	Expression
1		relexp0g	$$⊢R\in V\to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}$$
2		relfld	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\mathrm{dom}R\cup \mathrm{ran}R$$
3	2	reseq2d	$$⊢\mathrm{Rel}R\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}$$
4	3	eqcomd	$$⊢\mathrm{Rel}R\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$
5	1 4	sylan9eq	$$⊢\left(R\in V\wedge \mathrm{Rel}R\right)\to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$