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

Definition df-tsk 9148
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 9222 and the equivalent axioms). Axiom A was first presented in Tarski's article _Über unerreichbare Kardinalzahlen_. Tarski had invented the axiom A to enable ZFC to manage inaccessible cardinals. Later Grothendieck invented 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
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-tsk
StepHypRef Expression
1 ctsk 9147 . 2
2 vz . . . . . . . . 9
32cv 1394 . . . . . . . 8
43cpw 4012 . . . . . . 7
5 vy . . . . . . . 8
65cv 1394 . . . . . . 7
74, 6wss 3475 . . . . . 6
8 vw . . . . . . . . 9
98cv 1394 . . . . . . . 8
104, 9wss 3475 . . . . . . 7
1110, 8, 6wrex 2808 . . . . . 6
127, 11wa 369 . . . . 5
1312, 2, 6wral 2807 . . . 4
14 cen 7533 . . . . . . 7
153, 6, 14wbr 4452 . . . . . 6
162, 5wel 1819 . . . . . 6
1715, 16wo 368 . . . . 5
186cpw 4012 . . . . 5
1917, 2, 18wral 2807 . . . 4
2013, 19wa 369 . . 3
2120, 5cab 2442 . 2
221, 21wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  eltskg  9149
  Copyright terms: Public domain W3C validator