Definition df-tskm 9660

Description: A function that maps a set 𝑥 to the smallest Tarski class that contains the set. (Contributed by FL, 30-Dec-2010.)

Assertion

Ref	Expression
df-tskm	⊢ tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-tskm

Step	Hyp	Ref	Expression
1		ctskm 9659	. 2 class tarskiMap
2		vx	. . 3 setvar 𝑥
3		cvv 3200	. . 3 class V
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	wel 1991	. . . . 5 wff 𝑥 ∈ 𝑦
6		ctsk 9570	. . . . 5 class Tarski
7	5, 4, 6	crab 2916	. . . 4 class {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}
8	7	cint 4475	. . 3 class ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}
9	2, 3, 8	cmpt 4729	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})
10	1, 9	wceq 1483	1 wff tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})

This definition is referenced by:  tskmval  9661