# Metamath Proof Explorer

## Theorem chlub

Description: Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

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

### 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 shlub ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}{\vee }_{ℋ}{B}\subseteq {C}\right)$
4 2 3 syl3an2 ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}{\vee }_{ℋ}{B}\subseteq {C}\right)$
5 1 4 syl3an1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}{\vee }_{ℋ}{B}\subseteq {C}\right)$