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