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	$$⊢\mathrm{r*}=\left(x\in \mathrm{V}⟼\bigcap \left\{z|\left(x\subseteq z\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\subseteq z\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crcl	$$class\mathrm{r*}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vz	$$setvarz$$
4	1	cv	$$setvarx$$
5	3	cv	$$setvarz$$
6	4 5	wss	$$wffx\subseteq z$$
7		cid	$$class\mathrm{I}$$
8	5	cdm	$$class\mathrm{dom}z$$
9	5	crn	$$class\mathrm{ran}z$$
10	8 9	cun	$$class\left(\mathrm{dom}z\cup \mathrm{ran}z\right)$$
11	7 10	cres	$$class\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\right)$$
12	11 5	wss	$$wff{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\subseteq z$$
13	6 12	wa	$$wff\left(x\subseteq z\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\subseteq z\right)$$
14	13 3	cab	$$class\left\{z|\left(x\subseteq z\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\subseteq z\right)\right\}$$
15	14	cint	$$class\bigcap \left\{z|\left(x\subseteq z\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\subseteq z\right)\right\}$$
16	1 2 15	cmpt	$$class\left(x\in \mathrm{V}⟼\bigcap \left\{z|\left(x\subseteq z\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\subseteq z\right)\right\}\right)$$
17	0 16	wceq	$$wff\mathrm{r*}=\left(x\in \mathrm{V}⟼\bigcap \left\{z|\left(x\subseteq z\wedge {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}z\cup \mathrm{ran}z\right)}\subseteq z\right)\right\}\right)$$