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 38947
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 38943 . 2 class WAtoms
2 vk . . 3 setvar π‘˜
3 cvv 3474 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1540 . . . . 5 class π‘˜
6 catm 38219 . . . . 5 class Atoms
75, 6cfv 6543 . . . 4 class (Atomsβ€˜π‘˜)
84cv 1540 . . . . . . 7 class 𝑑
98csn 4628 . . . . . 6 class {𝑑}
10 cpolN 38859 . . . . . . 7 class βŠ₯𝑃
115, 10cfv 6543 . . . . . 6 class (βŠ₯π‘ƒβ€˜π‘˜)
129, 11cfv 6543 . . . . 5 class ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑})
137, 12cdif 3945 . . . 4 class ((Atomsβ€˜π‘˜) βˆ– ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑}))
144, 7, 13cmpt 5231 . . 3 class (𝑑 ∈ (Atomsβ€˜π‘˜) ↦ ((Atomsβ€˜π‘˜) βˆ– ((βŠ₯π‘ƒβ€˜π‘˜)β€˜{𝑑})))
152, 3, 14cmpt 5231 . 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  38949
  Copyright terms: Public domain W3C validator