Theorem shsspwh

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

	Ref	Expression
Assertion	shsspwh	$$⊢{\mathbf{S}}_{\mathscr{H}}\subseteq 𝒫\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		pwuni	$$⊢{\mathbf{S}}_{\mathscr{H}}\subseteq 𝒫\bigcup {\mathbf{S}}_{\mathscr{H}}$$
2		helsh	$$⊢\mathscr{H}\in {\mathbf{S}}_{\mathscr{H}}$$
3		shss	$$⊢x\in {\mathbf{S}}_{\mathscr{H}}\to x\subseteq \mathscr{H}$$
4	3	rgen	$$⊢\forall x\in {\mathbf{S}}_{\mathscr{H}}x\subseteq \mathscr{H}$$
5		ssunieq	$$⊢\left(\mathscr{H}\in {\mathbf{S}}_{\mathscr{H}}\wedge \forall x\in {\mathbf{S}}_{\mathscr{H}}x\subseteq \mathscr{H}\right)\to \mathscr{H}=\bigcup {\mathbf{S}}_{\mathscr{H}}$$
6	2 4 5	mp2an	$$⊢\mathscr{H}=\bigcup {\mathbf{S}}_{\mathscr{H}}$$
7	6	pweqi	$$⊢𝒫\mathscr{H}=𝒫\bigcup {\mathbf{S}}_{\mathscr{H}}$$
8	1 7	sseqtrri	$$⊢{\mathbf{S}}_{\mathscr{H}}\subseteq 𝒫\mathscr{H}$$