Metamath Proof Explorer


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=kVdAtomskAtomsk𝑃kd

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwpointsN classWAtoms
1 vk setvark
2 cvv classV
3 vd setvard
4 catm classAtoms
5 1 cv setvark
6 5 4 cfv classAtomsk
7 cpolN class𝑃
8 5 7 cfv class𝑃k
9 3 cv setvard
10 9 csn classd
11 10 8 cfv class𝑃kd
12 6 11 cdif classAtomsk𝑃kd
13 3 6 12 cmpt classdAtomskAtomsk𝑃kd
14 1 2 13 cmpt classkVdAtomskAtomsk𝑃kd
15 0 14 wceq wffWAtoms=kVdAtomskAtomsk𝑃kd