This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑘 ) 𝑥 ) ) }