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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cwpointsN | |
|
1 | vk | |
|
2 | cvv | |
|
3 | vd | |
|
4 | catm | |
|
5 | 1 | cv | |
6 | 5 4 | cfv | |
7 | cpolN | |
|
8 | 5 7 | cfv | |
9 | 3 | cv | |
10 | 9 | csn | |
11 | 10 8 | cfv | |
12 | 6 11 | cdif | |
13 | 3 6 12 | cmpt | |
14 | 1 2 13 | cmpt | |
15 | 0 14 | wceq | |