Theorem tcidm

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

	Ref	Expression
Assertion	tcidm	|- ( TC ` ( TC ` A ) ) = ( TC ` A )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- ( TC ` A ) C_ ( TC ` A )
2		tctr	|- Tr ( TC ` A )
3		fvex	|- ( TC ` A ) e. _V
4		tcmin	|- ( ( TC ` A ) e. _V -> ( ( ( TC ` A ) C_ ( TC ` A ) /\ Tr ( TC ` A ) ) -> ( TC ` ( TC ` A ) ) C_ ( TC ` A ) ) )
5	3 4	ax-mp	|- ( ( ( TC ` A ) C_ ( TC ` A ) /\ Tr ( TC ` A ) ) -> ( TC ` ( TC ` A ) ) C_ ( TC ` A ) )
6	1 2 5	mp2an	|- ( TC ` ( TC ` A ) ) C_ ( TC ` A )
7		tcid	|- ( ( TC ` A ) e. _V -> ( TC ` A ) C_ ( TC ` ( TC ` A ) ) )
8	3 7	ax-mp	|- ( TC ` A ) C_ ( TC ` ( TC ` A ) )
9	6 8	eqssi	|- ( TC ` ( TC ` A ) ) = ( TC ` A )