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	$$⊢\mathrm{Points}=\left(k\in \mathrm{V}⟼\left\{q|\exists p\in \mathrm{Atoms}\left(k\right)q=\left\{p\right\}\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpointsN	$$class\mathrm{Points}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vq	$$setvarq$$
4		vp	$$setvarp$$
5		catm	$$class\mathrm{Atoms}$$
6	1	cv	$$setvark$$
7	6 5	cfv	$$class\mathrm{Atoms}\left(k\right)$$
8	3	cv	$$setvarq$$
9	4	cv	$$setvarp$$
10	9	csn	$$class\left\{p\right\}$$
11	8 10	wceq	$$wffq=\left\{p\right\}$$
12	11 4 7	wrex	$$wff\exists p\in \mathrm{Atoms}\left(k\right)q=\left\{p\right\}$$
13	12 3	cab	$$class\left\{q|\exists p\in \mathrm{Atoms}\left(k\right)q=\left\{p\right\}\right\}$$
14	1 2 13	cmpt	$$class\left(k\in \mathrm{V}⟼\left\{q|\exists p\in \mathrm{Atoms}\left(k\right)q=\left\{p\right\}\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{Points}=\left(k\in \mathrm{V}⟼\left\{q|\exists p\in \mathrm{Atoms}\left(k\right)q=\left\{p\right\}\right\}\right)$$