Definition df-trcl 13726

Description: Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011.)

Assertion

Ref	Expression
df-trcl	|- t+ = ( x e. _V |-> |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) } )

Distinct variable group:   x, z

Detailed syntax breakdown of Definition df-trcl

Step	Hyp	Ref	Expression
1		ctcl 13724	. 2 class t+
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . . 7 class x
5		vz	. . . . . . . 8 setvar z
6	5	cv 1482	. . . . . . 7 class z
7	4, 6	wss 3574	. . . . . 6 wff x C_ z
8	6, 6	ccom 5118	. . . . . . 7 class ( z o. z )
9	8, 6	wss 3574	. . . . . 6 wff ( z o. z ) C_ z
10	7, 9	wa 384	. . . . 5 wff ( x C_ z /\ ( z o. z ) C_ z )
11	10, 5	cab 2608	. . . 4 class { z | ( x C_ z /\ ( z o. z ) C_ z ) }
12	11	cint 4475	. . 3 class |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) }
13	2, 3, 12	cmpt 4729	. 2 class ( x e. _V |-> |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) } )
14	1, 13	wceq 1483	1 wff t+ = ( x e. _V |-> |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) } )

This definition is referenced by:  trclfv  13741  dftrcl3  38012