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ℋ ∣ ∪ 𝐴 ⊆ 𝑥 } )