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

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 ( 𝐵 ∈ Cℋ → ( ¬ 𝐴 ⊆ 𝐵 → ¬ 𝐴 = 0ℋ ) )

Proof

Step Hyp Ref Expression
1 ch0le ⊢ ( 𝐵 ∈ Cℋ → 0ℋ ⊆ 𝐵 )
2 sseq1 ⊢ ( 𝐴 = 0ℋ → ( 𝐴 ⊆ 𝐵 ↔ 0ℋ ⊆ 𝐵 ) )
3 1 2 syl5ibrcom ⊢ ( 𝐵 ∈ Cℋ → ( 𝐴 = 0ℋ → 𝐴 ⊆ 𝐵 ) )
4 3 con3d ⊢ ( 𝐵 ∈ Cℋ → ( ¬ 𝐴 ⊆ 𝐵 → ¬ 𝐴 = 0ℋ ) )