Metamath Proof Explorer

Definition df-tsk

Description: The class of all Tarski classes. Tarski classes is a phrase coined by Grzegorz Bancerek in his articleTarski'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 and the equivalent axioms). Axiom A was first presented in Tarski's articleUeber unerreichbare Kardinalzahlen. Tarski introduced Axiom A to allow reasoning with inaccessible cardinals in ZFC. Later, Grothendieck introduced the concept of (Grothendieck) universes and showed they were exactly transitive Tarski classes. (Contributed by FL, 30-Dec-2010)

|- 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 ) ) }

 |-  Tarski

 |-  y

 |-  z

 |-  y

 |-  z

 |-  ~P z

 |-  ~P z C_ y

 |-  w

 |-  w

 |-  ~P z C_ w

 |-  E. w e. y ~P z C_ w

 |-  ( ~P z C_ y /\ E. w e. y ~P z C_ w )

 |-  A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w )

 |-  ~P y

 |-  ~~

 |-  z ~~ y

 |-  z e. y

 |-  ( z ~~ y \/ z e. y )

 |-  A. z e. ~P y ( z ~~ y \/ z e. 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 ) )

 |-  { 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 ) ) }

 |-  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 ) ) }