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

Definition df-tar 25882
Description: A function to study Tarski's classes. See valdom 25884 for its domain, vtare 25885 for its value at  (/), vtarsu 25886 for its value at a successor, vtarl 25887 for its value at a limit ordinal. (Contributed by FL, 20-Mar-2011.)
Assertion
Ref Expression
df-tar  |-  tar  =  ( a  e.  _V ,  b  e.  _V  |->  ( rec ( ( x  e.  _V  |->  ( ( { u  |  E. v  e.  x  (
u  C_  v  \/  u  =  ~P v
) }  u.  ~P x )  i^i  ( tarskiMap `  a ) ) ) ,  { a } )  |`  b )
)
Distinct variable group:    a, b, x, u, v

Detailed syntax breakdown of Definition df-tar
StepHypRef Expression
1 ctar 25881 . 2  class  tar
2 va . . 3  set  a
3 vb . . 3  set  b
4 cvv 2788 . . 3  class  _V
5 vx . . . . . 6  set  x
6 vu . . . . . . . . . . . . 13  set  u
76cv 1622 . . . . . . . . . . . 12  class  u
8 vv . . . . . . . . . . . . 13  set  v
98cv 1622 . . . . . . . . . . . 12  class  v
107, 9wss 3152 . . . . . . . . . . 11  wff  u  C_  v
119cpw 3625 . . . . . . . . . . . 12  class  ~P v
127, 11wceq 1623 . . . . . . . . . . 11  wff  u  =  ~P v
1310, 12wo 357 . . . . . . . . . 10  wff  ( u 
C_  v  \/  u  =  ~P v )
145cv 1622 . . . . . . . . . 10  class  x
1513, 8, 14wrex 2544 . . . . . . . . 9  wff  E. v  e.  x  ( u  C_  v  \/  u  =  ~P v )
1615, 6cab 2269 . . . . . . . 8  class  { u  |  E. v  e.  x  ( u  C_  v  \/  u  =  ~P v
) }
1714cpw 3625 . . . . . . . 8  class  ~P x
1816, 17cun 3150 . . . . . . 7  class  ( { u  |  E. v  e.  x  ( u  C_  v  \/  u  =  ~P v ) }  u.  ~P x )
192cv 1622 . . . . . . . 8  class  a
20 ctskm 8459 . . . . . . . 8  class  tarskiMap
2119, 20cfv 5255 . . . . . . 7  class  ( tarskiMap `  a )
2218, 21cin 3151 . . . . . 6  class  ( ( { u  |  E. v  e.  x  (
u  C_  v  \/  u  =  ~P v
) }  u.  ~P x )  i^i  ( tarskiMap `  a ) )
235, 4, 22cmpt 4077 . . . . 5  class  ( x  e.  _V  |->  ( ( { u  |  E. v  e.  x  (
u  C_  v  \/  u  =  ~P v
) }  u.  ~P x )  i^i  ( tarskiMap `  a ) ) )
2419csn 3640 . . . . 5  class  { a }
2523, 24crdg 6422 . . . 4  class  rec (
( x  e.  _V  |->  ( ( { u  |  E. v  e.  x  ( u  C_  v  \/  u  =  ~P v
) }  u.  ~P x )  i^i  ( tarskiMap `  a ) ) ) ,  { a } )
263cv 1622 . . . 4  class  b
2725, 26cres 4691 . . 3  class  ( rec ( ( x  e. 
_V  |->  ( ( { u  |  E. v  e.  x  ( u  C_  v  \/  u  =  ~P v ) }  u.  ~P x )  i^i  ( tarskiMap `  a
) ) ) ,  { a } )  |`  b )
282, 3, 4, 4, 27cmpt2 5860 . 2  class  ( a  e.  _V ,  b  e.  _V  |->  ( rec ( ( x  e. 
_V  |->  ( ( { u  |  E. v  e.  x  ( u  C_  v  \/  u  =  ~P v ) }  u.  ~P x )  i^i  ( tarskiMap `  a
) ) ) ,  { a } )  |`  b ) )
291, 28wceq 1623 1  wff  tar  =  ( a  e.  _V ,  b  e.  _V  |->  ( rec ( ( x  e.  _V  |->  ( ( { u  |  E. v  e.  x  (
u  C_  v  \/  u  =  ~P v
) }  u.  ~P x )  i^i  ( tarskiMap `  a ) ) ) ,  { a } )  |`  b )
)
Colors of variables: wff set class
This definition is referenced by:  valtar  25883
  Copyright terms: Public domain W3C validator