Theorem atnlt

Description: Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	atnlt.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atnlt	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \neg P\underset{\dot{}}{<}Q$$

Proof

Step	Hyp	Ref	Expression
1		atnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		atnlt.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
3	1	pltirr	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\right)\to \neg P\underset{\dot{}}{<}P$$
4	3	3adant3	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \neg P\underset{\dot{}}{<}P$$
5		breq2	$$⊢P=Q\to \left(P\underset{\dot{}}{<}P\leftrightarrow P\underset{\dot{}}{<}Q\right)$$
6	5	notbid	$$⊢P=Q\to \left(\neg P\underset{\dot{}}{<}P\leftrightarrow \neg P\underset{\dot{}}{<}Q\right)$$
7	4 6	syl5ibcom	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P=Q\to \neg P\underset{\dot{}}{<}Q\right)$$
8		eqid	$$⊢{\le }_K={\le }_K$$
9	8 1	pltle	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P\underset{\dot{}}{<}Q\to P{\le }_{K}Q\right)$$
10	8 2	atcmp	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P{\le }_{K}Q\leftrightarrow P=Q\right)$$
11	9 10	sylibd	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P\underset{\dot{}}{<}Q\to P=Q\right)$$
12	11	necon3ad	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \left(P\ne Q\to \neg P\underset{\dot{}}{<}Q\right)$$
13	7 12	pm2.61dne	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \neg P\underset{\dot{}}{<}Q$$