Definition df-at 29197

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 29198 and elat2 29199 for membership relations. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.)

Assertion

Ref	Expression
df-at	|- HAtoms = { x e. CH | 0H <oH x }

Detailed syntax breakdown of Definition df-at

Step	Hyp	Ref	Expression
1		cat 27822	. 2 class HAtoms
2		c0h 27792	. . . 4 class 0H
3		vx	. . . . 5 setvar x
4	3	cv 1482	. . . 4 class x
5		ccv 27821	. . . 4 class <oH
6	2, 4, 5	wbr 4653	. . 3 wff 0H <oH x
7		cch 27786	. . 3 class CH
8	6, 3, 7	crab 2916	. 2 class { x e. CH | 0H <oH x }
9	1, 8	wceq 1483	1 wff HAtoms = { x e. CH | 0H <oH x }

This definition is referenced by:  ela  29198  atssch  29202