Theorem hsupval2

Description: Alternate definition of supremum of a subset of the Hilbert lattice. Definition of supremum in Proposition 1 of Kalmbach p. 65. We actually define it on any collection of Hilbert space subsets, not just the Hilbert lattice CH , to allow more general theorems. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	hsupval2	$$⊢A\subseteq 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)=\bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup A\subseteq x\right\}$$

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		ococin	$$⊢\bigcup A\subseteq \mathscr{H}\to \perp \left(\perp \left(\bigcup A\right)\right)=\bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup A\subseteq x\right\}$$
4	2 3	sylbi	$$⊢A\subseteq 𝒫\mathscr{H}\to \perp \left(\perp \left(\bigcup A\right)\right)=\bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup A\subseteq x\right\}$$
5	1 4	eqtrd	$$⊢A\subseteq 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)=\bigcap \left\{x\in {\mathbf{C}}_{\mathscr{H}}|\bigcup A\subseteq x\right\}$$