Theorem llnnlt

Description: Two lattice lines cannot satisfy the less than relation. (Contributed by NM, 26-Jun-2012)

	Ref	Expression
Hypotheses	llnnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	llnnlt.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
Assertion	llnnlt	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \neg X\underset{\dot{}}{<}Y$$

Proof

Step	Hyp	Ref	Expression
1		llnnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		llnnlt.n	$$⊢N=\mathrm{LLines}\left(K\right)$$
3	1	pltirr	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\right)\to \neg X\underset{\dot{}}{<}X$$
4	3	3adant3	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \neg X\underset{\dot{}}{<}X$$
5		breq2	$$⊢X=Y\to \left(X\underset{\dot{}}{<}X\leftrightarrow X\underset{\dot{}}{<}Y\right)$$
6	5	notbid	$$⊢X=Y\to \left(\neg X\underset{\dot{}}{<}X\leftrightarrow \neg X\underset{\dot{}}{<}Y\right)$$
7	4 6	syl5ibcom	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \left(X=Y\to \neg X\underset{\dot{}}{<}Y\right)$$
8		eqid	$$⊢{\le }_K={\le }_K$$
9	8 1	pltle	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \left(X\underset{\dot{}}{<}Y\to X{\le }_{K}Y\right)$$
10	8 2	llncmp	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \left(X{\le }_{K}Y\leftrightarrow X=Y\right)$$
11	9 10	sylibd	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \left(X\underset{\dot{}}{<}Y\to X=Y\right)$$
12	11	necon3ad	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \left(X\ne Y\to \neg X\underset{\dot{}}{<}Y\right)$$
13	7 12	pm2.61dne	$$⊢\left(K\in \mathrm{HL}\wedge X\in N\wedge Y\in N\right)\to \neg X\underset{\dot{}}{<}Y$$