Metamath Proof Explorer


Theorem trclidm

Description: The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020)

Ref Expression
Assertion trclidm R V t+ t+ R = t+ R

Proof

Step Hyp Ref Expression
1 fvex t+ R V
2 trclfvcotr R V t+ R t+ R t+ R
3 cotrtrclfv t+ R V t+ R t+ R t+ R t+ t+ R = t+ R
4 1 2 3 sylancr R V t+ t+ R = t+ R