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

Metamath Proof Explorer

Theorem sshjcl

Description: Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000) (New usage is discouraged.)

Ref Expression
Assertion sshjcl 
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) e. CH )

Proof

Step Hyp Ref Expression
1 sshjval 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
2 unss 
 |-  ( ( A C_ ~H /\ B C_ ~H ) <-> ( A u. B ) C_ ~H )
3 ocss 
 |-  ( ( A u. B ) C_ ~H -> ( _|_ ` ( A u. B ) ) C_ ~H )
4 occl 
 |-  ( ( _|_ ` ( A u. B ) ) C_ ~H -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) e. CH )
5 3 4 syl 
 |-  ( ( A u. B ) C_ ~H -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) e. CH )
6 2 5 sylbi 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) e. CH )
7 1 6 eqeltrd 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) e. CH )