Definition df-tsk 9571

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 9645 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 = { y | ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) ) }

Distinct variable group:   y, z, w

Detailed syntax breakdown of Definition df-tsk

Step	Hyp	Ref	Expression
1		ctsk 9570	. 2 class Tarski
2		vz	. . . . . . . . 9 setvar z
3	2	cv 1482	. . . . . . . 8 class z
4	3	cpw 4158	. . . . . . 7 class ~P z
5		vy	. . . . . . . 8 setvar y
6	5	cv 1482	. . . . . . 7 class y
7	4, 6	wss 3574	. . . . . 6 wff ~P z C_ y
8		vw	. . . . . . . . 9 setvar w
9	8	cv 1482	. . . . . . . 8 class w
10	4, 9	wss 3574	. . . . . . 7 wff ~P z C_ w
11	10, 8, 6	wrex 2913	. . . . . 6 wff E. w e. y ~P z C_ w
12	7, 11	wa 384	. . . . 5 wff ( ~P z C_ y /\ E. w e. y ~P z C_ w )
13	12, 2, 6	wral 2912	. . . 4 wff A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w )
14		cen 7952	. . . . . . 7 class ~~
15	3, 6, 14	wbr 4653	. . . . . 6 wff z ~~ y
16	2, 5	wel 1991	. . . . . 6 wff z e. y
17	15, 16	wo 383	. . . . 5 wff ( z ~~ y \/ z e. y )
18	6	cpw 4158	. . . . 5 class ~P y
19	17, 2, 18	wral 2912	. . . 4 wff A. z e. ~P y ( z ~~ y \/ z e. y )
20	13, 19	wa 384	. . 3 wff ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) )
21	20, 5	cab 2608	. 2 class { y | ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) ) }
22	1, 21	wceq 1483	1 wff Tarski = { y | ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) ) }

This definition is referenced by:  eltskg  9572