Metamath Proof Explorer


Theorem chlubi

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

Ref Expression
Hypotheses ch0le.1
|- A e. CH
chjcl.2
|- B e. CH
chlub.1
|- C e. CH
Assertion chlubi
|- ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C )

Proof

Step Hyp Ref Expression
1 ch0le.1
 |-  A e. CH
2 chjcl.2
 |-  B e. CH
3 chlub.1
 |-  C e. CH
4 1 chshii
 |-  A e. SH
5 2 chshii
 |-  B e. SH
6 4 5 3 shlubi
 |-  ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C )