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

Metamath Proof Explorer

Theorem chsupunss

Description: The union of a set of closed subspaces is smaller than its supremum. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		chsspwh	$⊢ C_{ℋ} \subseteq 𝒫 ℋ$
2		sstr	$⊢ (A \subseteq C_{ℋ} \land C_{ℋ} \subseteq 𝒫 ℋ) \to A \subseteq 𝒫 ℋ$
3	1 2	mpan2	$⊢ A \subseteq C_{ℋ} \to A \subseteq 𝒫 ℋ$
4		hsupunss	$⊢ A \subseteq 𝒫 ℋ \to ⋃ A \subseteq ⋁_{ℋ} (A)$
5	3 4	syl	$⊢ A \subseteq C_{ℋ} \to ⋃ A \subseteq ⋁_{ℋ} (A)$