Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tsk Structured version   Visualization version   GIF version

Definition df-tsk 9556
 Description: The class of all Tarski classes. Tarski classes is a phrase coined by Grzegorz Bancerek in his article Tarski'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 9630 and the equivalent axioms). Axiom A was first presented in Tarski's article _Über 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.)
Assertion
Ref Expression
df-tsk Tarski = {𝑦 ∣ (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))}
Distinct variable group:   𝑦,𝑧,𝑤

Detailed syntax breakdown of Definition df-tsk
StepHypRef Expression
1 ctsk 9555 . 2 class Tarski
2 vz . . . . . . . . 9 setvar 𝑧
32cv 1480 . . . . . . . 8 class 𝑧
43cpw 4149 . . . . . . 7 class 𝒫 𝑧
5 vy . . . . . . . 8 setvar 𝑦
65cv 1480 . . . . . . 7 class 𝑦
74, 6wss 3567 . . . . . 6 wff 𝒫 𝑧𝑦
8 vw . . . . . . . . 9 setvar 𝑤
98cv 1480 . . . . . . . 8 class 𝑤
104, 9wss 3567 . . . . . . 7 wff 𝒫 𝑧𝑤
1110, 8, 6wrex 2910 . . . . . 6 wff 𝑤𝑦 𝒫 𝑧𝑤
127, 11wa 384 . . . . 5 wff (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤)
1312, 2, 6wral 2909 . . . 4 wff 𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤)
14 cen 7937 . . . . . . 7 class
153, 6, 14wbr 4644 . . . . . 6 wff 𝑧𝑦
162, 5wel 1989 . . . . . 6 wff 𝑧𝑦
1715, 16wo 383 . . . . 5 wff (𝑧𝑦𝑧𝑦)
186cpw 4149 . . . . 5 class 𝒫 𝑦
1917, 2, 18wral 2909 . . . 4 wff 𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦)
2013, 19wa 384 . . 3 wff (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))
2120, 5cab 2606 . 2 class {𝑦 ∣ (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))}
221, 21wceq 1481 1 wff Tarski = {𝑦 ∣ (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))}
 Colors of variables: wff setvar class This definition is referenced by:  eltskg  9557
 Copyright terms: Public domain W3C validator