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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpointsN	⊢ Points
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vq	⊢ 𝑞
4		vp	⊢ 𝑝
5		catm	⊢ Atoms
6	1	cv	⊢ 𝑘
7	6 5	cfv	⊢ ( Atoms ‘ 𝑘 )
8	3	cv	⊢ 𝑞
9	4	cv	⊢ 𝑝
10	9	csn	⊢ { 𝑝 }
11	8 10	wceq	⊢ 𝑞 = { 𝑝 }
12	11 4 7	wrex	⊢ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑞 = { 𝑝 }
13	12 3	cab	⊢ { 𝑞 ∣ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑞 = { 𝑝 } }
14	1 2 13	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑞 ∣ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑞 = { 𝑝 } } )
15	0 14	wceq	⊢ Points = ( 𝑘 ∈ V ↦ { 𝑞 ∣ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑞 = { 𝑝 } } )

Metamath Proof Explorer

Definition df-pointsN

Detailed syntax breakdown