Theorem fvrtrcllb0da

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

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

Proof

Step	Hyp	Ref	Expression
1		fvrtrcllb0da.rel	$$⊢\phi \to \mathrm{Rel}R$$
2		fvrtrcllb0da.r	$$⊢\phi \to R\in \mathrm{V}$$
3		dfrtrcl3	$$⊢\mathrm{t*}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)$$
4		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
6		0nn0	$$⊢0\in {\mathbb{N}}_0$$
7	6	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
8	3 2 5 1 7	fvmptiunrelexplb0da	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{t*}\left(R\right)$$