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

Metamath Proof Explorer

Theorem atncmp

Description: Frequently-used variation of atcmp . (Contributed by NM, 29-Jun-2012)

	Ref	Expression
Hypotheses	atcmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atcmp.a	$⊢ A = Atoms (K)$
Assertion	atncmp	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (\neg P \underset{˙}{\leq} Q \leftrightarrow P \neq Q)$

Step	Hyp	Ref	Expression
1		atcmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		atcmp.a	$⊢ A = Atoms (K)$
3	1 2	atcmp	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \underset{˙}{\leq} Q \leftrightarrow P = Q)$
4	3	necon3bbid	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (\neg P \underset{˙}{\leq} Q \leftrightarrow P \neq Q)$