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

Metamath Proof Explorer

Theorem atncmp

Description: Frequently-used variation of atcmp . (Contributed by NM, 29-Jun-2012)

Ref Expression
Hypotheses atcmp.l ⊢ ≤ = ( le ‘ 𝐾 )
atcmp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atncmp ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑄 ↔ 𝑃 ≠ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 atcmp.l ⊢ ≤ = ( le ‘ 𝐾 )
2 atcmp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 1 2 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄 ) )
4 3 necon3bbid ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑄 ↔ 𝑃 ≠ 𝑄 ) )