Metamath Proof Explorer

Theorem tctr

Description: Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tctr 
|- Tr ( TC ` A )

Proof

Step Hyp Ref Expression
1 trint 
 |-  ( A. y e. { x | ( A C_ x /\ Tr x ) } Tr y -> Tr |^| { x | ( A C_ x /\ Tr x ) } )
2 vex 
 |-  y e. _V
3 sseq2 
 |-  ( x = y -> ( A C_ x <-> A C_ y ) )
4 treq 
 |-  ( x = y -> ( Tr x <-> Tr y ) )
5 3 4 anbi12d 
 |-  ( x = y -> ( ( A C_ x /\ Tr x ) <-> ( A C_ y /\ Tr y ) ) )
6 2 5 elab 
 |-  ( y e. { x | ( A C_ x /\ Tr x ) } <-> ( A C_ y /\ Tr y ) )
7 6 simprbi 
 |-  ( y e. { x | ( A C_ x /\ Tr x ) } -> Tr y )
8 1 7 mprg 
 |-  Tr |^| { x | ( A C_ x /\ Tr x ) }
9 tcvalg 
 |-  ( A e. _V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
10 treq 
 |-  ( ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } -> ( Tr ( TC ` A ) <-> Tr |^| { x | ( A C_ x /\ Tr x ) } ) )
11 9 10 syl 
 |-  ( A e. _V -> ( Tr ( TC ` A ) <-> Tr |^| { x | ( A C_ x /\ Tr x ) } ) )
12 8 11 mpbiri 
 |-  ( A e. _V -> Tr ( TC ` A ) )
13 tr0 
 |-  Tr (/)
14 fvprc 
 |-  ( -. A e. _V -> ( TC ` A ) = (/) )
15 treq 
 |-  ( ( TC ` A ) = (/) -> ( Tr ( TC ` A ) <-> Tr (/) ) )
16 14 15 syl 
 |-  ( -. A e. _V -> ( Tr ( TC ` A ) <-> Tr (/) ) )
17 13 16 mpbiri 
 |-  ( -. A e. _V -> Tr ( TC ` A ) )
18 12 17 pm2.61i 
 |-  Tr ( TC ` A )