Metamath Proof Explorer


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
|- ( A C_ ~P ~H -> ( \/H ` A ) e. CH )

Proof

Step Hyp Ref Expression
1 hsupval
 |-  ( A C_ ~P ~H -> ( \/H ` A ) = ( _|_ ` ( _|_ ` U. A ) ) )
2 sspwuni
 |-  ( A C_ ~P ~H <-> U. A C_ ~H )
3 ocss
 |-  ( U. A C_ ~H -> ( _|_ ` U. A ) C_ ~H )
4 occl
 |-  ( ( _|_ ` U. A ) C_ ~H -> ( _|_ ` ( _|_ ` U. A ) ) e. CH )
5 3 4 syl
 |-  ( U. A C_ ~H -> ( _|_ ` ( _|_ ` U. A ) ) e. CH )
6 2 5 sylbi
 |-  ( A C_ ~P ~H -> ( _|_ ` ( _|_ ` U. A ) ) e. CH )
7 1 6 eqeltrd
 |-  ( A C_ ~P ~H -> ( \/H ` A ) e. CH )