Metamath Proof Explorer

Theorem chm0i

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

Ref Expression
Hypothesis ch0le.1 
|- A e. CH
Assertion chm0i 
|- ( A i^i 0H ) = 0H

Proof

Step Hyp Ref Expression
1 ch0le.1 
 |-  A e. CH
2 inss2 
 |-  ( A i^i 0H ) C_ 0H
3 1 ch0lei 
 |-  0H C_ A
4 ssid 
 |-  0H C_ 0H
5 3 4 ssini 
 |-  0H C_ ( A i^i 0H )
6 2 5 eqssi 
 |-  ( A i^i 0H ) = 0H