Metamath Proof Explorer


Theorem shjcl

Description: Closure of join in SH . (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion shjcl ( ( 𝐴S𝐵S ) → ( 𝐴 𝐵 ) ∈ C )

Proof

Step Hyp Ref Expression
1 shss ( 𝐴S𝐴 ⊆ ℋ )
2 shss ( 𝐵S𝐵 ⊆ ℋ )
3 sshjcl ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 𝐵 ) ∈ C )
4 1 2 3 syl2an ( ( 𝐴S𝐵S ) → ( 𝐴 𝐵 ) ∈ C )