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