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

Definition df-tsk 9173
 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 9247 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 9172 . 2
2 vz . . . . . . . . 9
32cv 1436 . . . . . . . 8
43cpw 3985 . . . . . . 7
5 vy . . . . . . . 8
65cv 1436 . . . . . . 7
74, 6wss 3442 . . . . . 6
8 vw . . . . . . . . 9
98cv 1436 . . . . . . . 8
104, 9wss 3442 . . . . . . 7
1110, 8, 6wrex 2783 . . . . . 6
127, 11wa 370 . . . . 5
1312, 2, 6wral 2782 . . . 4
14 cen 7574 . . . . . . 7
153, 6, 14wbr 4426 . . . . . 6
162, 5wel 1871 . . . . . 6
1715, 16wo 369 . . . . 5
186cpw 3985 . . . . 5
1917, 2, 18wral 2782 . . . 4
2013, 19wa 370 . . 3
2120, 5cab 2414 . 2
221, 21wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  eltskg  9174
 Copyright terms: Public domain W3C validator