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 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
StepHypRef Expression
1 cwpointsN 38662 . 2 class WAtoms
2 vk . . 3 setvar π‘˜
3 cvv 3473 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1540 . . . . 5 class π‘˜
6 catm 37938 . . . . 5 class Atoms
75, 6cfv 6532 . . . 4 class (Atomsβ€˜π‘˜)
84cv 1540 . . . . . . 7 class 𝑑
98csn 4622 . . . . . 6 class {𝑑}
10 cpolN 38578 . . . . . . 7 class βŠ₯𝑃
115, 10cfv 6532 . . . . . 6 class (βŠ₯π‘ƒβ€˜π‘˜)
129, 11cfv 6532 . . . . 5 class ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑})
137, 12cdif 3941 . . . 4 class ((Atomsβ€˜π‘˜) βˆ– ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑}))
144, 7, 13cmpt 5224 . . 3 class (𝑑 ∈ (Atomsβ€˜π‘˜) ↦ ((Atomsβ€˜π‘˜) βˆ– ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑})))
152, 3, 14cmpt 5224 . 2 class (π‘˜ ∈ V ↦ (𝑑 ∈ (Atomsβ€˜π‘˜) ↦ ((Atomsβ€˜π‘˜) βˆ– ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑}))))
161, 15wceq 1541 1 wff WAtoms = (π‘˜ ∈ V ↦ (𝑑 ∈ (Atomsβ€˜π‘˜) ↦ ((Atomsβ€˜π‘˜) βˆ– ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑}))))
Colors of variables: wff setvar class
This definition is referenced by:  watfvalN  38668
  Copyright terms: Public domain W3C validator