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 ) |
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 ) |