Metamath Proof Explorer


Theorem hsupunss

Description: The union of a set of Hilbert space subsets is smaller than its supremum. (Contributed by NM, 24-Nov-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hsupunss A 𝒫 A A

Proof

Step Hyp Ref Expression
1 sspwuni A 𝒫 A
2 ococss A A A
3 1 2 sylbi A 𝒫 A A
4 hsupval A 𝒫 A = A
5 3 4 sseqtrrd A 𝒫 A A