Metamath Proof Explorer


Theorem chjvali

Description: Value of join in CH . (Contributed by NM, 9-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses chjval.1
|- A e. CH
chjval.2
|- B e. CH
Assertion chjvali
|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 chjval.1
 |-  A e. CH
2 chjval.2
 |-  B e. CH
3 chjval
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
4 1 2 3 mp2an
 |-  ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) )