Metamath Proof Explorer

Theorem shex

Description: The set of subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion shex 
|- SH e. _V

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 1 pwex 
 |-  ~P ~H e. _V
3 shss 
 |-  ( x e. SH -> x C_ ~H )
4 velpw 
 |-  ( x e. ~P ~H <-> x C_ ~H )
5 3 4 sylibr 
 |-  ( x e. SH -> x e. ~P ~H )
6 5 ssriv 
 |-  SH C_ ~P ~H
7 2 6 ssexi 
 |-  SH e. _V