# Metamath Proof Explorer

## Theorem chlej1

Description: Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chlej1 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge {A}\subseteq {B}\right)\to {A}{\vee }_{ℋ}{C}\subseteq {B}{\vee }_{ℋ}{C}$

### Proof

Step Hyp Ref Expression
1 chsh ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to {A}\in {\mathbf{S}}_{ℋ}$
2 chsh ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to {B}\in {\mathbf{S}}_{ℋ}$
3 chsh ${⊢}{C}\in {\mathbf{C}}_{ℋ}\to {C}\in {\mathbf{S}}_{ℋ}$
4 shlej1 ${⊢}\left(\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{S}}_{ℋ}\right)\wedge {A}\subseteq {B}\right)\to {A}{\vee }_{ℋ}{C}\subseteq {B}{\vee }_{ℋ}{C}$
5 1 2 3 4 syl3anl ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge {A}\subseteq {B}\right)\to {A}{\vee }_{ℋ}{C}\subseteq {B}{\vee }_{ℋ}{C}$