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 ∈ B → P = p | ∃ a ∈ A p = a

Proof

Step Hyp Ref Expression
1 pointset.a ⊢ A = Atoms ⁡ K
2 pointset.p ⊢ P = Points ⁡ K
3 elex ⊢ K ∈ B → K ∈ V
4 fveq2 ⊢ k = K → Atoms ⁡ k = Atoms ⁡ K
5 4 1 eqtr4di ⊢ k = K → Atoms ⁡ k = A
6 5 rexeqdv ⊢ k = K → ∃ a ∈ Atoms ⁡ k p = a ↔ ∃ a ∈ A p = a
7 6 abbidv ⊢ k = K → p | ∃ a ∈ Atoms ⁡ k p = a = p | ∃ a ∈ A p = a
8 df-pointsN ⊢ Points = k ∈ V ⟼ p | ∃ a ∈ Atoms ⁡ k p = a
9 1 fvexi ⊢ A ∈ V
10 9 abrexex ⊢ p | ∃ a ∈ A p = a ∈ V
11 7 8 10 fvmpt ⊢ K ∈ V → Points ⁡ K = p | ∃ a ∈ A p = a
12 2 11 eqtrid ⊢ K ∈ V → P = p | ∃ a ∈ A p = a
13 3 12 syl ⊢ K ∈ B → P = p | ∃ a ∈ A p = a