Metamath Proof Explorer


Theorem atnlt

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

Ref Expression
Hypotheses atnlt.s < = ( lt ‘ 𝐾 )
atnlt.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atnlt ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ¬ 𝑃 < 𝑄 )

Proof

Step Hyp Ref Expression
1 atnlt.s < = ( lt ‘ 𝐾 )
2 atnlt.a 𝐴 = ( Atoms ‘ 𝐾 )
3 1 pltirr ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴 ) → ¬ 𝑃 < 𝑃 )
4 3 3adant3 ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ¬ 𝑃 < 𝑃 )
5 breq2 ( 𝑃 = 𝑄 → ( 𝑃 < 𝑃𝑃 < 𝑄 ) )
6 5 notbid ( 𝑃 = 𝑄 → ( ¬ 𝑃 < 𝑃 ↔ ¬ 𝑃 < 𝑄 ) )
7 4 6 syl5ibcom ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 = 𝑄 → ¬ 𝑃 < 𝑄 ) )
8 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 8 1 pltle ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 < 𝑄𝑃 ( le ‘ 𝐾 ) 𝑄 ) )
10 8 2 atcmp ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 ( le ‘ 𝐾 ) 𝑄𝑃 = 𝑄 ) )
11 9 10 sylibd ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 < 𝑄𝑃 = 𝑄 ) )
12 11 necon3ad ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃𝑄 → ¬ 𝑃 < 𝑄 ) )
13 7 12 pm2.61dne ( ( 𝐾 ∈ AtLat ∧ 𝑃𝐴𝑄𝐴 ) → ¬ 𝑃 < 𝑄 )