Theorem trclfvlb3

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

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

Proof

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