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

Definition df-tsk 8916
Description: The class of all Tarski classes. Tarski classes is a phrase coined by Grzegorz Bancerek in his article Tarski's Classes and Ranks, Journal of Formalized Mathematics, Vol 1, No 3, May-August 1990. A Tarski class is a set whose existence is ensured by Tarski's axiom A (see ax-groth 8990 and the equivalent axioms). Axiom A was first presented in Tarski's article _Über unerreichbare Kardinalzahlen_. Tarski had invented the axiom A to enable ZFC to manage inaccessible cardinals. Later Grothendieck invented the concept of Grothendieck universes and showed they were equal to transitive Tarski classes. (Contributed by FL, 30-Dec-2010.)
Assertion
Ref Expression
df-tsk  |-  Tarski  =  {
y  |  ( A. z  e.  y  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )  /\  A. z  e.  ~P  y ( z  ~~  y  \/  z  e.  y ) ) }
Distinct variable group:    y, z, w

Detailed syntax breakdown of Definition df-tsk
StepHypRef Expression
1 ctsk 8915 . 2  class  Tarski
2 vz . . . . . . . . 9  setvar  z
32cv 1368 . . . . . . . 8  class  z
43cpw 3860 . . . . . . 7  class  ~P z
5 vy . . . . . . . 8  setvar  y
65cv 1368 . . . . . . 7  class  y
74, 6wss 3328 . . . . . 6  wff  ~P z  C_  y
8 vw . . . . . . . . 9  setvar  w
98cv 1368 . . . . . . . 8  class  w
104, 9wss 3328 . . . . . . 7  wff  ~P z  C_  w
1110, 8, 6wrex 2716 . . . . . 6  wff  E. w  e.  y  ~P z  C_  w
127, 11wa 369 . . . . 5  wff  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )
1312, 2, 6wral 2715 . . . 4  wff  A. z  e.  y  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )
14 cen 7307 . . . . . . 7  class  ~~
153, 6, 14wbr 4292 . . . . . 6  wff  z  ~~  y
162, 5wel 1757 . . . . . 6  wff  z  e.  y
1715, 16wo 368 . . . . 5  wff  ( z 
~~  y  \/  z  e.  y )
186cpw 3860 . . . . 5  class  ~P y
1917, 2, 18wral 2715 . . . 4  wff  A. z  e.  ~P  y ( z 
~~  y  \/  z  e.  y )
2013, 19wa 369 . . 3  wff  ( A. z  e.  y  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )  /\  A. z  e.  ~P  y ( z  ~~  y  \/  z  e.  y ) )
2120, 5cab 2429 . 2  class  { y  |  ( A. z  e.  y  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )  /\  A. z  e.  ~P  y
( z  ~~  y  \/  z  e.  y
) ) }
221, 21wceq 1369 1  wff  Tarski  =  {
y  |  ( A. z  e.  y  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )  /\  A. z  e.  ~P  y ( z  ~~  y  \/  z  e.  y ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  eltskg  8917
  Copyright terms: Public domain W3C validator