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	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ( 𝑅 ∪ ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		trclfvdecomr	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) )
2		trclfvcom	⊢ ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) )
3	2	uneq2d	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∪ ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) ) = ( 𝑅 ∪ ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) )
4	1 3	eqtrd	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ( 𝑅 ∪ ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) )