Definition df-watsN 38666

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 38662	. 2 class WAtoms
2		vk	. . 3 setvar 𝑘
3		cvv 3473	. . 3 class V
4		vd	. . . 4 setvar 𝑑
5	2	cv 1540	. . . . 5 class 𝑘
6		catm 37938	. . . . 5 class Atoms
7	5, 6	cfv 6532	. . . 4 class (Atoms‘𝑘)
8	4	cv 1540	. . . . . . 7 class 𝑑
9	8	csn 4622	. . . . . 6 class {𝑑}
10		cpolN 38578	. . . . . . 7 class ⊥𝑃
11	5, 10	cfv 6532	. . . . . 6 class (⊥𝑃‘𝑘)
12	9, 11	cfv 6532	. . . . 5 class ((⊥𝑃‘𝑘)‘{𝑑})
13	7, 12	cdif 3941	. . . 4 class ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))
14	4, 7, 13	cmpt 5224	. . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑})))
15	2, 3, 14	cmpt 5224	. 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))))
16	1, 15	wceq 1541	1 wff WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))))

This definition is referenced by:  watfvalN  38668