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

Metamath Proof Explorer

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