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 e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crtcl 
 |-  t*
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vz 
 |-  z
4 cid 
 |-  _I
5 1 cv 
 |-  x
6 5 cdm 
 |-  dom x
7 5 crn 
 |-  ran x
8 6 7 cun 
 |-  ( dom x u. ran x )
9 4 8 cres 
 |-  ( _I |` ( dom x u. ran x ) )
10 3 cv 
 |-  z
11 9 10 wss 
 |-  ( _I |` ( dom x u. ran x ) ) C_ z
12 5 10 wss 
 |-  x C_ z
13 10 10 ccom 
 |-  ( z o. z )
14 13 10 wss 
 |-  ( z o. z ) C_ z
15 11 12 14 w3a 
 |-  ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z )
16 15 3 cab 
 |-  { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) }
17 16 cint 
 |-  |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) }
18 1 2 17 cmpt 
 |-  ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )
19 0 18 wceq 
 |-  t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )