Definition df-pointsN 38886

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 = (𝑘 ∈ V ↦ {𝑞 ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}})

Distinct variable group:   𝑘,𝑝,𝑞

Detailed syntax breakdown of Definition df-pointsN

Step	Hyp	Ref	Expression
1		cpointsN 38879	. 2 class Points
2		vk	. . 3 setvar 𝑘
3		cvv 3468	. . 3 class V
4		vq	. . . . . . 7 setvar 𝑞
5	4	cv 1532	. . . . . 6 class 𝑞
6		vp	. . . . . . . 8 setvar 𝑝
7	6	cv 1532	. . . . . . 7 class 𝑝
8	7	csn 4623	. . . . . 6 class {𝑝}
9	5, 8	wceq 1533	. . . . 5 wff 𝑞 = {𝑝}
10	2	cv 1532	. . . . . 6 class 𝑘
11		catm 38646	. . . . . 6 class Atoms
12	10, 11	cfv 6537	. . . . 5 class (Atoms‘𝑘)
13	9, 6, 12	wrex 3064	. . . 4 wff ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}
14	13, 4	cab 2703	. . 3 class {𝑞 ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}}
15	2, 3, 14	cmpt 5224	. 2 class (𝑘 ∈ V ↦ {𝑞 ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}})
16	1, 15	wceq 1533	1 wff Points = (𝑘 ∈ V ↦ {𝑞 ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}})

This definition is referenced by:  pointsetN  39125