Definition df-atl 37239

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.)

Assertion

Ref	Expression
df-atl	⊢ AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}

Distinct variable group:   𝑘,𝑝,𝑥

Detailed syntax breakdown of Definition df-atl

Step	Hyp	Ref	Expression
1		cal 37205	. 2 class AtLat
2		vk	. . . . . . 7 setvar 𝑘
3	2	cv 1538	. . . . . 6 class 𝑘
4		cbs 16840	. . . . . 6 class Base
5	3, 4	cfv 6418	. . . . 5 class (Base‘𝑘)
6		cglb 17943	. . . . . . 7 class glb
7	3, 6	cfv 6418	. . . . . 6 class (glb‘𝑘)
8	7	cdm 5580	. . . . 5 class dom (glb‘𝑘)
9	5, 8	wcel 2108	. . . 4 wff (Base‘𝑘) ∈ dom (glb‘𝑘)
10		vx	. . . . . . . 8 setvar 𝑥
11	10	cv 1538	. . . . . . 7 class 𝑥
12		cp0 18056	. . . . . . . 8 class 0.
13	3, 12	cfv 6418	. . . . . . 7 class (0.‘𝑘)
14	11, 13	wne 2942	. . . . . 6 wff 𝑥 ≠ (0.‘𝑘)
15		vp	. . . . . . . . 9 setvar 𝑝
16	15	cv 1538	. . . . . . . 8 class 𝑝
17		cple 16895	. . . . . . . . 9 class le
18	3, 17	cfv 6418	. . . . . . . 8 class (le‘𝑘)
19	16, 11, 18	wbr 5070	. . . . . . 7 wff 𝑝(le‘𝑘)𝑥
20		catm 37204	. . . . . . . 8 class Atoms
21	3, 20	cfv 6418	. . . . . . 7 class (Atoms‘𝑘)
22	19, 15, 21	wrex 3064	. . . . . 6 wff ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥
23	14, 22	wi 4	. . . . 5 wff (𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
24	23, 10, 5	wral 3063	. . . 4 wff ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
25	9, 24	wa 395	. . 3 wff ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))
26		clat 18064	. . 3 class Lat
27	25, 2, 26	crab 3067	. 2 class {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
28	1, 27	wceq 1539	1 wff AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}

This definition is referenced by:  isatl  37240