Metamath Proof Explorer


Theorem chj1i

Description: Join with Hilbert lattice unit. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1
|- A e. CH
Assertion chj1i
|- ( A vH ~H ) = ~H

Proof

Step Hyp Ref Expression
1 ch0le.1
 |-  A e. CH
2 helch
 |-  ~H e. CH
3 1 2 chjcli
 |-  ( A vH ~H ) e. CH
4 3 chssii
 |-  ( A vH ~H ) C_ ~H
5 2 1 chub2i
 |-  ~H C_ ( A vH ~H )
6 4 5 eqssi
 |-  ( A vH ~H ) = ~H