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\in {\mathbf{C}}_{\mathscr{H}}\to \left(\neg A\subseteq B\to \neg A=0_{\mathscr{H}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ch0le	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to 0_{\mathscr{H}}\subseteq B$$
2		sseq1	$$⊢A=0_{\mathscr{H}}\to \left(A\subseteq B\leftrightarrow 0_{\mathscr{H}}\subseteq B\right)$$
3	1 2	syl5ibrcom	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(A=0_{\mathscr{H}}\to A\subseteq B\right)$$
4	3	con3d	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\neg A\subseteq B\to \neg A=0_{\mathscr{H}}\right)$$