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 = ( x e. _V |-> |^| { y e. Tarski | x e. y } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctskm	|- tarskiMap
1		vx	|- x
2		cvv	|- _V
3		vy	|- y
4		ctsk	|- Tarski
5	1	cv	|- x
6	3	cv	|- y
7	5 6	wcel	|- x e. y
8	7 3 4	crab	|- { y e. Tarski | x e. y }
9	8	cint	|- |^| { y e. Tarski | x e. y }
10	1 2 9	cmpt	|- ( x e. _V |-> |^| { y e. Tarski | x e. y } )
11	0 10	wceq	|- tarskiMap = ( x e. _V |-> |^| { y e. Tarski | x e. y } )