This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chj1i

Description: Join with Hilbert lattice one. (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