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 A 𝒫 A = x C | A x

Proof

Step Hyp Ref Expression
1 hsupval A 𝒫 A = A
2 sspwuni A 𝒫 A
3 ococin A A = x C | A x
4 2 3 sylbi A 𝒫 A = x C | A x
5 1 4 eqtrd A 𝒫 A = x C | A x