Definition df-atl

Description: Define the class of atomic lattices, in which every nonzero element is greater than or equal to an atom. We also ensure the existence of a lattice zero, since a lattice by itself may not have a zero. (Contributed by NM, 18-Sep-2011) (Revised by NM, 14-Sep-2018)

	Ref	Expression
Assertion	df-atl	$$⊢\mathrm{AtLat}=\left\{k\in \mathrm{Lat}|\left({\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)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cal	$$class\mathrm{AtLat}$$
1		vk	$$setvark$$
2		clat	$$class\mathrm{Lat}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvark$$
5	4 3	cfv	$$class{\mathrm{Base}}_k$$
6		cglb	$$class\mathrm{glb}$$
7	4 6	cfv	$$class\mathrm{glb}\left(k\right)$$
8	7	cdm	$$class\mathrm{dom}\mathrm{glb}\left(k\right)$$
9	5 8	wcel	$$wff{\mathrm{Base}}_k\in \mathrm{dom}\mathrm{glb}\left(k\right)$$
10		vx	$$setvarx$$
11	10	cv	$$setvarx$$
12		cp0	$$class\mathrm{0.}$$
13	4 12	cfv	$$class\mathrm{0.}\left(k\right)$$
14	11 13	wne	$$wffx\ne \mathrm{0.}\left(k\right)$$
15		vp	$$setvarp$$
16		catm	$$class\mathrm{Atoms}$$
17	4 16	cfv	$$class\mathrm{Atoms}\left(k\right)$$
18	15	cv	$$setvarp$$
19		cple	$$class\mathrm{le}$$
20	4 19	cfv	$$class{\le }_k$$
21	18 11 20	wbr	$$wffp{\le }_{k}x$$
22	21 15 17	wrex	$$wff\exists p\in \mathrm{Atoms}\left(k\right)p{\le }_{k}x$$
23	14 22	wi	$$wff\left(x\ne \mathrm{0.}\left(k\right)\to \exists p\in \mathrm{Atoms}\left(k\right)p{\le }_{k}x\right)$$
24	23 10 5	wral	$$wff\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)$$
25	9 24	wa	$$wff\left({\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)$$
26	25 1 2	crab	$$class\left\{k\in \mathrm{Lat}|\left({\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)\right\}$$
27	0 26	wceq	$$wff\mathrm{AtLat}=\left\{k\in \mathrm{Lat}|\left({\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)\right\}$$