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

Definition df-tsk 9773
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 9847 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 9772 . 2 class Tarski
2 vz . . . . . . . . 9 setvar 𝑧
32cv 1630 . . . . . . . 8 class 𝑧
43cpw 4297 . . . . . . 7 class 𝒫 𝑧
5 vy . . . . . . . 8 setvar 𝑦
65cv 1630 . . . . . . 7 class 𝑦
74, 6wss 3723 . . . . . 6 wff 𝒫 𝑧𝑦
8 vw . . . . . . . . 9 setvar 𝑤
98cv 1630 . . . . . . . 8 class 𝑤
104, 9wss 3723 . . . . . . 7 wff 𝒫 𝑧𝑤
1110, 8, 6wrex 3062 . . . . . 6 wff 𝑤𝑦 𝒫 𝑧𝑤
127, 11wa 382 . . . . 5 wff (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤)
1312, 2, 6wral 3061 . . . 4 wff 𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤)
14 cen 8106 . . . . . . 7 class
153, 6, 14wbr 4786 . . . . . 6 wff 𝑧𝑦
162, 5wel 2146 . . . . . 6 wff 𝑧𝑦
1715, 16wo 836 . . . . 5 wff (𝑧𝑦𝑧𝑦)
186cpw 4297 . . . . 5 class 𝒫 𝑦
1917, 2, 18wral 3061 . . . 4 wff 𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦)
2013, 19wa 382 . . 3 wff (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))
2120, 5cab 2757 . 2 class {𝑦 ∣ (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))}
221, 21wceq 1631 1 wff Tarski = {𝑦 ∣ (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))}
Colors of variables: wff setvar class
This definition is referenced by:  eltskg  9774
  Copyright terms: Public domain W3C validator