Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-atl Structured version   Unicode version

Definition df-atl 34898
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
StepHypRef Expression
1 cal 34864 . 2  class  AtLat
2 vk . . . . . . 7  setvar  k
32cv 1382 . . . . . 6  class  k
4 cbs 14614 . . . . . 6  class  Base
53, 4cfv 5578 . . . . 5  class  ( Base `  k )
6 cglb 15551 . . . . . . 7  class  glb
73, 6cfv 5578 . . . . . 6  class  ( glb `  k )
87cdm 4989 . . . . 5  class  dom  ( glb `  k )
95, 8wcel 1804 . . . 4  wff  ( Base `  k )  e.  dom  ( glb `  k )
10 vx . . . . . . . 8  setvar  x
1110cv 1382 . . . . . . 7  class  x
12 cp0 15646 . . . . . . . 8  class  0.
133, 12cfv 5578 . . . . . . 7  class  ( 0.
`  k )
1411, 13wne 2638 . . . . . 6  wff  x  =/=  ( 0. `  k
)
15 vp . . . . . . . . 9  setvar  p
1615cv 1382 . . . . . . . 8  class  p
17 cple 14686 . . . . . . . . 9  class  le
183, 17cfv 5578 . . . . . . . 8  class  ( le
`  k )
1916, 11, 18wbr 4437 . . . . . . 7  wff  p ( le `  k ) x
20 catm 34863 . . . . . . . 8  class  Atoms
213, 20cfv 5578 . . . . . . 7  class  ( Atoms `  k )
2219, 15, 21wrex 2794 . . . . . 6  wff  E. p  e.  ( Atoms `  k )
p ( le `  k ) x
2314, 22wi 4 . . . . 5  wff  ( x  =/=  ( 0. `  k )  ->  E. p  e.  ( Atoms `  k )
p ( le `  k ) x )
2423, 10, 5wral 2793 . . . 4  wff  A. x  e.  ( Base `  k
) ( x  =/=  ( 0. `  k
)  ->  E. p  e.  ( Atoms `  k )
p ( le `  k ) x )
259, 24wa 369 . . 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 15654 . . 3  class  Lat
2725, 2, 26crab 2797 . 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 ) ) }
281, 27wceq 1383 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 ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  isatl  34899
  Copyright terms: Public domain W3C validator