Theorem atncvrN

Description: Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atncvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	atncvr.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atncvrN	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ¬ 𝑃 𝐶 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		atncvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
2		atncvr.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
4	3 2	atn0	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≠ ( 0. ‘ 𝐾 ) )
5	4	3adant3	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ≠ ( 0. ‘ 𝐾 ) )
6		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7	6 2	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
8		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9	6 8 3 1 2	atcvreq0	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 𝐶 𝑄 ↔ 𝑃 = ( 0. ‘ 𝐾 ) ) )
10	7 9	syl3an2	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 𝐶 𝑄 ↔ 𝑃 = ( 0. ‘ 𝐾 ) ) )
11	10	necon3bbid	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ¬ 𝑃 𝐶 𝑄 ↔ 𝑃 ≠ ( 0. ‘ 𝐾 ) ) )
12	5 11	mpbird	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ¬ 𝑃 𝐶 𝑄 )