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 B A B C

Proof

Step Hyp Ref Expression
1 sshjval A B A B = A B
2 unss A B A B
3 ocss A B A B
4 occl A B A B C
5 3 4 syl A B A B C
6 2 5 sylbi A B A B C
7 1 6 eqeltrd A B A B C