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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
pointset.p ⊢ 𝑃 = ( Points ‘ 𝐾 )
Assertion pointsetN ( 𝐾 ∈ 𝐵 → 𝑃 = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )

Proof

Step Hyp Ref Expression
1 pointset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 pointset.p ⊢ 𝑃 = ( Points ‘ 𝐾 )
3 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
4 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
5 4 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
6 5 rexeqdv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑎 ∈ ( Atoms ‘ 𝑘 ) 𝑝 = { 𝑎 } ↔ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } ) )
7 6 abbidv ⊢ ( 𝑘 = 𝐾 → { 𝑝 ∣ ∃ 𝑎 ∈ ( Atoms ‘ 𝑘 ) 𝑝 = { 𝑎 } } = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )
8 df-pointsN ⊢ Points = ( 𝑘 ∈ V ↦ { 𝑝 ∣ ∃ 𝑎 ∈ ( Atoms ‘ 𝑘 ) 𝑝 = { 𝑎 } } )
9 1 fvexi ⊢ 𝐴 ∈ V
10 9 abrexex ⊢ { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } ∈ V
11 7 8 10 fvmpt ⊢ ( 𝐾 ∈ V → ( Points ‘ 𝐾 ) = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )
12 2 11 eqtrid ⊢ ( 𝐾 ∈ V → 𝑃 = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )
13 3 12 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝑃 = { 𝑝 ∣ ∃ 𝑎 ∈ 𝐴 𝑝 = { 𝑎 } } )