Metamath Proof Explorer


Definition df-at

Description: Define the set of atoms in a Hilbert lattice. An atom is a nonzero element of a lattice such that anything less than it is zero, i.e. it is the smallest nonzero element of the lattice. Definition of atom in Kalmbach p. 15. See ela and elat2 for membership relations. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion df-at
|- HAtoms = { x e. CH | 0H 

Detailed syntax breakdown

Step Hyp Ref Expression
0 cat
 |-  HAtoms
1 vx
 |-  x
2 cch
 |-  CH
3 c0h
 |-  0H
4 ccv
 |-  
5 1 cv
 |-  x
6 3 5 4 wbr
 |-  0H 
7 6 1 2 crab
 |-  { x e. CH | 0H 
8 0 7 wceq
 |-  HAtoms = { x e. CH | 0H