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

Definition df-tsk 8387
Description: The class of all Tarski's classes. Tarski's 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's class is a set whose existence is ensured by Tarski's axiom A (see ax-groth 8461 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's universes and showed they were equal to transitive Tarski's 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 8386 . 2  class  Tarski
2 vz . . . . . . . . 9  set  z
32cv 1631 . . . . . . . 8  class  z
43cpw 3638 . . . . . . 7  class  ~P z
5 vy . . . . . . . 8  set  y
65cv 1631 . . . . . . 7  class  y
74, 6wss 3165 . . . . . 6  wff  ~P z  C_  y
8 vw . . . . . . . . 9  set  w
98cv 1631 . . . . . . . 8  class  w
104, 9wss 3165 . . . . . . 7  wff  ~P z  C_  w
1110, 8, 6wrex 2557 . . . . . 6  wff  E. w  e.  y  ~P z  C_  w
127, 11wa 358 . . . . 5  wff  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )
1312, 2, 6wral 2556 . . . 4  wff  A. z  e.  y  ( ~P z  C_  y  /\  E. w  e.  y  ~P z  C_  w )
14 cen 6876 . . . . . . 7  class  ~~
153, 6, 14wbr 4039 . . . . . 6  wff  z  ~~  y
162, 5wel 1697 . . . . . 6  wff  z  e.  y
1715, 16wo 357 . . . . 5  wff  ( z 
~~  y  \/  z  e.  y )
186cpw 3638 . . . . 5  class  ~P y
1917, 2, 18wral 2556 . . . 4  wff  A. z  e.  ~P  y ( z 
~~  y  \/  z  e.  y )
2013, 19wa 358 . . 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 2282 . 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 1632 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 set class
This definition is referenced by:  eltskg  8388
  Copyright terms: Public domain W3C validator