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 A 𝒫 span A S

Proof

Step Hyp Ref Expression
1 uniss A 𝒫 A 𝒫
2 unipw 𝒫 =
3 1 2 sseqtrdi A 𝒫 A
4 spancl A span A S
5 3 4 syl A 𝒫 span A S