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 34093
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 34089 . 2 class WAtoms
2 vk . . 3 setvar 𝑘
3 cvv 3168 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1473 . . . . 5 class 𝑘
6 catm 33367 . . . . 5 class Atoms
75, 6cfv 5786 . . . 4 class (Atoms‘𝑘)
84cv 1473 . . . . . . 7 class 𝑑
98csn 4120 . . . . . 6 class {𝑑}
10 cpolN 34005 . . . . . . 7 class 𝑃
115, 10cfv 5786 . . . . . 6 class (⊥𝑃𝑘)
129, 11cfv 5786 . . . . 5 class ((⊥𝑃𝑘)‘{𝑑})
137, 12cdif 3532 . . . 4 class ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))
144, 7, 13cmpt 4633 . . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑})))
152, 3, 14cmpt 4633 . 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))))
161, 15wceq 1474 1 wff WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))))
Colors of variables: wff setvar class
This definition is referenced by:  watfvalN  34095
  Copyright terms: Public domain W3C validator