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 = (
	atncvr.a	|- A = ( Atoms ` K )
Assertion	atncvrN	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> -. P C Q )

Proof

Step	Hyp	Ref	Expression
1		atncvr.c	|- C = (
2		atncvr.a	|- A = ( Atoms ` K )
3		eqid	|- ( 0. ` K ) = ( 0. ` K )
4	3 2	atn0	|- ( ( K e. AtLat /\ P e. A ) -> P =/= ( 0. ` K ) )
5	4	3adant3	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> P =/= ( 0. ` K ) )
6		eqid	|- ( Base ` K ) = ( Base ` K )
7	6 2	atbase	|- ( P e. A -> P e. ( Base ` K ) )
8		eqid	|- ( le ` K ) = ( le ` K )
9	6 8 3 1 2	atcvreq0	|- ( ( K e. AtLat /\ P e. ( Base ` K ) /\ Q e. A ) -> ( P C Q <-> P = ( 0. ` K ) ) )
10	7 9	syl3an2	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P C Q <-> P = ( 0. ` K ) ) )
11	10	necon3bbid	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( -. P C Q <-> P =/= ( 0. ` K ) ) )
12	5 11	mpbird	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> -. P C Q )