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	$$⊢\mathrm{WAtoms}=\left(k\in \mathrm{V}⟼\left(d\in \mathrm{Atoms}\left(k\right)⟼\mathrm{Atoms}\left(k\right)\setminus {\perp }_{𝑃}\left(k\right)\left(\left\{d\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwpointsN	$$class\mathrm{WAtoms}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vd	$$setvard$$
4		catm	$$class\mathrm{Atoms}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{Atoms}\left(k\right)$$
7		cpolN	$$class{\perp }_{𝑃}$$
8	5 7	cfv	$$class{\perp }_{𝑃}\left(k\right)$$
9	3	cv	$$setvard$$
10	9	csn	$$class\left\{d\right\}$$
11	10 8	cfv	$$class{\perp }_{𝑃}\left(k\right)\left(\left\{d\right\}\right)$$
12	6 11	cdif	$$class\left(\mathrm{Atoms}\left(k\right)\setminus {\perp }_{𝑃}\left(k\right)\left(\left\{d\right\}\right)\right)$$
13	3 6 12	cmpt	$$class\left(d\in \mathrm{Atoms}\left(k\right)⟼\mathrm{Atoms}\left(k\right)\setminus {\perp }_{𝑃}\left(k\right)\left(\left\{d\right\}\right)\right)$$
14	1 2 13	cmpt	$$class\left(k\in \mathrm{V}⟼\left(d\in \mathrm{Atoms}\left(k\right)⟼\mathrm{Atoms}\left(k\right)\setminus {\perp }_{𝑃}\left(k\right)\left(\left\{d\right\}\right)\right)\right)$$
15	0 14	wceq	$$wff\mathrm{WAtoms}=\left(k\in \mathrm{V}⟼\left(d\in \mathrm{Atoms}\left(k\right)⟼\mathrm{Atoms}\left(k\right)\setminus {\perp }_{𝑃}\left(k\right)\left(\left\{d\right\}\right)\right)\right)$$