Metamath Proof Explorer


Theorem llnnlt

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

Ref Expression
Hypotheses llnnlt.s < ˙ = < K
llnnlt.n N = LLines K
Assertion llnnlt K HL X N Y N ¬ X < ˙ Y

Proof

Step Hyp Ref Expression
1 llnnlt.s < ˙ = < K
2 llnnlt.n N = LLines K
3 1 pltirr K HL X N ¬ X < ˙ X
4 3 3adant3 K HL X N Y N ¬ X < ˙ X
5 breq2 X = Y X < ˙ X X < ˙ Y
6 5 notbid X = Y ¬ X < ˙ X ¬ X < ˙ Y
7 4 6 syl5ibcom K HL X N Y N X = Y ¬ X < ˙ Y
8 eqid K = K
9 8 1 pltle K HL X N Y N X < ˙ Y X K Y
10 8 2 llncmp K HL X N Y N X K Y X = Y
11 9 10 sylibd K HL X N Y N X < ˙ Y X = Y
12 11 necon3ad K HL X N Y N X Y ¬ X < ˙ Y
13 7 12 pm2.61dne K HL X N Y N ¬ X < ˙ Y