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	⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) ∈ Cℋ )

Proof

Step	Hyp	Ref	Expression
1		hsupval	⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) = ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) )
2		sspwuni	⊢ ( 𝐴 ⊆ 𝒫 ℋ ↔ ∪ 𝐴 ⊆ ℋ )
3		ocss	⊢ ( ∪ 𝐴 ⊆ ℋ → ( ⊥ ‘ ∪ 𝐴 ) ⊆ ℋ )
4		occl	⊢ ( ( ⊥ ‘ ∪ 𝐴 ) ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ∈ Cℋ )
5	3 4	syl	⊢ ( ∪ 𝐴 ⊆ ℋ → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ∈ Cℋ )
6	2 5	sylbi	⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ⊥ ‘ ( ⊥ ‘ ∪ 𝐴 ) ) ∈ Cℋ )
7	1 6	eqeltrd	⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘ 𝐴 ) ∈ Cℋ )