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 32770
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 32736 . 2  class  AtLat
2 vk . . . . . . 7  setvar  k
32cv 1436 . . . . . 6  class  k
4 cbs 15057 . . . . . 6  class  Base
53, 4cfv 5537 . . . . 5  class  ( Base `  k )
6 cglb 16124 . . . . . . 7  class  glb
73, 6cfv 5537 . . . . . 6  class  ( glb `  k )
87cdm 4789 . . . . 5  class  dom  ( glb `  k )
95, 8wcel 1872 . . . 4  wff  ( Base `  k )  e.  dom  ( glb `  k )
10 vx . . . . . . . 8  setvar  x
1110cv 1436 . . . . . . 7  class  x
12 cp0 16219 . . . . . . . 8  class  0.
133, 12cfv 5537 . . . . . . 7  class  ( 0.
`  k )
1411, 13wne 2593 . . . . . 6  wff  x  =/=  ( 0. `  k
)
15 vp . . . . . . . . 9  setvar  p
1615cv 1436 . . . . . . . 8  class  p
17 cple 15133 . . . . . . . . 9  class  le
183, 17cfv 5537 . . . . . . . 8  class  ( le
`  k )
1916, 11, 18wbr 4359 . . . . . . 7  wff  p ( le `  k ) x
20 catm 32735 . . . . . . . 8  class  Atoms
213, 20cfv 5537 . . . . . . 7  class  ( Atoms `  k )
2219, 15, 21wrex 2709 . . . . . 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 2708 . . . 4  wff  A. x  e.  ( Base `  k
) ( x  =/=  ( 0. `  k
)  ->  E. p  e.  ( Atoms `  k )
p ( le `  k ) x )
259, 24wa 370 . . 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 16227 . . 3  class  Lat
2725, 2, 26crab 2712 . 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 1437 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  32771
  Copyright terms: Public domain W3C validator