Theorem trclfvlb

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

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

Proof

Step	Hyp	Ref	Expression
1		ssmin	$$⊢R\subseteq \bigcap \left\{r|\left(R\subseteq r\wedge r\circ r\subseteq r\right)\right\}$$
2		trclfv	$$⊢R\in V\to \mathrm{t+}\left(R\right)=\bigcap \left\{r|\left(R\subseteq r\wedge r\circ r\subseteq r\right)\right\}$$
3	1 2	sseqtrrid	$$⊢R\in V\to R\subseteq \mathrm{t+}\left(R\right)$$