This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tcidm

Description: The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tcidm ( TC ‘ ( TC ‘ 𝐴 ) ) = ( TC ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 ssid ⊢ ( TC ‘ 𝐴 ) ⊆ ( TC ‘ 𝐴 )
2 tctr ⊢ Tr ( TC ‘ 𝐴 )
3 fvex ⊢ ( TC ‘ 𝐴 ) ∈ V
4 tcmin ⊢ ( ( TC ‘ 𝐴 ) ∈ V → ( ( ( TC ‘ 𝐴 ) ⊆ ( TC ‘ 𝐴 ) ∧ Tr ( TC ‘ 𝐴 ) ) → ( TC ‘ ( TC ‘ 𝐴 ) ) ⊆ ( TC ‘ 𝐴 ) ) )
5 3 4 ax-mp ⊢ ( ( ( TC ‘ 𝐴 ) ⊆ ( TC ‘ 𝐴 ) ∧ Tr ( TC ‘ 𝐴 ) ) → ( TC ‘ ( TC ‘ 𝐴 ) ) ⊆ ( TC ‘ 𝐴 ) )
6 1 2 5 mp2an ⊢ ( TC ‘ ( TC ‘ 𝐴 ) ) ⊆ ( TC ‘ 𝐴 )
7 tcid ⊢ ( ( TC ‘ 𝐴 ) ∈ V → ( TC ‘ 𝐴 ) ⊆ ( TC ‘ ( TC ‘ 𝐴 ) ) )
8 3 7 ax-mp ⊢ ( TC ‘ 𝐴 ) ⊆ ( TC ‘ ( TC ‘ 𝐴 ) )
9 6 8 eqssi ⊢ ( TC ‘ ( TC ‘ 𝐴 ) ) = ( TC ‘ 𝐴 )