Definition df-at 30700

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

Assertion

Ref	Expression
df-at	⊢ HAtoms = {𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥}

Detailed syntax breakdown of Definition df-at

Step	Hyp	Ref	Expression
1		cat 29327	. 2 class HAtoms
2		c0h 29297	. . . 4 class 0ℋ
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1538	. . . 4 class 𝑥
5		ccv 29326	. . . 4 class ⋖ℋ
6	2, 4, 5	wbr 5074	. . 3 wff 0ℋ ⋖ℋ 𝑥
7		cch 29291	. . 3 class Cℋ
8	6, 3, 7	crab 3068	. 2 class {𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥}
9	1, 8	wceq 1539	1 wff HAtoms = {𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥}

This definition is referenced by:  ela  30701  atssch  30705