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 = { 𝑘 ∈ Lat ∣ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cal AtLat
1 vk 𝑘
2 clat Lat
3 cbs Base
4 1 cv 𝑘
5 4 3 cfv ( Base ‘ 𝑘 )
6 cglb glb
7 4 6 cfv ( glb ‘ 𝑘 )
8 7 cdm dom ( glb ‘ 𝑘 )
9 5 8 wcel ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 )
10 vx 𝑥
11 10 cv 𝑥
12 cp0 0.
13 4 12 cfv ( 0. ‘ 𝑘 )
14 11 13 wne 𝑥 ≠ ( 0. ‘ 𝑘 )
15 vp 𝑝
16 catm Atoms
17 4 16 cfv ( Atoms ‘ 𝑘 )
18 15 cv 𝑝
19 cple le
20 4 19 cfv ( le ‘ 𝑘 )
21 18 11 20 wbr 𝑝 ( le ‘ 𝑘 ) 𝑥
22 21 15 17 wrex 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥
23 14 22 wi ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 )
24 23 10 5 wral 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 )
25 9 24 wa ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) )
26 25 1 2 crab { 𝑘 ∈ Lat ∣ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) ) }
27 0 26 wceq AtLat = { 𝑘 ∈ Lat ∣ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) ) }