Definition df-tskm 10907

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 10906	. 2 class tarskiMap
2		vx	. . 3 setvar 𝑥
3		cvv 3488	. . 3 class V
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	wel 2109	. . . . 5 wff 𝑥 ∈ 𝑦
6		ctsk 10817	. . . . 5 class Tarski
7	5, 4, 6	crab 3443	. . . 4 class {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}
8	7	cint 4970	. . 3 class ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}
9	2, 3, 8	cmpt 5249	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})
10	1, 9	wceq 1537	1 wff tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})

This definition is referenced by:  tskmval  10908