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	$$⊢C={⋖}_K$$
	atncvr.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atncvrN	$$⊢\left(K\in \mathrm{AtLat}\wedge P\in A\wedge Q\in A\right)\to \neg PCQ$$

Proof

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