# Metamath Proof Explorer

## 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* = x ∈ V ⟼ ⋂ z | I ↾ dom ⁡ x ∪ ran ⁡ x ⊆ z ∧ x ⊆ z ∧ z ∘ z ⊆ z$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 crtcl $class t*$
1 vx $setvar x$
2 cvv $class V$
3 vz $setvar z$
4 cid $class I$
5 1 cv $setvar x$
6 5 cdm $class dom ⁡ x$
7 5 crn $class ran ⁡ x$
8 6 7 cun $class dom ⁡ x ∪ ran ⁡ x$
9 4 8 cres $class I ↾ dom ⁡ x ∪ ran ⁡ x$
10 3 cv $setvar z$
11 9 10 wss $wff I ↾ dom ⁡ x ∪ ran ⁡ x ⊆ z$
12 5 10 wss $wff x ⊆ z$
13 10 10 ccom $class z ∘ z$
14 13 10 wss $wff z ∘ z ⊆ z$
15 11 12 14 w3a $wff I ↾ dom ⁡ x ∪ ran ⁡ x ⊆ z ∧ x ⊆ z ∧ z ∘ z ⊆ z$
16 15 3 cab $class z | I ↾ dom ⁡ x ∪ ran ⁡ x ⊆ z ∧ x ⊆ z ∧ z ∘ z ⊆ z$
17 16 cint $class ⋂ z | I ↾ dom ⁡ x ∪ ran ⁡ x ⊆ z ∧ x ⊆ z ∧ z ∘ z ⊆ z$
18 1 2 17 cmpt $class x ∈ V ⟼ ⋂ z | I ↾ dom ⁡ x ∪ ran ⁡ x ⊆ z ∧ x ⊆ z ∧ z ∘ z ⊆ z$
19 0 18 wceq $wff t* = x ∈ V ⟼ ⋂ z | I ↾ dom ⁡ x ∪ ran ⁡ x ⊆ z ∧ x ⊆ z ∧ z ∘ z ⊆ z$