Metamath Proof Explorer

Definition df-atl

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)

Ref Expression
Assertion df-atl ⊢ AtLat = k ∈ Lat | Base k ∈ dom ⁡ glb ⁡ k ∧ ∀ x ∈ Base k x ≠ 0. ⁡ k → ∃ p ∈ Atoms ⁡ k p ≤ k x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cal class AtLat
1 vk setvar k
2 clat class Lat
3 cbs class Base
4 1 cv setvar k
5 4 3 cfv class Base k
6 cglb class glb
7 4 6 cfv class glb ⁡ k
8 7 cdm class dom ⁡ glb ⁡ k
9 5 8 wcel wff Base k ∈ dom ⁡ glb ⁡ k
10 vx setvar x
11 10 cv setvar x
12 cp0 class 0.
13 4 12 cfv class 0. ⁡ k
14 11 13 wne wff x ≠ 0. ⁡ k
15 vp setvar p
16 catm class Atoms
17 4 16 cfv class Atoms ⁡ k
18 15 cv setvar p
19 cple class le
20 4 19 cfv class ≤ k
21 18 11 20 wbr wff p ≤ k x
22 21 15 17 wrex wff ∃ p ∈ Atoms ⁡ k p ≤ k x
23 14 22 wi wff x ≠ 0. ⁡ k → ∃ p ∈ Atoms ⁡ k p ≤ k x
24 23 10 5 wral wff ∀ x ∈ Base k x ≠ 0. ⁡ k → ∃ p ∈ Atoms ⁡ k p ≤ k x
25 9 24 wa wff Base k ∈ dom ⁡ glb ⁡ k ∧ ∀ x ∈ Base k x ≠ 0. ⁡ k → ∃ p ∈ Atoms ⁡ k p ≤ k x
26 25 1 2 crab class k ∈ Lat | Base k ∈ dom ⁡ glb ⁡ k ∧ ∀ x ∈ Base k x ≠ 0. ⁡ k → ∃ p ∈ Atoms ⁡ k p ≤ k x
27 0 26 wceq wff AtLat = k ∈ Lat | Base k ∈ dom ⁡ glb ⁡ k ∧ ∀ x ∈ Base k x ≠ 0. ⁡ k → ∃ p ∈ Atoms ⁡ k p ≤ k x