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

Metamath Proof Explorer

Theorem tcvalg

Description: Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf ; see tz9.1 .) (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tcvalg 
|- ( A e. V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( y = A -> ( TC ` y ) = ( TC ` A ) )
2 sseq1 
 |-  ( y = A -> ( y C_ x <-> A C_ x ) )
3 2 anbi1d 
 |-  ( y = A -> ( ( y C_ x /\ Tr x ) <-> ( A C_ x /\ Tr x ) ) )
4 3 abbidv 
 |-  ( y = A -> { x | ( y C_ x /\ Tr x ) } = { x | ( A C_ x /\ Tr x ) } )
5 4 inteqd 
 |-  ( y = A -> |^| { x | ( y C_ x /\ Tr x ) } = |^| { x | ( A C_ x /\ Tr x ) } )
6 1 5 eqeq12d 
 |-  ( y = A -> ( ( TC ` y ) = |^| { x | ( y C_ x /\ Tr x ) } <-> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } ) )
7 vex 
 |-  y e. _V
8 7 tz9.1c 
 |-  |^| { x | ( y C_ x /\ Tr x ) } e. _V
9 df-tc 
 |-  TC = ( y e. _V |-> |^| { x | ( y C_ x /\ Tr x ) } )
10 9 fvmpt2 
 |-  ( ( y e. _V /\ |^| { x | ( y C_ x /\ Tr x ) } e. _V ) -> ( TC ` y ) = |^| { x | ( y C_ x /\ Tr x ) } )
11 7 8 10 mp2an 
 |-  ( TC ` y ) = |^| { x | ( y C_ x /\ Tr x ) }
12 6 11 vtoclg 
 |-  ( A e. V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )