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