Metamath Proof Explorer


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=AtomsK
Assertion atncvrN KAtLatPAQA¬PCQ

Proof

Step Hyp Ref Expression
1 atncvr.c C=K
2 atncvr.a A=AtomsK
3 eqid 0.K=0.K
4 3 2 atn0 KAtLatPAP0.K
5 4 3adant3 KAtLatPAQAP0.K
6 eqid BaseK=BaseK
7 6 2 atbase PAPBaseK
8 eqid K=K
9 6 8 3 1 2 atcvreq0 KAtLatPBaseKQAPCQP=0.K
10 7 9 syl3an2 KAtLatPAQAPCQP=0.K
11 10 necon3bbid KAtLatPAQA¬PCQP0.K
12 5 11 mpbird KAtLatPAQA¬PCQ