Definition df-tskm

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctskm	⊢ tarskiMap
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		ctsk	⊢ Tarski
5	1	cv	⊢ 𝑥
6	3	cv	⊢ 𝑦
7	5 6	wcel	⊢ 𝑥 ∈ 𝑦
8	7 3 4	crab	⊢ { 𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦 }
9	8	cint	⊢ ∩ { 𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦 }
10	1 2 9	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦 } )
11	0 10	wceq	⊢ tarskiMap = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦 } )