Theorem relexp0d

Description: A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	relexp0d.1	$$⊢\phi \to \mathrm{Rel}R$$
	relexp0d.2	$$⊢\phi \to R\in V$$
Assertion	relexp0d	$$⊢\phi \to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$

Proof

Step	Hyp	Ref	Expression
1		relexp0d.1	$$⊢\phi \to \mathrm{Rel}R$$
2		relexp0d.2	$$⊢\phi \to R\in V$$
3		relexp0	$$⊢\left(R\in V\wedge \mathrm{Rel}R\right)\to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$
4	2 1 3	syl2anc	$$⊢\phi \to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$