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