Metamath Proof Explorer


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 RVt+R=RRt+R

Proof

Step Hyp Ref Expression
1 trclfvdecomr RVt+R=Rt+RR
2 trclfvcom RVt+RR=Rt+R
3 2 uneq2d RVRt+RR=RRt+R
4 1 3 eqtrd RVt+R=RRt+R