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 = k ∈ V ⟼ d ∈ Atoms ⁡ k ⟼ Atoms ⁡ k ∖ ⊥ 𝑃 ⁡ k ⁡ d

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwpointsN class WAtoms
1 vk setvar k
2 cvv class V
3 vd setvar d
4 catm class Atoms
5 1 cv setvar k
6 5 4 cfv class Atoms ⁡ k
7 cpolN class ⊥ 𝑃
8 5 7 cfv class ⊥ 𝑃 ⁡ k
9 3 cv setvar d
10 9 csn class d
11 10 8 cfv class ⊥ 𝑃 ⁡ k ⁡ d
12 6 11 cdif class Atoms ⁡ k ∖ ⊥ 𝑃 ⁡ k ⁡ d
13 3 6 12 cmpt class d ∈ Atoms ⁡ k ⟼ Atoms ⁡ k ∖ ⊥ 𝑃 ⁡ k ⁡ d
14 1 2 13 cmpt class k ∈ V ⟼ d ∈ Atoms ⁡ k ⟼ Atoms ⁡ k ∖ ⊥ 𝑃 ⁡ k ⁡ d
15 0 14 wceq wff WAtoms = k ∈ V ⟼ d ∈ Atoms ⁡ k ⟼ Atoms ⁡ k ∖ ⊥ 𝑃 ⁡ k ⁡ d