Theorem atne0

Description: An atom is not the Hilbert lattice zero. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	atne0	$$⊢A\in \mathrm{HAtoms}\to A\ne 0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		elat2	$$⊢A\in \mathrm{HAtoms}\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(A\ne 0_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)\right)$$
2		simprl	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(A\ne 0_{\mathscr{H}}\wedge \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq A\to \left(x=A\vee x=0_{\mathscr{H}}\right)\right)\right)\right)\to A\ne 0_{\mathscr{H}}$$
3	1 2	sylbi	$$⊢A\in \mathrm{HAtoms}\to A\ne 0_{\mathscr{H}}$$