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 
|- SH C_ ~P ~H

Proof

Step Hyp Ref Expression
1 pwuni 
 |-  SH C_ ~P U. SH
2 helsh 
 |-  ~H e. SH
3 shss 
 |-  ( x e. SH -> x C_ ~H )
4 3 rgen 
 |-  A. x e. SH x C_ ~H
5 ssunieq 
 |-  ( ( ~H e. SH /\ A. x e. SH x C_ ~H ) -> ~H = U. SH )
6 2 4 5 mp2an 
 |-  ~H = U. SH
7 6 pweqi 
 |-  ~P ~H = ~P U. SH
8 1 7 sseqtrri 
 |-  SH C_ ~P ~H