Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dftsk  Unicode version 
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 MayAugust 1990. A Tarski's class is a set whose existence is ensured by Tarski's axiom A (see axgroth 8445 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, 30Dec2010.) 
Ref  Expression 

dftsk 
Step  Hyp  Ref  Expression 

1  ctsk 8370  . 2  
2  vz  . . . . . . . . 9  
3  2  cv 1622  . . . . . . . 8 
4  3  cpw 3625  . . . . . . 7 
5  vy  . . . . . . . 8  
6  5  cv 1622  . . . . . . 7 
7  4, 6  wss 3152  . . . . . 6 
8  vw  . . . . . . . . 9  
9  8  cv 1622  . . . . . . . 8 
10  4, 9  wss 3152  . . . . . . 7 
11  10, 8, 6  wrex 2544  . . . . . 6 
12  7, 11  wa 358  . . . . 5 
13  12, 2, 6  wral 2543  . . . 4 
14  cen 6860  . . . . . . 7  
15  3, 6, 14  wbr 4023  . . . . . 6 
16  2, 5  wel 1685  . . . . . 6 
17  15, 16  wo 357  . . . . 5 
18  6  cpw 3625  . . . . 5 
19  17, 2, 18  wral 2543  . . . 4 
20  13, 19  wa 358  . . 3 
21  20, 5  cab 2269  . 2 
22  1, 21  wceq 1623  1 
Colors of variables: wff set class 
This definition is referenced by: eltskg 8372 
Copyright terms: Public domain  W3C validator 