Definition df-watsN 37128

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

Assertion

Ref	Expression
df-watsN	⊢ WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))))

Distinct variable group:   𝑘,𝑑

Detailed syntax breakdown of Definition df-watsN

Step	Hyp	Ref	Expression
1		cwpointsN 37124	. 2 class WAtoms
2		vk	. . 3 setvar 𝑘
3		cvv 3496	. . 3 class V
4		vd	. . . 4 setvar 𝑑
5	2	cv 1536	. . . . 5 class 𝑘
6		catm 36401	. . . . 5 class Atoms
7	5, 6	cfv 6357	. . . 4 class (Atoms‘𝑘)
8	4	cv 1536	. . . . . . 7 class 𝑑
9	8	csn 4569	. . . . . 6 class {𝑑}
10		cpolN 37040	. . . . . . 7 class ⊥𝑃
11	5, 10	cfv 6357	. . . . . 6 class (⊥𝑃‘𝑘)
12	9, 11	cfv 6357	. . . . 5 class ((⊥𝑃‘𝑘)‘{𝑑})
13	7, 12	cdif 3935	. . . 4 class ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))
14	4, 7, 13	cmpt 5148	. . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑})))
15	2, 3, 14	cmpt 5148	. 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))))
16	1, 15	wceq 1537	1 wff WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))))

This definition is referenced by:  watfvalN  37130