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 𝒫\mathscr{H}\to \bigcup A\subseteq {\bigvee }_{\mathscr{H}}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		sspwuni	$$⊢A\subseteq 𝒫\mathscr{H}\leftrightarrow \bigcup A\subseteq \mathscr{H}$$
2		ococss	$$⊢\bigcup A\subseteq \mathscr{H}\to \bigcup A\subseteq \perp \left(\perp \left(\bigcup A\right)\right)$$
3	1 2	sylbi	$$⊢A\subseteq 𝒫\mathscr{H}\to \bigcup A\subseteq \perp \left(\perp \left(\bigcup A\right)\right)$$
4		hsupval	$$⊢A\subseteq 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)=\perp \left(\perp \left(\bigcup A\right)\right)$$
5	3 4	sseqtrrd	$$⊢A\subseteq 𝒫\mathscr{H}\to \bigcup A\subseteq {\bigvee }_{\mathscr{H}}\left(A\right)$$