hsupcl

Description: Closure of supremum of set of subsets of Hilbert space. Note that the supremum belongs to CH even if the subsets do not. (Contributed by NM, 10-Nov-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	hsupcl	$⊢ A \subseteq 𝒫 ℋ \to ⋁_{ℋ} (A) \in C_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		hsupval	$⊢ A \subseteq 𝒫 ℋ \to ⋁_{ℋ} (A) = ⊥ (⊥ (⋃ A))$
2		sspwuni	$⊢ A \subseteq 𝒫 ℋ \leftrightarrow ⋃ A \subseteq ℋ$
3		ocss	$⊢ ⋃ A \subseteq ℋ \to ⊥ (⋃ A) \subseteq ℋ$
4		occl	$⊢ ⊥ (⋃ A) \subseteq ℋ \to ⊥ (⊥ (⋃ A)) \in C_{ℋ}$
5	3 4	syl	$⊢ ⋃ A \subseteq ℋ \to ⊥ (⊥ (⋃ A)) \in C_{ℋ}$
6	2 5	sylbi	$⊢ A \subseteq 𝒫 ℋ \to ⊥ (⊥ (⋃ A)) \in C_{ℋ}$
7	1 6	eqeltrd	$⊢ A \subseteq 𝒫 ℋ \to ⋁_{ℋ} (A) \in C_{ℋ}$

Metamath Proof Explorer

Theorem hsupcl

Proof