Metamath Proof Explorer

Theorem chnlen0

Description: A Hilbert lattice element that is not a subset of another is nonzero. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion chnlen0 
|- ( B e. CH -> ( -. A C_ B -> -. A = 0H ) )

Proof

Step Hyp Ref Expression
1 ch0le 
 |-  ( B e. CH -> 0H C_ B )
2 sseq1 
 |-  ( A = 0H -> ( A C_ B <-> 0H C_ B ) )
3 1 2 syl5ibrcom 
 |-  ( B e. CH -> ( A = 0H -> A C_ B ) )
4 3 con3d 
 |-  ( B e. CH -> ( -. A C_ B -> -. A = 0H ) )