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