This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shsupcl

Description: Closure of the subspace supremum of set of subsets of Hilbert space. (Contributed by NM, 26-Nov-2004) (New usage is discouraged.)

Ref Expression
Assertion shsupcl ( 𝐴 ⊆ 𝒫 ℋ → ( span ‘ ∪ 𝐴 ) ∈ Sℋ )

Proof

Step Hyp Ref Expression
1 uniss ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ∪ 𝐴 ⊆ ∪ 𝒫 ℋ )
2 unipw ⊢ ∪ 𝒫 ℋ = ℋ
3 1 2 sseqtrdi ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ∪ 𝐴 ⊆ ℋ )
4 spancl ⊢ ( ∪ 𝐴 ⊆ ℋ → ( span ‘ ∪ 𝐴 ) ∈ Sℋ )
5 3 4 syl ⊢ ( 𝐴 ⊆ 𝒫 ℋ → ( span ‘ ∪ 𝐴 ) ∈ Sℋ )