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 ‘ 𝐴 )