Definition df-atl 39299

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 39265	. 2 class AtLat
2		vk	. . . . . . 7 setvar 𝑘
3	2	cv 1539	. . . . . 6 class 𝑘
4		cbs 17247	. . . . . 6 class Base
5	3, 4	cfv 6561	. . . . 5 class (Base‘𝑘)
6		cglb 18356	. . . . . . 7 class glb
7	3, 6	cfv 6561	. . . . . 6 class (glb‘𝑘)
8	7	cdm 5685	. . . . 5 class dom (glb‘𝑘)
9	5, 8	wcel 2108	. . . 4 wff (Base‘𝑘) ∈ dom (glb‘𝑘)
10		vx	. . . . . . . 8 setvar 𝑥
11	10	cv 1539	. . . . . . 7 class 𝑥
12		cp0 18468	. . . . . . . 8 class 0.
13	3, 12	cfv 6561	. . . . . . 7 class (0.‘𝑘)
14	11, 13	wne 2940	. . . . . 6 wff 𝑥 ≠ (0.‘𝑘)
15		vp	. . . . . . . . 9 setvar 𝑝
16	15	cv 1539	. . . . . . . 8 class 𝑝
17		cple 17304	. . . . . . . . 9 class le
18	3, 17	cfv 6561	. . . . . . . 8 class (le‘𝑘)
19	16, 11, 18	wbr 5143	. . . . . . 7 wff 𝑝(le‘𝑘)𝑥
20		catm 39264	. . . . . . . 8 class Atoms
21	3, 20	cfv 6561	. . . . . . 7 class (Atoms‘𝑘)
22	19, 15, 21	wrex 3070	. . . . . 6 wff ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥
23	14, 22	wi 4	. . . . 5 wff (𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
24	23, 10, 5	wral 3061	. . . 4 wff ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
25	9, 24	wa 395	. . 3 wff ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))
26		clat 18476	. . 3 class Lat
27	25, 2, 26	crab 3436	. 2 class {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
28	1, 27	wceq 1540	1 wff AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}

This definition is referenced by:  isatl  39300