Theorem trclfvub

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

	Ref	Expression
Assertion	trclfvub	$$⊢R\in V\to \mathrm{t+}\left(R\right)\subseteq R\cup \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2		trclubg	$$⊢R\in V\to \bigcap \left\{r|\left(R\subseteq r\wedge r\circ r\subseteq r\right)\right\}\subseteq R\cup \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
3	1 2	eqsstrd	$$⊢R\in V\to \mathrm{t+}\left(R\right)\subseteq R\cup \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$