Theorem pointsetN

Description: The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pointset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pointset.p	$$⊢P=\mathrm{Points}\left(K\right)$$
Assertion	pointsetN	$$⊢K\in B\to P=\left\{p|\exists a\in Ap=\left\{a\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		pointset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		pointset.p	$$⊢P=\mathrm{Points}\left(K\right)$$
3		elex	$$⊢K\in B\to K\in \mathrm{V}$$
4		fveq2	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=\mathrm{Atoms}\left(K\right)$$
5	4 1	eqtr4di	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=A$$
6	5	rexeqdv	$$⊢k=K\to \left(\exists a\in \mathrm{Atoms}\left(k\right)p=\left\{a\right\}\leftrightarrow \exists a\in Ap=\left\{a\right\}\right)$$
7	6	abbidv	$$⊢k=K\to \left\{p|\exists a\in \mathrm{Atoms}\left(k\right)p=\left\{a\right\}\right\}=\left\{p|\exists a\in Ap=\left\{a\right\}\right\}$$
8		df-pointsN	$$⊢\mathrm{Points}=\left(k\in \mathrm{V}⟼\left\{p|\exists a\in \mathrm{Atoms}\left(k\right)p=\left\{a\right\}\right\}\right)$$
9	1	fvexi	$$⊢A\in \mathrm{V}$$
10	9	abrexex	$$⊢\left\{p|\exists a\in Ap=\left\{a\right\}\right\}\in \mathrm{V}$$
11	7 8 10	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{Points}\left(K\right)=\left\{p|\exists a\in Ap=\left\{a\right\}\right\}$$
12	2 11	syl5eq	$$⊢K\in \mathrm{V}\to P=\left\{p|\exists a\in Ap=\left\{a\right\}\right\}$$
13	3 12	syl	$$⊢K\in B\to P=\left\{p|\exists a\in Ap=\left\{a\right\}\right\}$$