Theorem trclfvlb2

Description: The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020)

	Ref	Expression
Assertion	trclfvlb2	$$⊢R\in V\to R\circ R\subseteq \mathrm{t+}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		trclfvcotr	$$⊢R\in V\to \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
2		trclfvlb	$$⊢R\in V\to R\subseteq \mathrm{t+}\left(R\right)$$
3	1 2 2	trrelssd	$$⊢R\in V\to R\circ R\subseteq \mathrm{t+}\left(R\right)$$