Description: SH closure of join. (Contributed by NM, 5-May-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | shincl.1 | ⊢ 𝐴 ∈ Sℋ | |
shincl.2 | ⊢ 𝐵 ∈ Sℋ | ||
Assertion | shjshcli | ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Sℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shincl.1 | ⊢ 𝐴 ∈ Sℋ | |
2 | shincl.2 | ⊢ 𝐵 ∈ Sℋ | |
3 | 1 2 | shjcli | ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ |
4 | 3 | chshii | ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Sℋ |