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 | z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctsk class Tarski
1 vy setvar y
2 vz setvar z
3 1 cv setvar y
4 2 cv setvar z
5 4 cpw class 𝒫 z
6 5 3 wss wff 𝒫 z y
7 vw setvar w
8 7 cv setvar w
9 5 8 wss wff 𝒫 z w
10 9 7 3 wrex wff w y 𝒫 z w
11 6 10 wa wff 𝒫 z y w y 𝒫 z w
12 11 2 3 wral wff z y 𝒫 z y w y 𝒫 z w
13 3 cpw class 𝒫 y
14 cen class
15 4 3 14 wbr wff z y
16 4 3 wcel wff z y
17 15 16 wo wff z y z y
18 17 2 13 wral wff z 𝒫 y z y z y
19 12 18 wa wff z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y
20 19 1 cab class y | z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y
21 0 20 wceq wff Tarski = y | z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y