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 34065
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 34031 . 2 class AtLat
2 vk . . . . . . 7 setvar 𝑘
32cv 1479 . . . . . 6 class 𝑘
4 cbs 15781 . . . . . 6 class Base
53, 4cfv 5847 . . . . 5 class (Base‘𝑘)
6 cglb 16864 . . . . . . 7 class glb
73, 6cfv 5847 . . . . . 6 class (glb‘𝑘)
87cdm 5074 . . . . 5 class dom (glb‘𝑘)
95, 8wcel 1987 . . . 4 wff (Base‘𝑘) ∈ dom (glb‘𝑘)
10 vx . . . . . . . 8 setvar 𝑥
1110cv 1479 . . . . . . 7 class 𝑥
12 cp0 16958 . . . . . . . 8 class 0.
133, 12cfv 5847 . . . . . . 7 class (0.‘𝑘)
1411, 13wne 2790 . . . . . 6 wff 𝑥 ≠ (0.‘𝑘)
15 vp . . . . . . . . 9 setvar 𝑝
1615cv 1479 . . . . . . . 8 class 𝑝
17 cple 15869 . . . . . . . . 9 class le
183, 17cfv 5847 . . . . . . . 8 class (le‘𝑘)
1916, 11, 18wbr 4613 . . . . . . 7 wff 𝑝(le‘𝑘)𝑥
20 catm 34030 . . . . . . . 8 class Atoms
213, 20cfv 5847 . . . . . . 7 class (Atoms‘𝑘)
2219, 15, 21wrex 2908 . . . . . 6 wff 𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥
2314, 22wi 4 . . . . 5 wff (𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
2423, 10, 5wral 2907 . . . 4 wff 𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
259, 24wa 384 . . 3 wff ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))
26 clat 16966 . . 3 class Lat
2725, 2, 26crab 2911 . 2 class {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
281, 27wceq 1480 1 wff AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
Colors of variables: wff setvar class
This definition is referenced by:  isatl  34066
  Copyright terms: Public domain W3C validator