MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rtrcl Unicode version

Definition df-rtrcl 20852
Description: Reflexive-transitive closure of a relation. Experimental. (Contributed by FL, 27-Jun-2011.)
Assertion
Ref Expression
df-rtrcl  |-  t
*  =  ( x  e.  _V  |->  |^| { z  |  ( (  _I  |`  ( dom  x  u. 
ran  x ) ) 
C_  z  /\  x  C_  z  /\  ( z  o.  z )  C_  z ) } )
Distinct variable group:    x, z

Detailed syntax breakdown of Definition df-rtrcl
StepHypRef Expression
1 crtcl 20850 . 2  class  t *
2 vx . . 3  set  x
3 cvv 2788 . . 3  class  _V
4 cid 4304 . . . . . . . 8  class  _I
52cv 1622 . . . . . . . . . 10  class  x
65cdm 4689 . . . . . . . . 9  class  dom  x
75crn 4690 . . . . . . . . 9  class  ran  x
86, 7cun 3150 . . . . . . . 8  class  ( dom  x  u.  ran  x
)
94, 8cres 4691 . . . . . . 7  class  (  _I  |`  ( dom  x  u. 
ran  x ) )
10 vz . . . . . . . 8  set  z
1110cv 1622 . . . . . . 7  class  z
129, 11wss 3152 . . . . . 6  wff  (  _I  |`  ( dom  x  u. 
ran  x ) ) 
C_  z
135, 11wss 3152 . . . . . 6  wff  x  C_  z
1411, 11ccom 4693 . . . . . . 7  class  ( z  o.  z )
1514, 11wss 3152 . . . . . 6  wff  ( z  o.  z )  C_  z
1612, 13, 15w3a 934 . . . . 5  wff  ( (  _I  |`  ( dom  x  u.  ran  x ) )  C_  z  /\  x  C_  z  /\  (
z  o.  z ) 
C_  z )
1716, 10cab 2269 . . . 4  class  { z  |  ( (  _I  |`  ( dom  x  u. 
ran  x ) ) 
C_  z  /\  x  C_  z  /\  ( z  o.  z )  C_  z ) }
1817cint 3862 . . 3  class  |^| { z  |  ( (  _I  |`  ( dom  x  u. 
ran  x ) ) 
C_  z  /\  x  C_  z  /\  ( z  o.  z )  C_  z ) }
192, 3, 18cmpt 4077 . 2  class  ( x  e.  _V  |->  |^| { z  |  ( (  _I  |`  ( dom  x  u. 
ran  x ) ) 
C_  z  /\  x  C_  z  /\  ( z  o.  z )  C_  z ) } )
201, 19wceq 1623 1  wff  t
*  =  ( x  e.  _V  |->  |^| { z  |  ( (  _I  |`  ( dom  x  u. 
ran  x ) ) 
C_  z  /\  x  C_  z  /\  ( z  o.  z )  C_  z ) } )
Colors of variables: wff set class
This definition is referenced by:  dfrtrcl2  24045
  Copyright terms: Public domain W3C validator