This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chsspwh

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

		Ref	Expression
	Assertion	chsspwh	$⊢ C_{ℋ} \subseteq 𝒫 ℋ$

Step	Hyp	Ref	Expression
1		chsssh	$⊢ C_{ℋ} \subseteq S_{ℋ}$
2		shsspwh	$⊢ S_{ℋ} \subseteq 𝒫 ℋ$
3	1 2	sstri	$⊢ C_{ℋ} \subseteq 𝒫 ℋ$