This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ¬ 𝑃 < 𝑄 )