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 34294
 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 34290 . 2 class WAtoms
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1474 . . . . 5 class 𝑘
6 catm 33568 . . . . 5 class Atoms
75, 6cfv 5804 . . . 4 class (Atoms‘𝑘)
84cv 1474 . . . . . . 7 class 𝑑
98csn 4125 . . . . . 6 class {𝑑}
10 cpolN 34206 . . . . . . 7 class 𝑃
115, 10cfv 5804 . . . . . 6 class (⊥𝑃𝑘)
129, 11cfv 5804 . . . . 5 class ((⊥𝑃𝑘)‘{𝑑})
137, 12cdif 3537 . . . 4 class ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))
144, 7, 13cmpt 4643 . . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑})))
152, 3, 14cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))))
161, 15wceq 1475 1 wff WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃𝑘)‘{𝑑}))))
 Colors of variables: wff setvar class This definition is referenced by:  watfvalN  34296
 Copyright terms: Public domain W3C validator