This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } } )