Theorem hsupval2

Description: Alternate definition of supremum of a subset of the Hilbert lattice. Definition of supremum in Proposition 1 of Kalmbach p. 65. We actually define it on any collection of Hilbert space subsets, not just the Hilbert lattice CH , to allow more general theorems. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	hsupval2	|- ( A C_ ~P ~H -> ( \/H ` A ) = |^| { x e. CH | U. A C_ x } )

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		ococin	|- ( U. A C_ ~H -> ( _|_ ` ( _|_ ` U. A ) ) = |^| { x e. CH | U. A C_ x } )
4	2 3	sylbi	|- ( A C_ ~P ~H -> ( _|_ ` ( _|_ ` U. A ) ) = |^| { x e. CH | U. A C_ x } )
5	1 4	eqtrd	|- ( A C_ ~P ~H -> ( \/H ` A ) = |^| { x e. CH | U. A C_ x } )