Definition df-rtrcl

Description: Reflexive-transitive closure of a relation. This is the smallest superset which is reflexive property over all elements of its domain and range and has the transitive property. (Contributed by FL, 27-Jun-2011)

	Ref	Expression
Assertion	df-rtrcl	⊢ t* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )

Detailed syntax breakdown

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