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 e. V -> ( t+ ` R ) = ( R u. ( R o. ( t+ ` R ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		trclfvdecomr	|- ( R e. V -> ( t+ ` R ) = ( R u. ( ( t+ ` R ) o. R ) ) )
2		trclfvcom	|- ( R e. V -> ( ( t+ ` R ) o. R ) = ( R o. ( t+ ` R ) ) )
3	2	uneq2d	|- ( R e. V -> ( R u. ( ( t+ ` R ) o. R ) ) = ( R u. ( R o. ( t+ ` R ) ) ) )
4	1 3	eqtrd	|- ( R e. V -> ( t+ ` R ) = ( R u. ( R o. ( t+ ` R ) ) ) )