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 )