# 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 ${⊢}\mathrm{Tarski}=\left\{{y}|\left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(𝒫{z}\subseteq {y}\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}𝒫{z}\subseteq {w}\right)\wedge \forall {z}\in 𝒫{y}\phantom{\rule{.4em}{0ex}}\left({z}\approx {y}\vee {z}\in {y}\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ctsk ${class}\mathrm{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}\subseteq {y}$
7 vw ${setvar}{w}$
8 7 cv ${setvar}{w}$
9 5 8 wss ${wff}𝒫{z}\subseteq {w}$
10 9 7 3 wrex ${wff}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}𝒫{z}\subseteq {w}$
11 6 10 wa ${wff}\left(𝒫{z}\subseteq {y}\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}𝒫{z}\subseteq {w}\right)$
12 11 2 3 wral ${wff}\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(𝒫{z}\subseteq {y}\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}𝒫{z}\subseteq {w}\right)$
13 3 cpw ${class}𝒫{y}$
14 cen ${class}\approx$
15 4 3 14 wbr ${wff}{z}\approx {y}$
16 4 3 wcel ${wff}{z}\in {y}$
17 15 16 wo ${wff}\left({z}\approx {y}\vee {z}\in {y}\right)$
18 17 2 13 wral ${wff}\forall {z}\in 𝒫{y}\phantom{\rule{.4em}{0ex}}\left({z}\approx {y}\vee {z}\in {y}\right)$
19 12 18 wa ${wff}\left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(𝒫{z}\subseteq {y}\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}𝒫{z}\subseteq {w}\right)\wedge \forall {z}\in 𝒫{y}\phantom{\rule{.4em}{0ex}}\left({z}\approx {y}\vee {z}\in {y}\right)\right)$
20 19 1 cab ${class}\left\{{y}|\left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(𝒫{z}\subseteq {y}\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}𝒫{z}\subseteq {w}\right)\wedge \forall {z}\in 𝒫{y}\phantom{\rule{.4em}{0ex}}\left({z}\approx {y}\vee {z}\in {y}\right)\right)\right\}$
21 0 20 wceq ${wff}\mathrm{Tarski}=\left\{{y}|\left(\forall {z}\in {y}\phantom{\rule{.4em}{0ex}}\left(𝒫{z}\subseteq {y}\wedge \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}𝒫{z}\subseteq {w}\right)\wedge \forall {z}\in 𝒫{y}\phantom{\rule{.4em}{0ex}}\left({z}\approx {y}\vee {z}\in {y}\right)\right)\right\}$