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

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_{ℋ} \subseteq 𝒫 ℋ$

Step	Hyp	Ref	Expression
1		pwuni	$⊢ S_{ℋ} \subseteq 𝒫 ⋃ S_{ℋ}$
2		helsh	$⊢ ℋ \in S_{ℋ}$
3		shss	$⊢ x \in S_{ℋ} \to x \subseteq ℋ$
4	3	rgen	$⊢ \forall x \in S_{ℋ} x \subseteq ℋ$
5		ssunieq	$⊢ (ℋ \in S_{ℋ} \land \forall x \in S_{ℋ} x \subseteq ℋ) \to ℋ = ⋃ S_{ℋ}$
6	2 4 5	mp2an	$⊢ ℋ = ⋃ S_{ℋ}$
7	6	pweqi	$⊢ 𝒫 ℋ = 𝒫 ⋃ S_{ℋ}$
8	1 7	sseqtrri	$⊢ S_{ℋ} \subseteq 𝒫 ℋ$