Theorem fvtrcllb1d

Description: A set is a subset of its image under the transitive closure. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypothesis	fvtrcllb1d.r	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	fvtrcllb1d	$$⊢\phi \to R\subseteq \mathrm{t+}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvtrcllb1d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		dftrcl3	$$⊢\mathrm{t+}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \mathbb{N}}\left(r{\uparrow }_{r}n\right)\right)$$
3		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
4	3	a1i	$$⊢\phi \to \mathbb{N}\in \mathrm{V}$$
5		1nn	$$⊢1\in \mathbb{N}$$
6	5	a1i	$$⊢\phi \to 1\in \mathbb{N}$$
7	2 1 4 6	fvmptiunrelexplb1d	$$⊢\phi \to R\subseteq \mathrm{t+}\left(R\right)$$