Definition df-trcl

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctcl	|- t+
1		vx	|- x
2		cvv	|- _V
3		vz	|- z
4	1	cv	|- x
5	3	cv	|- z
6	4 5	wss	|- x C_ z
7	5 5	ccom	|- ( z o. z )
8	7 5	wss	|- ( z o. z ) C_ z
9	6 8	wa	|- ( x C_ z /\ ( z o. z ) C_ z )
10	9 3	cab	|- { z | ( x C_ z /\ ( z o. z ) C_ z ) }
11	10	cint	|- |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) }
12	1 2 11	cmpt	|- ( x e. _V |-> |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) } )
13	0 12	wceq	|- t+ = ( x e. _V |-> |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) } )