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 e. _V |-> { q | E. p e. ( Atoms ` k ) q = { p } } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpointsN	|- Points
1		vk	|- k
2		cvv	|- _V
3		vq	|- q
4		vp	|- p
5		catm	|- Atoms
6	1	cv	|- k
7	6 5	cfv	|- ( Atoms ` k )
8	3	cv	|- q
9	4	cv	|- p
10	9	csn	|- { p }
11	8 10	wceq	|- q = { p }
12	11 4 7	wrex	|- E. p e. ( Atoms ` k ) q = { p }
13	12 3	cab	|- { q | E. p e. ( Atoms ` k ) q = { p } }
14	1 2 13	cmpt	|- ( k e. _V |-> { q | E. p e. ( Atoms ` k ) q = { p } } )
15	0 14	wceq	|- Points = ( k e. _V |-> { q | E. p e. ( Atoms ` k ) q = { p } } )