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 the axiom A to enable ZFC to manage inaccessible cardinals. Later Grothendieck introduced the concept of Grothendieck universes and showed they were equal to transitive Tarski classes. (Contributed by FL, 30-Dec-2010)

Ref Expression
Assertion 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctsk
 |-  Tarski
1 vy
 |-  y
2 vz
 |-  z
3 1 cv
 |-  y
4 2 cv
 |-  z
5 4 cpw
 |-  ~P z
6 5 3 wss
 |-  ~P z C_ y
7 vw
 |-  w
8 7 cv
 |-  w
9 5 8 wss
 |-  ~P z C_ w
10 9 7 3 wrex
 |-  E. w e. y ~P z C_ w
11 6 10 wa
 |-  ( ~P z C_ y /\ E. w e. y ~P z C_ w )
12 11 2 3 wral
 |-  A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w )
13 3 cpw
 |-  ~P y
14 cen
 |-  ~~
15 4 3 14 wbr
 |-  z ~~ y
16 4 3 wcel
 |-  z e. y
17 15 16 wo
 |-  ( z ~~ y \/ z e. y )
18 17 2 13 wral
 |-  A. z e. ~P y ( z ~~ y \/ z e. y )
19 12 18 wa
 |-  ( 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 ) )
20 19 1 cab
 |-  { 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 ) ) }
21 0 20 wceq
 |-  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 ) ) }