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

Definition df-atl 29488
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.)
Assertion
Ref Expression
df-atl  |-  AtLat  =  {
k  e.  Lat  | 
( ( 0. `  k )  e.  (
Base `  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 29454 . 2  class  AtLat
2 vk . . . . . . 7  set  k
32cv 1622 . . . . . 6  class  k
4 cp0 14143 . . . . . 6  class  0.
53, 4cfv 5255 . . . . 5  class  ( 0.
`  k )
6 cbs 13148 . . . . . 6  class  Base
73, 6cfv 5255 . . . . 5  class  ( Base `  k )
85, 7wcel 1684 . . . 4  wff  ( 0.
`  k )  e.  ( Base `  k
)
9 vx . . . . . . . 8  set  x
109cv 1622 . . . . . . 7  class  x
1110, 5wne 2446 . . . . . 6  wff  x  =/=  ( 0. `  k
)
12 vp . . . . . . . . 9  set  p
1312cv 1622 . . . . . . . 8  class  p
14 cple 13215 . . . . . . . . 9  class  le
153, 14cfv 5255 . . . . . . . 8  class  ( le
`  k )
1613, 10, 15wbr 4023 . . . . . . 7  wff  p ( le `  k ) x
17 catm 29453 . . . . . . . 8  class  Atoms
183, 17cfv 5255 . . . . . . 7  class  ( Atoms `  k )
1916, 12, 18wrex 2544 . . . . . 6  wff  E. p  e.  ( Atoms `  k )
p ( le `  k ) x
2011, 19wi 4 . . . . 5  wff  ( x  =/=  ( 0. `  k )  ->  E. p  e.  ( Atoms `  k )
p ( le `  k ) x )
2120, 9, 7wral 2543 . . . 4  wff  A. x  e.  ( Base `  k
) ( x  =/=  ( 0. `  k
)  ->  E. p  e.  ( Atoms `  k )
p ( le `  k ) x )
228, 21wa 358 . . 3  wff  ( ( 0. `  k )  e.  ( Base `  k
)  /\  A. x  e.  ( Base `  k
) ( x  =/=  ( 0. `  k
)  ->  E. p  e.  ( Atoms `  k )
p ( le `  k ) x ) )
23 clat 14151 . . 3  class  Lat
2422, 2, 23crab 2547 . 2  class  { k  e.  Lat  |  ( ( 0. `  k
)  e.  ( Base `  k )  /\  A. x  e.  ( Base `  k ) ( x  =/=  ( 0. `  k )  ->  E. p  e.  ( Atoms `  k )
p ( le `  k ) x ) ) }
251, 24wceq 1623 1  wff  AtLat  =  {
k  e.  Lat  | 
( ( 0. `  k )  e.  (
Base `  k )  /\  A. x  e.  (
Base `  k )
( x  =/=  ( 0. `  k )  ->  E. p  e.  ( Atoms `  k ) p ( le `  k
) x ) ) }
Colors of variables: wff set class
This definition is referenced by:  isatl  29489
  Copyright terms: Public domain W3C validator