Theorem fvrcllb0da

Description: A restriction of the identity relation is a subset of the reflexive closure of a relation. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypotheses	fvrcllb0da.rel	$$⊢\phi \to \mathrm{Rel}R$$
	fvrcllb0da.r	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	fvrcllb0da	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{r*}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvrcllb0da.rel	$$⊢\phi \to \mathrm{Rel}R$$
2		fvrcllb0da.r	$$⊢\phi \to R\in \mathrm{V}$$
3		dfrcl4	$$⊢\mathrm{r*}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \left\{0,1\right\}}\left(r{\uparrow }_{r}n\right)\right)$$
4		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to \left\{0,1\right\}\in \mathrm{V}$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7	6	prid1	$$⊢0\in \left\{0,1\right\}$$
8	7	a1i	$$⊢\phi \to 0\in \left\{0,1\right\}$$
9	3 2 5 1 8	fvmptiunrelexplb0da	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{r*}\left(R\right)$$