Theorem trclidm

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

	Ref	Expression
Assertion	trclidm	|- ( R e. V -> ( t+ ` ( t+ ` R ) ) = ( t+ ` R ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( t+ ` R ) e. _V
2		trclfvcotr	|- ( R e. V -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )
3		cotrtrclfv	|- ( ( ( t+ ` R ) e. _V /\ ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) ) -> ( t+ ` ( t+ ` R ) ) = ( t+ ` R ) )
4	1 2 3	sylancr	|- ( R e. V -> ( t+ ` ( t+ ` R ) ) = ( t+ ` R ) )