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

Metamath Proof Explorer

Theorem hsupval2

Description: Alternate definition of supremum of a subset of the Hilbert lattice. Definition of supremum in Proposition 1 of Kalmbach p. 65. We actually define it on any collection of Hilbert space subsets, not just the Hilbert lattice CH , to allow more general theorems. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion hsupval2 ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ∩ { 𝑥 ∈ Cℋ ∣ ∪ 𝐴 ⊆ 𝑥 } )

Proof

Step Hyp Ref Expression
1 hsupval ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) )
2 sspwuni ⊢ ( 𝐴 ⊆ 𝒫 ℋ ↔ ∪ 𝐴 ⊆ ℋ )
3 ococin ⊢ ( ∪ 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) = ∩ { 𝑥 ∈ Cℋ ∣ ∪ 𝐴 ⊆ 𝑥 } )
4 2 3 sylbi ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) = ∩ { 𝑥 ∈ Cℋ ∣ ∪ 𝐴 ⊆ 𝑥 } )
5 1 4 eqtrd ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ∩ { 𝑥 ∈ Cℋ ∣ ∪ 𝐴 ⊆ 𝑥 } )