Theorem atncmp

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

	Ref	Expression
Hypotheses	atcmp.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	atcmp.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atncmp	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(\neg P\underset{\dot{}}{\le }Q\leftrightarrow P\ne Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		atcmp.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		atcmp.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3	1 2	atcmp	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P\underset{\dot{}}{\le }Q\leftrightarrow P=Q\right)$$
4	3	necon3bbid	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(\neg P\underset{\dot{}}{\le }Q\leftrightarrow P\ne Q\right)$$