Theorem trclfvdecoml

Description: The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		trclfvdecomr	$$⊢R\in V\to \mathrm{t+}\left(R\right)=R\cup \left(\mathrm{t+}\left(R\right)\circ R\right)$$
2		trclfvcom	$$⊢R\in V\to \mathrm{t+}\left(R\right)\circ R=R\circ \mathrm{t+}\left(R\right)$$
3	2	uneq2d	$$⊢R\in V\to R\cup \left(\mathrm{t+}\left(R\right)\circ R\right)=R\cup \left(R\circ \mathrm{t+}\left(R\right)\right)$$
4	1 3	eqtrd	$$⊢R\in V\to \mathrm{t+}\left(R\right)=R\cup \left(R\circ \mathrm{t+}\left(R\right)\right)$$