Definition df-tc

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

	Ref	Expression
Assertion	df-tc	|- TC = ( x e. _V |-> |^| { y | ( x C_ y /\ Tr y ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctc	|- TC
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4	1	cv	|- x
5	3	cv	|- y
6	4 5	wss	|- x C_ y
7	5	wtr	|- Tr y
8	6 7	wa	|- ( x C_ y /\ Tr y )
9	8 3	cab	|- { y | ( x C_ y /\ Tr y ) }
10	9	cint	|- |^| { y | ( x C_ y /\ Tr y ) }
11	1 2 10	cmpt	|- ( x e. _V |-> |^| { y | ( x C_ y /\ Tr y ) } )
12	0 11	wceq	|- TC = ( x e. _V |-> |^| { y | ( x C_ y /\ Tr y ) } )