Metamath Proof Explorer


Theorem shsspwh

Description: Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

Ref Expression
Assertion shsspwh S ⊆ 𝒫 ℋ

Proof

Step Hyp Ref Expression
1 pwuni S ⊆ 𝒫 S
2 helsh ℋ ∈ S
3 shss ( 𝑥S𝑥 ⊆ ℋ )
4 3 rgen 𝑥S 𝑥 ⊆ ℋ
5 ssunieq ( ( ℋ ∈ S ∧ ∀ 𝑥S 𝑥 ⊆ ℋ ) → ℋ = S )
6 2 4 5 mp2an ℋ = S
7 6 pweqi 𝒫 ℋ = 𝒫 S
8 1 7 sseqtrri S ⊆ 𝒫 ℋ