Metamath Proof Explorer


Theorem chub2i

Description: CH join is an upper bound of two elements. (Contributed by NM, 5-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 𝐴C
chjcl.2 𝐵C
Assertion chub2i 𝐴 ⊆ ( 𝐵 𝐴 )

Proof

Step Hyp Ref Expression
1 ch0le.1 𝐴C
2 chjcl.2 𝐵C
3 1 2 chub1i 𝐴 ⊆ ( 𝐴 𝐵 )
4 1 2 chjcomi ( 𝐴 𝐵 ) = ( 𝐵 𝐴 )
5 3 4 sseqtri 𝐴 ⊆ ( 𝐵 𝐴 )