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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crcl	⊢ r*
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vz	⊢ 𝑧
4	1	cv	⊢ 𝑥
5	3	cv	⊢ 𝑧
6	4 5	wss	⊢ 𝑥 ⊆ 𝑧
7		cid	⊢ I
8	5	cdm	⊢ dom 𝑧
9	5	crn	⊢ ran 𝑧
10	8 9	cun	⊢ ( dom 𝑧 ∪ ran 𝑧 )
11	7 10	cres	⊢ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) )
12	11 5	wss	⊢ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧
13	6 12	wa	⊢ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 )
14	13 3	cab	⊢ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) }
15	14	cint	⊢ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) }
16	1 2 15	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } )
17	0 16	wceq	⊢ r* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } )