Definition df-tc 8613

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

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-tc

Step	Hyp	Ref	Expression
1		ctc 8612	. 2 class TC
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . . 7 class x
5		vy	. . . . . . . 8 setvar y
6	5	cv 1482	. . . . . . 7 class y
7	4, 6	wss 3574	. . . . . 6 wff x C_ y
8	6	wtr 4752	. . . . . 6 wff Tr y
9	7, 8	wa 384	. . . . 5 wff ( x C_ y /\ Tr y )
10	9, 5	cab 2608	. . . 4 class { y | ( x C_ y /\ Tr y ) }
11	10	cint 4475	. . 3 class |^| { y | ( x C_ y /\ Tr y ) }
12	2, 3, 11	cmpt 4729	. 2 class ( x e. _V |-> |^| { y | ( x C_ y /\ Tr y ) } )
13	1, 12	wceq 1483	1 wff TC = ( x e. _V |-> |^| { y | ( x C_ y /\ Tr y ) } )

This definition is referenced by:  tcvalg  8614