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 35057
 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 35023 . 2 class AtLat
2 vk . . . . . . 7 setvar 𝑘
32cv 1619 . . . . . 6 class 𝑘
4 cbs 16030 . . . . . 6 class Base
53, 4cfv 6037 . . . . 5 class (Base‘𝑘)
6 cglb 17115 . . . . . . 7 class glb
73, 6cfv 6037 . . . . . 6 class (glb‘𝑘)
87cdm 5254 . . . . 5 class dom (glb‘𝑘)
95, 8wcel 2127 . . . 4 wff (Base‘𝑘) ∈ dom (glb‘𝑘)
10 vx . . . . . . . 8 setvar 𝑥
1110cv 1619 . . . . . . 7 class 𝑥
12 cp0 17209 . . . . . . . 8 class 0.
133, 12cfv 6037 . . . . . . 7 class (0.‘𝑘)
1411, 13wne 2920 . . . . . 6 wff 𝑥 ≠ (0.‘𝑘)
15 vp . . . . . . . . 9 setvar 𝑝
1615cv 1619 . . . . . . . 8 class 𝑝
17 cple 16121 . . . . . . . . 9 class le
183, 17cfv 6037 . . . . . . . 8 class (le‘𝑘)
1916, 11, 18wbr 4792 . . . . . . 7 wff 𝑝(le‘𝑘)𝑥
20 catm 35022 . . . . . . . 8 class Atoms
213, 20cfv 6037 . . . . . . 7 class (Atoms‘𝑘)
2219, 15, 21wrex 3039 . . . . . 6 wff 𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥
2314, 22wi 4 . . . . 5 wff (𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
2423, 10, 5wral 3038 . . . 4 wff 𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)
259, 24wa 383 . . 3 wff ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))
26 clat 17217 . . 3 class Lat
2725, 2, 26crab 3042 . 2 class {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
281, 27wceq 1620 1 wff AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))}
 Colors of variables: wff setvar class This definition is referenced by:  isatl  35058
 Copyright terms: Public domain W3C validator