Definition df-rcl 36984

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* = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)})

Distinct variable group:   𝑥,𝑧

Detailed syntax breakdown of Definition df-rcl

Step	Hyp	Ref	Expression
1		crcl 36983	. 2 class r*
2		vx	. . 3 setvar 𝑥
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . . . 7 class 𝑥
5		vz	. . . . . . . 8 setvar 𝑧
6	5	cv 1474	. . . . . . 7 class 𝑧
7	4, 6	wss 3540	. . . . . 6 wff 𝑥 ⊆ 𝑧
8		cid 4948	. . . . . . . 8 class I
9	6	cdm 5038	. . . . . . . . 9 class dom 𝑧
10	6	crn 5039	. . . . . . . . 9 class ran 𝑧
11	9, 10	cun 3538	. . . . . . . 8 class (dom 𝑧 ∪ ran 𝑧)
12	8, 11	cres 5040	. . . . . . 7 class ( I ↾ (dom 𝑧 ∪ ran 𝑧))
13	12, 6	wss 3540	. . . . . 6 wff ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧
14	7, 13	wa 383	. . . . 5 wff (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)
15	14, 5	cab 2596	. . . 4 class {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}
16	15	cint 4410	. . 3 class ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}
17	2, 3, 16	cmpt 4643	. 2 class (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)})
18	1, 17	wceq 1475	1 wff r* = (𝑥 ∈ V ↦ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)})

This definition is referenced by:  dfrcl2  36985