Metamath Proof Explorer


Theorem chlubii

Description: Hilbert lattice join is the least upper bound of two elements (one direction of chlubi ). (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1
|- A e. CH
chjcl.2
|- B e. CH
chlub.1
|- C e. CH
Assertion chlubii
|- ( ( 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 2 3 chlubi
 |-  ( ( A C_ C /\ B C_ C ) <-> ( A vH B ) C_ C )
5 4 biimpi
 |-  ( ( A C_ C /\ B C_ C ) -> ( A vH B ) C_ C )