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 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)

		Ref	Expression
	Assertion	df-tsk	⊢ Tarski = { 𝑦 ∣ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctsk	⊢ Tarski
1		vy	⊢ 𝑦
2		vz	⊢ 𝑧
3	1	cv	⊢ 𝑦
4	2	cv	⊢ 𝑧
5	4	cpw	⊢ 𝒫 𝑧
6	5 3	wss	⊢ 𝒫 𝑧 ⊆ 𝑦
7		vw	⊢ 𝑤
8	7	cv	⊢ 𝑤
9	5 8	wss	⊢ 𝒫 𝑧 ⊆ 𝑤
10	9 7 3	wrex	⊢ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤
11	6 10	wa	⊢ ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 )
12	11 2 3	wral	⊢ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 )
13	3	cpw	⊢ 𝒫 𝑦
14		cen	⊢ ≈
15	4 3 14	wbr	⊢ 𝑧 ≈ 𝑦
16	4 3	wcel	⊢ 𝑧 ∈ 𝑦
17	15 16	wo	⊢ ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 )
18	17 2 13	wral	⊢ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 )
19	12 18	wa	⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) )
20	19 1	cab	⊢ { 𝑦 ∣ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) }
21	0 20	wceq	⊢ Tarski = { 𝑦 ∣ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∃ 𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦 ) ) }

Metamath Proof Explorer

Definition df-tsk

Detailed syntax breakdown