Theorem 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 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		hsupval	$$⊢A\subseteq 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)=\perp \left(\perp \left(\bigcup A\right)\right)$$
2		sspwuni	$$⊢A\subseteq 𝒫\mathscr{H}\leftrightarrow \bigcup A\subseteq \mathscr{H}$$
3		ocss	$$⊢\bigcup A\subseteq \mathscr{H}\to \perp \left(\bigcup A\right)\subseteq \mathscr{H}$$
4		occl	$$⊢\perp \left(\bigcup A\right)\subseteq \mathscr{H}\to \perp \left(\perp \left(\bigcup A\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	3 4	syl	$$⊢\bigcup A\subseteq \mathscr{H}\to \perp \left(\perp \left(\bigcup A\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	2 5	sylbi	$$⊢A\subseteq 𝒫\mathscr{H}\to \perp \left(\perp \left(\bigcup A\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	1 6	eqeltrd	$$⊢A\subseteq 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$