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 = Atoms K
Assertion atncvrN K AtLat P A Q A ¬ P C Q

Proof

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 AtLat P A P 0. K
5 4 3adant3 K AtLat P A Q A P 0. K
6 eqid Base K = Base K
7 6 2 atbase P A P Base K
8 eqid K = K
9 6 8 3 1 2 atcvreq0 K AtLat P Base K Q A P C Q P = 0. K
10 7 9 syl3an2 K AtLat P A Q A P C Q P = 0. K
11 10 necon3bbid K AtLat P A Q A ¬ P C Q P 0. K
12 5 11 mpbird K AtLat P A Q A ¬ P C Q