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

Metamath Proof Explorer

Definition df-pointsN

Detailed syntax breakdown