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

Metamath Proof Explorer

Theorem hsupval

Description: Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 . (Contributed by NM, 9-Dec-2003) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion hsupval 
|- ( A C_ ~P ~H -> ( \/H ` A ) = ( _|_ ` ( _|_ ` U. A ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex 
 |-  ~H e. _V
2 1 pwex 
 |-  ~P ~H e. _V
3 2 elpw2 
 |-  ( A e. ~P ~P ~H <-> A C_ ~P ~H )
4 unieq 
 |-  ( x = A -> U. x = U. A )
5 4 fveq2d 
 |-  ( x = A -> ( _|_ ` U. x ) = ( _|_ ` U. A ) )
6 5 fveq2d 
 |-  ( x = A -> ( _|_ ` ( _|_ ` U. x ) ) = ( _|_ ` ( _|_ ` U. A ) ) )
7 df-chsup 
 |-  \/H = ( x e. ~P ~P ~H |-> ( _|_ ` ( _|_ ` U. x ) ) )
8 fvex 
 |-  ( _|_ ` ( _|_ ` U. A ) ) e. _V
9 6 7 8 fvmpt 
 |-  ( A e. ~P ~P ~H -> ( \/H ` A ) = ( _|_ ` ( _|_ ` U. A ) ) )
10 3 9 sylbir 
 |-  ( A C_ ~P ~H -> ( \/H ` A ) = ( _|_ ` ( _|_ ` U. A ) ) )