Definition df-rtrcl 13727

Description: Reflexive-transitive closure of a relation. This is the smallest superset which is reflexive property over all elements of its domain and range and has the transitive property. (Contributed by FL, 27-Jun-2011.)

Assertion

Ref	Expression
df-rtrcl	|- t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )

Distinct variable group:   x, z

Detailed syntax breakdown of Definition df-rtrcl

Step	Hyp	Ref	Expression
1		crtcl 13725	. 2 class t*
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		cid 5023	. . . . . . . 8 class _I
5	2	cv 1482	. . . . . . . . . 10 class x
6	5	cdm 5114	. . . . . . . . 9 class dom x
7	5	crn 5115	. . . . . . . . 9 class ran x
8	6, 7	cun 3572	. . . . . . . 8 class ( dom x u. ran x )
9	4, 8	cres 5116	. . . . . . 7 class ( _I |` ( dom x u. ran x ) )
10		vz	. . . . . . . 8 setvar z
11	10	cv 1482	. . . . . . 7 class z
12	9, 11	wss 3574	. . . . . 6 wff ( _I |` ( dom x u. ran x ) ) C_ z
13	5, 11	wss 3574	. . . . . 6 wff x C_ z
14	11, 11	ccom 5118	. . . . . . 7 class ( z o. z )
15	14, 11	wss 3574	. . . . . 6 wff ( z o. z ) C_ z
16	12, 13, 15	w3a 1037	. . . . 5 wff ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z )
17	16, 10	cab 2608	. . . 4 class { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) }
18	17	cint 4475	. . 3 class |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) }
19	2, 3, 18	cmpt 4729	. 2 class ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )
20	1, 19	wceq 1483	1 wff t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )

This definition is referenced by:  dfrtrcl2  13802  dfrtrcl5  37936  dfrtrcl3  38025