Definition df-tsk

Description: The class of all Tarski classes. Tarski classes is a phrase coined by Grzegorz Bancerek in his articleTarski'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 and the equivalent axioms). Axiom A was first presented in Tarski's articleUeber 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)

	Ref	Expression
Assertion	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 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctsk	|- Tarski
1		vy	|- y
2		vz	|- z
3	1	cv	|- y
4	2	cv	|- z
5	4	cpw	|- ~P z
6	5 3	wss	|- ~P z C_ y
7		vw	|- w
8	7	cv	|- w
9	5 8	wss	|- ~P z C_ w
10	9 7 3	wrex	|- E. w e. y ~P z C_ w
11	6 10	wa	|- ( ~P z C_ y /\ E. w e. y ~P z C_ w )
12	11 2 3	wral	|- A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w )
13	3	cpw	|- ~P y
14		cen	|- ~~
15	4 3 14	wbr	|- z ~~ y
16	4 3	wcel	|- z e. y
17	15 16	wo	|- ( z ~~ y \/ z e. y )
18	17 2 13	wral	|- A. z e. ~P y ( z ~~ y \/ z e. y )
19	12 18	wa	|- ( 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 ) )
20	19 1	cab	|- { 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 ) ) }
21	0 20	wceq	|- 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 ) ) }