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 = ( Atoms ` K )
	pointset.p	|- P = ( Points ` K )
Assertion	pointsetN	|- ( K e. B -> P = { p | E. a e. A p = { a } } )

Proof

Step	Hyp	Ref	Expression
1		pointset.a	|- A = ( Atoms ` K )
2		pointset.p	|- P = ( Points ` K )
3		elex	|- ( K e. B -> K e. _V )
4		fveq2	|- ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
5	4 1	eqtr4di	|- ( k = K -> ( Atoms ` k ) = A )
6	5	rexeqdv	|- ( k = K -> ( E. a e. ( Atoms ` k ) p = { a } <-> E. a e. A p = { a } ) )
7	6	abbidv	|- ( k = K -> { p | E. a e. ( Atoms ` k ) p = { a } } = { p | E. a e. A p = { a } } )
8		df-pointsN	|- Points = ( k e. _V |-> { p | E. a e. ( Atoms ` k ) p = { a } } )
9	1	fvexi	|- A e. _V
10	9	abrexex	|- { p | E. a e. A p = { a } } e. _V
11	7 8 10	fvmpt	|- ( K e. _V -> ( Points ` K ) = { p | E. a e. A p = { a } } )
12	2 11	eqtrid	|- ( K e. _V -> P = { p | E. a e. A p = { a } } )
13	3 12	syl	|- ( K e. B -> P = { p | E. a e. A p = { a } } )