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 𝐴C
chjcl.2 𝐵C
chlub.1 𝐶C
Assertion chlubii ( ( 𝐴𝐶𝐵𝐶 ) → ( 𝐴 𝐵 ) ⊆ 𝐶 )

Proof

Step Hyp Ref Expression
1 ch0le.1 𝐴C
2 chjcl.2 𝐵C
3 chlub.1 𝐶C
4 1 2 3 chlubi ( ( 𝐴𝐶𝐵𝐶 ) ↔ ( 𝐴 𝐵 ) ⊆ 𝐶 )
5 4 biimpi ( ( 𝐴𝐶𝐵𝐶 ) → ( 𝐴 𝐵 ) ⊆ 𝐶 )