# Metamath Proof Explorer

## 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}}\phantom{\rule{.4em}{0ex}}\left({x}\ne \mathrm{0.}\left({k}\right)\to \exists {p}\in \mathrm{Atoms}\left({k}\right)\phantom{\rule{.4em}{0ex}}{p}{\le }_{{k}}{x}\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cal ${class}\mathrm{AtLat}$
1 vk ${setvar}{k}$
2 clat ${class}\mathrm{Lat}$
3 cbs ${class}\mathrm{Base}$
4 1 cv ${setvar}{k}$
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 ${setvar}{x}$
11 10 cv ${setvar}{x}$
12 cp0 ${class}\mathrm{0.}$
13 4 12 cfv ${class}\mathrm{0.}\left({k}\right)$
14 11 13 wne ${wff}{x}\ne \mathrm{0.}\left({k}\right)$
15 vp ${setvar}{p}$
16 catm ${class}\mathrm{Atoms}$
17 4 16 cfv ${class}\mathrm{Atoms}\left({k}\right)$
18 15 cv ${setvar}{p}$
19 cple ${class}\mathrm{le}$
20 4 19 cfv ${class}{\le }_{{k}}$
21 18 11 20 wbr ${wff}{p}{\le }_{{k}}{x}$
22 21 15 17 wrex ${wff}\exists {p}\in \mathrm{Atoms}\left({k}\right)\phantom{\rule{.4em}{0ex}}{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)\phantom{\rule{.4em}{0ex}}{p}{\le }_{{k}}{x}\right)$
24 23 10 5 wral ${wff}\forall {x}\in {\mathrm{Base}}_{{k}}\phantom{\rule{.4em}{0ex}}\left({x}\ne \mathrm{0.}\left({k}\right)\to \exists {p}\in \mathrm{Atoms}\left({k}\right)\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}\left({x}\ne \mathrm{0.}\left({k}\right)\to \exists {p}\in \mathrm{Atoms}\left({k}\right)\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}\left({x}\ne \mathrm{0.}\left({k}\right)\to \exists {p}\in \mathrm{Atoms}\left({k}\right)\phantom{\rule{.4em}{0ex}}{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}}\phantom{\rule{.4em}{0ex}}\left({x}\ne \mathrm{0.}\left({k}\right)\to \exists {p}\in \mathrm{Atoms}\left({k}\right)\phantom{\rule{.4em}{0ex}}{p}{\le }_{{k}}{x}\right)\right)\right\}$