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 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cal 
 |-  AtLat
1 vk 
 |-  k
2 clat 
 |-  Lat
3 cbs 
 |-  Base
4 1 cv 
 |-  k
5 4 3 cfv 
 |-  ( Base ` k )
6 cglb 
 |-  glb
7 4 6 cfv 
 |-  ( glb ` k )
8 7 cdm 
 |-  dom ( glb ` k )
9 5 8 wcel 
 |-  ( Base ` k ) e. dom ( glb ` k )
10 vx 
 |-  x
11 10 cv 
 |-  x
12 cp0 
 |-  0.
13 4 12 cfv 
 |-  ( 0. ` k )
14 11 13 wne 
 |-  x =/= ( 0. ` k )
15 vp 
 |-  p
16 catm 
 |-  Atoms
17 4 16 cfv 
 |-  ( Atoms ` k )
18 15 cv 
 |-  p
19 cple 
 |-  le
20 4 19 cfv 
 |-  ( le ` k )
21 18 11 20 wbr 
 |-  p ( le ` k ) x
22 21 15 17 wrex 
 |-  E. p e. ( Atoms ` k ) p ( le ` k ) x
23 14 22 wi 
 |-  ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x )
24 23 10 5 wral 
 |-  A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x )
25 9 24 wa 
 |-  ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x ) )
26 25 1 2 crab 
 |-  { 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 ) ) }
27 0 26 wceq 
 |-  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 ) ) }