atncvrN

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

	Ref	Expression
Hypotheses	atncvr.c	$⊢ C = ⋖_{K}$
	atncvr.a	$⊢ A = Atoms (K)$
Assertion	atncvrN	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to \neg P C Q$

Step	Hyp	Ref	Expression
1		atncvr.c	$⊢ C = ⋖_{K}$
2		atncvr.a	$⊢ A = Atoms (K)$
3		eqid	$⊢ 0. (K) = 0. (K)$
4	3 2	atn0	$⊢ (K \in AtLat \land P \in A) \to P \neq 0. (K)$
5	4	3adant3	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to P \neq 0. (K)$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9	6 8 3 1 2	atcvreq0	$⊢ (K \in AtLat \land P \in {Base}_{K} \land Q \in A) \to (P C Q \leftrightarrow P = 0. (K))$
10	7 9	syl3an2	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P C Q \leftrightarrow P = 0. (K))$
11	10	necon3bbid	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (\neg P C Q \leftrightarrow P \neq 0. (K))$
12	5 11	mpbird	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to \neg P C Q$

Metamath Proof Explorer