Definition df-watsN

Description: Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" d . These are all atoms not in the polarity of { d } ) , which is the hyperplane determined by d . Definition of set W in Crawley p. 111. (Contributed by NM, 26-Jan-2012)

	Ref	Expression
Assertion	df-watsN	|- WAtoms = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwpointsN	|- WAtoms
1		vk	|- k
2		cvv	|- _V
3		vd	|- d
4		catm	|- Atoms
5	1	cv	|- k
6	5 4	cfv	|- ( Atoms ` k )
7		cpolN	|- _|_P
8	5 7	cfv	|- ( _|_P ` k )
9	3	cv	|- d
10	9	csn	|- { d }
11	10 8	cfv	|- ( ( _|_P ` k ) ` { d } )
12	6 11	cdif	|- ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) )
13	3 6 12	cmpt	|- ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) )
14	1 2 13	cmpt	|- ( k e. _V |-> ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) ) )
15	0 14	wceq	|- WAtoms = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) ) )