atn0

Description: An atom is not zero. ( atne0 analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atne0.z	$⊢ \underset{˙}{0} = 0. (K)$
	atne0.a	$⊢ A = Atoms (K)$
Assertion	atn0	$⊢ (K \in AtLat \land P \in A) \to P \neq \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		atne0.z	$⊢ \underset{˙}{0} = 0. (K)$
2		atne0.a	$⊢ A = Atoms (K)$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5	3 4 1 2	isat3	$⊢ K \in AtLat \to (P \in A \leftrightarrow (P \in {Base}_{K} \land P \neq \underset{˙}{0} \land \forall x \in {Base}_{K} (x \leq_{K} P \to (x = P \lor x = \underset{˙}{0}))))$
6		simp2	$⊢ (P \in {Base}_{K} \land P \neq \underset{˙}{0} \land \forall x \in {Base}_{K} (x \leq_{K} P \to (x = P \lor x = \underset{˙}{0}))) \to P \neq \underset{˙}{0}$
7	5 6	biimtrdi	$⊢ K \in AtLat \to (P \in A \to P \neq \underset{˙}{0})$
8	7	imp	$⊢ (K \in AtLat \land P \in A) \to P \neq \underset{˙}{0}$

Metamath Proof Explorer