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 ` 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 )