Theorem atllat

Description: An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Assertion	atllat	$$⊢K\in \mathrm{AtLat}\to K\in \mathrm{Lat}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
2		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
3		eqid	$$⊢{\le }_K={\le }_K$$
4		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
5		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
6	1 2 3 4 5	isatl	$$⊢K\in \mathrm{AtLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge {\mathrm{Base}}_K\in \mathrm{dom}\mathrm{glb}\left(K\right)\wedge \forall x\in {\mathrm{Base}}_K\left(x\ne \mathrm{0.}\left(K\right)\to \exists p\in \mathrm{Atoms}\left(K\right)p{\le }_{K}x\right)\right)$$
7	6	simp1bi	$$⊢K\in \mathrm{AtLat}\to K\in \mathrm{Lat}$$