Definition df-pointsN 37443

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 37436	. 2 class Points
2		vk	. . 3 setvar 𝑘
3		cvv 3422	. . 3 class V
4		vq	. . . . . . 7 setvar 𝑞
5	4	cv 1538	. . . . . 6 class 𝑞
6		vp	. . . . . . . 8 setvar 𝑝
7	6	cv 1538	. . . . . . 7 class 𝑝
8	7	csn 4558	. . . . . 6 class {𝑝}
9	5, 8	wceq 1539	. . . . 5 wff 𝑞 = {𝑝}
10	2	cv 1538	. . . . . 6 class 𝑘
11		catm 37204	. . . . . 6 class Atoms
12	10, 11	cfv 6418	. . . . 5 class (Atoms‘𝑘)
13	9, 6, 12	wrex 3064	. . . 4 wff ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}
14	13, 4	cab 2715	. . 3 class {𝑞 ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}}
15	2, 3, 14	cmpt 5153	. 2 class (𝑘 ∈ V ↦ {𝑞 ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}})
16	1, 15	wceq 1539	1 wff Points = (𝑘 ∈ V ↦ {𝑞 ∣ ∃𝑝 ∈ (Atoms‘𝑘)𝑞 = {𝑝}})

This definition is referenced by:  pointsetN  37682