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