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

Metamath Proof Explorer

Theorem hsupunss

Description: The union of a set of Hilbert space subsets is smaller than its supremum. (Contributed by NM, 24-Nov-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	hsupunss	$⊢ A \subseteq 𝒫 ℋ \to ⋃ A \subseteq ⋁_{ℋ} (A)$

Proof

Step	Hyp	Ref	Expression
1		sspwuni	$⊢ A \subseteq 𝒫 ℋ \leftrightarrow ⋃ A \subseteq ℋ$
2		ococss	$⊢ ⋃ A \subseteq ℋ \to ⋃ A \subseteq ⊥ (⊥ (⋃ A))$
3	1 2	sylbi	$⊢ A \subseteq 𝒫 ℋ \to ⋃ A \subseteq ⊥ (⊥ (⋃ A))$
4		hsupval	$⊢ A \subseteq 𝒫 ℋ \to ⋁_{ℋ} (A) = ⊥ (⊥ (⋃ A))$
5	3 4	sseqtrrd	$⊢ A \subseteq 𝒫 ℋ \to ⋃ A \subseteq ⋁_{ℋ} (A)$