Theorem fvrcllb0d

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

	Ref	Expression
Hypothesis	fvrcllb0d.r	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	fvrcllb0d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\subseteq \mathrm{r*}\left(R\right)$$

Proof

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