Metamath Proof Explorer

Theorem ttcidm

Description: The transitive closure operation is idempotent. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttcidm 
|- TC+ TC+ A = TC+ A

Proof

Step Hyp Ref Expression
1 ttctr 
 |-  Tr TC+ A
2 ttctrid 
 |-  ( Tr TC+ A -> TC+ TC+ A = TC+ A )
3 1 2 ax-mp 
 |-  TC+ TC+ A = TC+ A