Definition df-tsk 9450

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 9524 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	⊢ Tarski = {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))}

Distinct variable group:   𝑦,𝑧,𝑤

Detailed syntax breakdown of Definition df-tsk

Step	Hyp	Ref	Expression
1		ctsk 9449	. 2 class Tarski
2		vz	. . . . . . . . 9 setvar 𝑧
3	2	cv 1474	. . . . . . . 8 class 𝑧
4	3	cpw 4108	. . . . . . 7 class 𝒫 𝑧
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1474	. . . . . . 7 class 𝑦
7	4, 6	wss 3540	. . . . . 6 wff 𝒫 𝑧 ⊆ 𝑦
8		vw	. . . . . . . . 9 setvar 𝑤
9	8	cv 1474	. . . . . . . 8 class 𝑤
10	4, 9	wss 3540	. . . . . . 7 wff 𝒫 𝑧 ⊆ 𝑤
11	10, 8, 6	wrex 2897	. . . . . 6 wff ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤
12	7, 11	wa 383	. . . . 5 wff (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)
13	12, 2, 6	wral 2896	. . . 4 wff ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)
14		cen 7838	. . . . . . 7 class ≈
15	3, 6, 14	wbr 4583	. . . . . 6 wff 𝑧 ≈ 𝑦
16	2, 5	wel 1978	. . . . . 6 wff 𝑧 ∈ 𝑦
17	15, 16	wo 382	. . . . 5 wff (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)
18	6	cpw 4108	. . . . 5 class 𝒫 𝑦
19	17, 2, 18	wral 2896	. . . 4 wff ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)
20	13, 19	wa 383	. . 3 wff (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
21	20, 5	cab 2596	. 2 class {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))}
22	1, 21	wceq 1475	1 wff Tarski = {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))}

This definition is referenced by:  eltskg  9451