Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-atl Structured version   Visualization version   GIF version

Definition df-atl 36316
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
StepHypRef Expression
1 cal 36282 . 2 class AtLat
2 vk . . . . . . 7 setvar 𝑘
32cv 1527 . . . . . 6 class 𝑘
4 cbs 16473 . . . . . 6 class Base
53, 4cfv 6349 . . . . 5 class (Base‘𝑘)
6 cglb 17543 . . . . . . 7 class glb
73, 6cfv 6349 . . . . . 6 class (glb‘𝑘)
87cdm 5549 . . . . 5 class dom (glb‘𝑘)
95, 8wcel 2105 . . . 4 wff (Base‘𝑘) ∈ dom (glb‘𝑘)
10 vx . . . . . . . 8 setvar 𝑥
1110cv 1527 . . . . . . 7 class 𝑥
12 cp0 17637 . . . . . . . 8 class 0.
133, 12cfv 6349 . . . . . . 7 class (0.‘𝑘)
1411, 13wne 3016 . . . . . 6 wff 𝑥 ≠ (0.‘𝑘)
15 vp . . . . . . . . 9 setvar 𝑝
1615cv 1527 . . . . . . . 8 class 𝑝
17 cple 16562 . . . . . . . . 9 class le
183, 17cfv 6349 . . . . . . . 8 class (le‘𝑘)
1916, 11, 18wbr 5058 . . . . . . 7 wff 𝑝(le‘𝑘)𝑥
20 catm 36281 . . . . . . . 8 class Atoms
213, 20cfv 6349 . . . . . . 7 class (Atoms‘𝑘)
2219, 15, 21wrex 3139 . . . . . 6 wff 𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥
2314, 22wi 4 . . . . 5 wff (𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
2423, 10, 5wral 3138 . . . 4 wff 𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
259, 24wa 396 . . 3 wff ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))
26 clat 17645 . . 3 class Lat
2725, 2, 26crab 3142 . 2 class {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
281, 27wceq 1528 1 wff AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
Colors of variables: wff setvar class
This definition is referenced by:  isatl  36317
  Copyright terms: Public domain W3C validator