Theorem hsupval

Description: Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 . (Contributed by NM, 9-Dec-2003) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	hsupval	$$⊢A\subseteq 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)=\perp \left(\perp \left(\bigcup A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2	1	pwex	$$⊢𝒫\mathscr{H}\in \mathrm{V}$$
3	2	elpw2	$$⊢A\in 𝒫𝒫\mathscr{H}\leftrightarrow A\subseteq 𝒫\mathscr{H}$$
4		unieq	$$⊢x=A\to \bigcup x=\bigcup A$$
5	4	fveq2d	$$⊢x=A\to \perp \left(\bigcup x\right)=\perp \left(\bigcup A\right)$$
6	5	fveq2d	$$⊢x=A\to \perp \left(\perp \left(\bigcup x\right)\right)=\perp \left(\perp \left(\bigcup A\right)\right)$$
7		df-chsup	$$⊢{\bigvee }_{\mathscr{H}}=\left(x\in 𝒫𝒫\mathscr{H}⟼\perp \left(\perp \left(\bigcup x\right)\right)\right)$$
8		fvex	$$⊢\perp \left(\perp \left(\bigcup A\right)\right)\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢A\in 𝒫𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)=\perp \left(\perp \left(\bigcup A\right)\right)$$
10	3 9	sylbir	$$⊢A\subseteq 𝒫\mathscr{H}\to {\bigvee }_{\mathscr{H}}\left(A\right)=\perp \left(\perp \left(\bigcup A\right)\right)$$