Metamath Proof Explorer
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ℋ ) |