Metamath Proof Explorer


Theorem chdmj4i

Description: De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 𝐴C
chjcl.2 𝐵C
Assertion chdmj4i ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 ch0le.1 𝐴C
2 chjcl.2 𝐵C
3 2 choccli ( ⊥ ‘ 𝐵 ) ∈ C
4 1 3 chdmj2i ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
5 2 pjococi ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵
6 5 ineq2i ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴𝐵 )
7 4 6 eqtri ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴𝐵 )