Definition df-pointsN 34788

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.)

Assertion

Ref	Expression
df-pointsN	|- Points = ( k e. _V |-> { q | E. p e. ( Atoms ` k ) q = { p } } )

Distinct variable group:   k, p, q

Detailed syntax breakdown of Definition df-pointsN

Step	Hyp	Ref	Expression
1		cpointsN 34781	. 2 class Points
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vq	. . . . . . 7 setvar q
5	4	cv 1482	. . . . . 6 class q
6		vp	. . . . . . . 8 setvar p
7	6	cv 1482	. . . . . . 7 class p
8	7	csn 4177	. . . . . 6 class { p }
9	5, 8	wceq 1483	. . . . 5 wff q = { p }
10	2	cv 1482	. . . . . 6 class k
11		catm 34550	. . . . . 6 class Atoms
12	10, 11	cfv 5888	. . . . 5 class ( Atoms ` k )
13	9, 6, 12	wrex 2913	. . . 4 wff E. p e. ( Atoms ` k ) q = { p }
14	13, 4	cab 2608	. . 3 class { q | E. p e. ( Atoms ` k ) q = { p } }
15	2, 3, 14	cmpt 4729	. 2 class ( k e. _V |-> { q | E. p e. ( Atoms ` k ) q = { p } } )
16	1, 15	wceq 1483	1 wff Points = ( k e. _V |-> { q | E. p e. ( Atoms ` k ) q = { p } } )

This definition is referenced by:  pointsetN  35027