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 = { 𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cat	⊢ HAtoms
1		vx	⊢ 𝑥
2		cch	⊢ Cℋ
3		c0h	⊢ 0ℋ
4		ccv	⊢ ⋖ℋ
5	1	cv	⊢ 𝑥
6	3 5 4	wbr	⊢ 0ℋ ⋖ℋ 𝑥
7	6 1 2	crab	⊢ { 𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥 }
8	0 7	wceq	⊢ HAtoms = { 𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥 }