Theorem hsupunss

Description: The union of a set of Hilbert space subsets is smaller than its supremum. (Contributed by NM, 24-Nov-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sspwuni	|- ( A C_ ~P ~H <-> U. A C_ ~H )
2		ococss	|- ( U. A C_ ~H -> U. A C_ ( _|_ ` ( _|_ ` U. A ) ) )
3	1 2	sylbi	|- ( A C_ ~P ~H -> U. A C_ ( _|_ ` ( _|_ ` U. A ) ) )
4		hsupval	|- ( A C_ ~P ~H -> ( \/H ` A ) = ( _|_ ` ( _|_ ` U. A ) ) )
5	3 4	sseqtrrd	|- ( A C_ ~P ~H -> U. A C_ ( \/H ` A ) )