Definition df-atl 34585

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 = { k e. Lat | ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x ) ) }

Distinct variable group:   k, p, x

Detailed syntax breakdown of Definition df-atl

Step	Hyp	Ref	Expression
1		cal 34551	. 2 class AtLat
2		vk	. . . . . . 7 setvar k
3	2	cv 1482	. . . . . 6 class k
4		cbs 15857	. . . . . 6 class Base
5	3, 4	cfv 5888	. . . . 5 class ( Base ` k )
6		cglb 16943	. . . . . . 7 class glb
7	3, 6	cfv 5888	. . . . . 6 class ( glb ` k )
8	7	cdm 5114	. . . . 5 class dom ( glb ` k )
9	5, 8	wcel 1990	. . . 4 wff ( Base ` k ) e. dom ( glb ` k )
10		vx	. . . . . . . 8 setvar x
11	10	cv 1482	. . . . . . 7 class x
12		cp0 17037	. . . . . . . 8 class 0.
13	3, 12	cfv 5888	. . . . . . 7 class ( 0. ` k )
14	11, 13	wne 2794	. . . . . 6 wff x =/= ( 0. ` k )
15		vp	. . . . . . . . 9 setvar p
16	15	cv 1482	. . . . . . . 8 class p
17		cple 15948	. . . . . . . . 9 class le
18	3, 17	cfv 5888	. . . . . . . 8 class ( le ` k )
19	16, 11, 18	wbr 4653	. . . . . . 7 wff p ( le ` k ) x
20		catm 34550	. . . . . . . 8 class Atoms
21	3, 20	cfv 5888	. . . . . . 7 class ( Atoms ` k )
22	19, 15, 21	wrex 2913	. . . . . 6 wff E. p e. ( Atoms ` k ) p ( le ` k ) x
23	14, 22	wi 4	. . . . 5 wff ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x )
24	23, 10, 5	wral 2912	. . . 4 wff A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x )
25	9, 24	wa 384	. . 3 wff ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x ) )
26		clat 17045	. . 3 class Lat
27	25, 2, 26	crab 2916	. 2 class { k e. Lat | ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x ) ) }
28	1, 27	wceq 1483	1 wff AtLat = { k e. Lat | ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x ) ) }

This definition is referenced by:  isatl  34586