Definition df-atl 38157

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 38123	. 2 class AtLat
2		vk	. . . . . . 7 setvar 𝑘
3	2	cv 1541	. . . . . 6 class 𝑘
4		cbs 17141	. . . . . 6 class Base
5	3, 4	cfv 6541	. . . . 5 class (Base‘𝑘)
6		cglb 18260	. . . . . . 7 class glb
7	3, 6	cfv 6541	. . . . . 6 class (glb‘𝑘)
8	7	cdm 5676	. . . . 5 class dom (glb‘𝑘)
9	5, 8	wcel 2107	. . . 4 wff (Base‘𝑘) ∈ dom (glb‘𝑘)
10		vx	. . . . . . . 8 setvar 𝑥
11	10	cv 1541	. . . . . . 7 class 𝑥
12		cp0 18373	. . . . . . . 8 class 0.
13	3, 12	cfv 6541	. . . . . . 7 class (0.‘𝑘)
14	11, 13	wne 2941	. . . . . 6 wff 𝑥 ≠ (0.‘𝑘)
15		vp	. . . . . . . . 9 setvar 𝑝
16	15	cv 1541	. . . . . . . 8 class 𝑝
17		cple 17201	. . . . . . . . 9 class le
18	3, 17	cfv 6541	. . . . . . . 8 class (le‘𝑘)
19	16, 11, 18	wbr 5148	. . . . . . 7 wff 𝑝(le‘𝑘)𝑥
20		catm 38122	. . . . . . . 8 class Atoms
21	3, 20	cfv 6541	. . . . . . 7 class (Atoms‘𝑘)
22	19, 15, 21	wrex 3071	. . . . . 6 wff ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥
23	14, 22	wi 4	. . . . 5 wff (𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
24	23, 10, 5	wral 3062	. . . 4 wff ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
25	9, 24	wa 397	. . 3 wff ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))
26		clat 18381	. . 3 class Lat
27	25, 2, 26	crab 3433	. 2 class {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
28	1, 27	wceq 1542	1 wff AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}

This definition is referenced by:  isatl  38158