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 ( 𝐴 ⊆ 𝒫 ℋ → 𝐴 ⊆ ( 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sspwuni ( 𝐴 ⊆ 𝒫 ℋ ↔ 𝐴 ⊆ ℋ )
2 ococss ( 𝐴 ⊆ ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
3 1 2 sylbi ( 𝐴 ⊆ 𝒫 ℋ → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
4 hsupval ( 𝐴 ⊆ 𝒫 ℋ → ( 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) )
5 3 4 sseqtrrd ( 𝐴 ⊆ 𝒫 ℋ → 𝐴 ⊆ ( 𝐴 ) )