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

Definition df-tsk 8614
 Description: The class of all Tarski's classes. Tarski's 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's class is a set whose existence is ensured by Tarski's axiom A (see ax-groth 8688 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's universes and showed they were equal to transitive Tarski's 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 8613 . 2
2 vz . . . . . . . . 9
32cv 1651 . . . . . . . 8
43cpw 3791 . . . . . . 7
5 vy . . . . . . . 8
65cv 1651 . . . . . . 7
74, 6wss 3312 . . . . . 6
8 vw . . . . . . . . 9
98cv 1651 . . . . . . . 8
104, 9wss 3312 . . . . . . 7
1110, 8, 6wrex 2698 . . . . . 6
127, 11wa 359 . . . . 5
1312, 2, 6wral 2697 . . . 4
14 cen 7098 . . . . . . 7
153, 6, 14wbr 4204 . . . . . 6
162, 5wel 1726 . . . . . 6
1715, 16wo 358 . . . . 5
186cpw 3791 . . . . 5
1917, 2, 18wral 2697 . . . 4
2013, 19wa 359 . . 3
2120, 5cab 2421 . 2
221, 21wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  eltskg  8615
 Copyright terms: Public domain W3C validator