Metamath Proof Explorer


Theorem atcvr2

Description: An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012)

Ref Expression
Hypotheses atcvr1.j ˙ = join K
atcvr1.c C = K
atcvr1.a A = Atoms K
Assertion atcvr2 K HL P A Q A P Q P C Q ˙ P

Proof

Step Hyp Ref Expression
1 atcvr1.j ˙ = join K
2 atcvr1.c C = K
3 atcvr1.a A = Atoms K
4 hlomcmcv K HL K OML K CLat K CvLat
5 1 2 3 cvlatcvr2 K OML K CLat K CvLat P A Q A P Q P C Q ˙ P
6 4 5 syl3an1 K HL P A Q A P Q P C Q ˙ P