Metamath Proof Explorer

Definition df-pointsN

Description: Define set of all projective points in a Hilbert lattice (actually in any set at all, for simplicity). A projective point is the singleton of a lattice atom. Definition 15.1 of MaedaMaeda p. 61. Note that item 1 in Holland95 p. 222 defines a point as the atom itself, but this leads to a complicated subspace ordering that may be either membership or inclusion based on its arguments. (Contributed by NM, 2-Oct-2011)

Ref Expression
Assertion df-pointsN ⊢ Points = k ∈ V ⟼ q | ∃ p ∈ Atoms ⁡ k q = p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpointsN class Points
1 vk setvar k
2 cvv class V
3 vq setvar q
4 vp setvar p
5 catm class Atoms
6 1 cv setvar k
7 6 5 cfv class Atoms ⁡ k
8 3 cv setvar q
9 4 cv setvar p
10 9 csn class p
11 8 10 wceq wff q = p
12 11 4 7 wrex wff ∃ p ∈ Atoms ⁡ k q = p
13 12 3 cab class q | ∃ p ∈ Atoms ⁡ k q = p
14 1 2 13 cmpt class k ∈ V ⟼ q | ∃ p ∈ Atoms ⁡ k q = p
15 0 14 wceq wff Points = k ∈ V ⟼ q | ∃ p ∈ Atoms ⁡ k q = p