Theorem cvlatl

Description: An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Assertion	cvlatl	$$⊢K\in \mathrm{CvLat}\to K\in \mathrm{AtLat}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
2		eqid	$$⊢{\le }_K={\le }_K$$
3		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
4		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
5	1 2 3 4	iscvlat	$$⊢K\in \mathrm{CvLat}\leftrightarrow \left(K\in \mathrm{AtLat}\wedge \forall p\in \mathrm{Atoms}\left(K\right)\forall q\in \mathrm{Atoms}\left(K\right)\forall x\in {\mathrm{Base}}_K\left(\left(\neg p{\le }_{K}x\wedge p{\le }_K\left(x\mathrm{join}\left(K\right)q\right)\right)\to q{\le }_K\left(x\mathrm{join}\left(K\right)p\right)\right)\right)$$
6	5	simplbi	$$⊢K\in \mathrm{CvLat}\to K\in \mathrm{AtLat}$$