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	$$⊢\mathrm{tarskiMap}=\left(x\in \mathrm{V}⟼\bigcap \left\{y\in \mathrm{Tarski}|x\in y\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctskm	$$class\mathrm{tarskiMap}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4		ctsk	$$class\mathrm{Tarski}$$
5	1	cv	$$setvarx$$
6	3	cv	$$setvary$$
7	5 6	wcel	$$wffx\in y$$
8	7 3 4	crab	$$class\left\{y\in \mathrm{Tarski}|x\in y\right\}$$
9	8	cint	$$class\bigcap \left\{y\in \mathrm{Tarski}|x\in y\right\}$$
10	1 2 9	cmpt	$$class\left(x\in \mathrm{V}⟼\bigcap \left\{y\in \mathrm{Tarski}|x\in y\right\}\right)$$
11	0 10	wceq	$$wff\mathrm{tarskiMap}=\left(x\in \mathrm{V}⟼\bigcap \left\{y\in \mathrm{Tarski}|x\in y\right\}\right)$$