Definition df-tsk 10827

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 10901 and the equivalent axioms). Axiom A was first presented in Tarski's article Ueber unerreichbare Kardinalzahlen. Tarski introduced Axiom A to allow reasoning with inaccessible cardinals in ZFC. Later, Grothendieck introduced the concept of (Grothendieck) universes and showed they were exactly 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 10826	. 2 class Tarski
2		vz	. . . . . . . . 9 setvar 𝑧
3	2	cv 1569	. . . . . . . 8 class 𝑧
4	3	cpw 4557	. . . . . . 7 class 𝒫 𝑧
5		vy	. . . . . . . 8 setvar 𝑦
6	5	cv 1569	. . . . . . 7 class 𝑦
7	4, 6	wss 3899	. . . . . 6 wff 𝒫 𝑧 ⊆ 𝑦
8		vw	. . . . . . . . 9 setvar 𝑤
9	8	cv 1569	. . . . . . . 8 class 𝑤
10	4, 9	wss 3899	. . . . . . 7 wff 𝒫 𝑧 ⊆ 𝑤
11	10, 8, 6	wrex 3087	. . . . . 6 wff ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤
12	7, 11	wa 401	. . . . 5 wff (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)
13	12, 2, 6	wral 3077	. . . 4 wff ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤)
14		cen 8963	. . . . . . 7 class ≈
15	3, 6, 14	wbr 5103	. . . . . 6 wff 𝑧 ≈ 𝑦
16	2, 5	wel 2146	. . . . . 6 wff 𝑧 ∈ 𝑦
17	15, 16	wo 861	. . . . 5 wff (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)
18	6	cpw 4557	. . . . 5 class 𝒫 𝑦
19	17, 2, 18	wral 3077	. . . 4 wff ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)
20	13, 19	wa 401	. . 3 wff (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
21	20, 5	cab 2739	. 2 class {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))}
22	1, 21	wceq 1570	1 wff Tarski = {𝑦 ∣ (∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))}

This definition is used by:  eltskg  10828