Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-watsN Structured version   Visualization version   GIF version

Definition df-watsN 37285
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
StepHypRef Expression
1 cwpointsN 37281 . 2 class WAtoms
2 vk . . 3 setvar 𝑘
3 cvv 3444 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1537 . . . . 5 class 𝑘
6 catm 36558 . . . . 5 class Atoms
75, 6cfv 6328 . . . 4 class (Atoms‘𝑘)
84cv 1537 . . . . . . 7 class 𝑑
98csn 4528 . . . . . 6 class {𝑑}
10 cpolN 37197 . . . . . . 7 class 𝑃
115, 10cfv 6328 . . . . . 6 class (⊥𝑃𝑘)
129, 11cfv 6328 . . . . 5 class ((⊥𝑃𝑘)‘{𝑑})
137, 12cdif 3881 . . . 4 class ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))
144, 7, 13cmpt 5113 . . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑})))
152, 3, 14cmpt 5113 . 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))))
161, 15wceq 1538 1 wff WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))))
Colors of variables: wff setvar class
This definition is referenced by:  watfvalN  37287
  Copyright terms: Public domain W3C validator