Definition df-tskm 10895

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 10894	. 2 class tarskiMap
2		vx	. . 3 setvar 𝑥
3		cvv 3450	. . 3 class V
4		vy	. . . . . 6 setvar 𝑦
5	2, 4	wel 2146	. . . . 5 wff 𝑥 ∈ 𝑦
6		ctsk 10805	. . . . 5 class Tarski
7	5, 4, 6	crab 3412	. . . 4 class {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}
8	7	cint 4906	. . 3 class ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦}
9	2, 3, 8	cmpt 5185	. 2 class (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})
10	1, 9	wceq 1570	1 wff tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})

This definition is used by:  tskmval  10896