Definition df-rcl

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crcl	|- r*
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		cid	|- _I
8	5	cdm	|- dom z
9	5	crn	|- ran z
10	8 9	cun	|- ( dom z u. ran z )
11	7 10	cres	|- ( _I |` ( dom z u. ran z ) )
12	11 5	wss	|- ( _I |` ( dom z u. ran z ) ) C_ z
13	6 12	wa	|- ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z )
14	13 3	cab	|- { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) }
15	14	cint	|- |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) }
16	1 2 15	cmpt	|- ( x e. _V |-> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )
17	0 16	wceq	|- r* = ( x e. _V |-> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )