Theorem trclidm

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

	Ref	Expression
Assertion	trclidm	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ ( t+ ‘ 𝑅 ) ) = ( t+ ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( t+ ‘ 𝑅 ) ∈ V
2		trclfvcotr	⊢ ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
3		cotrtrclfv	⊢ ( ( ( t+ ‘ 𝑅 ) ∈ V ∧ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) ) → ( t+ ‘ ( t+ ‘ 𝑅 ) ) = ( t+ ‘ 𝑅 ) )
4	1 2 3	sylancr	⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ ( t+ ‘ 𝑅 ) ) = ( t+ ‘ 𝑅 ) )