Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trcls Unicode version

Definition df-trcls 25996
Description: The transitive closure of a set. (Contributed by FL, 17-Apr-2011.)
Assertion
Ref Expression
df-trcls  |-  tr  =  ( x  e.  _V  |->  U_ a  e.  om  (
( rec ( ( z  e.  _V  |->  ( z  u.  U. z
) ) ,  x
)  |`  om ) `  a ) )
Distinct variable group:    x, a, z

Detailed syntax breakdown of Definition df-trcls
StepHypRef Expression
1 ctr 25995 . 2  class  tr
2 vx . . 3  set  x
3 cvv 2801 . . 3  class  _V
4 va . . . 4  set  a
5 com 4672 . . . 4  class  om
64cv 1631 . . . . 5  class  a
7 vz . . . . . . . 8  set  z
87cv 1631 . . . . . . . . 9  class  z
98cuni 3843 . . . . . . . . 9  class  U. z
108, 9cun 3163 . . . . . . . 8  class  ( z  u.  U. z )
117, 3, 10cmpt 4093 . . . . . . 7  class  ( z  e.  _V  |->  ( z  u.  U. z ) )
122cv 1631 . . . . . . 7  class  x
1311, 12crdg 6438 . . . . . 6  class  rec (
( z  e.  _V  |->  ( z  u.  U. z ) ) ,  x )
1413, 5cres 4707 . . . . 5  class  ( rec ( ( z  e. 
_V  |->  ( z  u. 
U. z ) ) ,  x )  |`  om )
156, 14cfv 5271 . . . 4  class  ( ( rec ( ( z  e.  _V  |->  ( z  u.  U. z ) ) ,  x )  |`  om ) `  a
)
164, 5, 15ciun 3921 . . 3  class  U_ a  e.  om  ( ( rec ( ( z  e. 
_V  |->  ( z  u. 
U. z ) ) ,  x )  |`  om ) `  a )
172, 3, 16cmpt 4093 . 2  class  ( x  e.  _V  |->  U_ a  e.  om  ( ( rec ( ( z  e. 
_V  |->  ( z  u. 
U. z ) ) ,  x )  |`  om ) `  a ) )
181, 17wceq 1632 1  wff  tr  =  ( x  e.  _V  |->  U_ a  e.  om  (
( rec ( ( z  e.  _V  |->  ( z  u.  U. z
) ) ,  x
)  |`  om ) `  a ) )
Colors of variables: wff set class
This definition is referenced by:  trclval  25997
  Copyright terms: Public domain W3C validator