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

Metamath Proof Explorer

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 HAtoms \to A \neq 0_{ℋ}$

Step	Hyp	Ref	Expression
1		elat2	$⊢ A \in HAtoms \leftrightarrow (A \in C_{ℋ} \land (A \neq 0_{ℋ} \land \forall x \in C_{ℋ} (x \subseteq A \to (x = A \lor x = 0_{ℋ}))))$
2		simprl	$⊢ (A \in C_{ℋ} \land (A \neq 0_{ℋ} \land \forall x \in C_{ℋ} (x \subseteq A \to (x = A \lor x = 0_{ℋ})))) \to A \neq 0_{ℋ}$
3	1 2	sylbi	$⊢ A \in HAtoms \to A \neq 0_{ℋ}$