Definition df-rcl 37965

Description: Reflexive closure of a relation. This is the smallest superset which has the reflexive property. (Contributed by RP, 5-Jun-2020.)

Assertion

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

Distinct variable group:   x, z

Detailed syntax breakdown of Definition df-rcl

Step	Hyp	Ref	Expression
1		crcl 37964	. 2 class r*
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		cid 5023	. . . . . . . 8 class _I
9	6	cdm 5114	. . . . . . . . 9 class dom z
10	6	crn 5115	. . . . . . . . 9 class ran z
11	9, 10	cun 3572	. . . . . . . 8 class ( dom z u. ran z )
12	8, 11	cres 5116	. . . . . . 7 class ( _I |` ( dom z u. ran z ) )
13	12, 6	wss 3574	. . . . . 6 wff ( _I |` ( dom z u. ran z ) ) C_ z
14	7, 13	wa 384	. . . . 5 wff ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z )
15	14, 5	cab 2608	. . . 4 class { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) }
16	15	cint 4475	. . 3 class |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) }
17	2, 3, 16	cmpt 4729	. 2 class ( x e. _V |-> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )
18	1, 17	wceq 1483	1 wff r* = ( x e. _V |-> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )

This definition is referenced by:  dfrcl2  37966