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

Definition df-cvlat 29817
Description: Define the class of atomic lattices with the covering property. (This is actually the exchange property, but they are equivalent. The literature usually uses the covering property terminology.) (Contributed by NM, 5-Nov-2012.)
Assertion
Ref Expression
df-cvlat  |-  CvLat  =  {
k  e.  AtLat  |  A. a  e.  ( Atoms `  k ) A. b  e.  ( Atoms `  k ) A. c  e.  ( Base `  k ) ( ( -.  a ( le `  k ) c  /\  a ( le `  k ) ( c ( join `  k ) b ) )  ->  b ( le `  k ) ( c ( join `  k
) a ) ) }
Distinct variable group:    k, c, a, b

Detailed syntax breakdown of Definition df-cvlat
StepHypRef Expression
1 clc 29760 . 2  class  CvLat
2 va . . . . . . . . . . 11  set  a
32cv 1648 . . . . . . . . . 10  class  a
4 vc . . . . . . . . . . 11  set  c
54cv 1648 . . . . . . . . . 10  class  c
6 vk . . . . . . . . . . . 12  set  k
76cv 1648 . . . . . . . . . . 11  class  k
8 cple 13499 . . . . . . . . . . 11  class  le
97, 8cfv 5421 . . . . . . . . . 10  class  ( le
`  k )
103, 5, 9wbr 4180 . . . . . . . . 9  wff  a ( le `  k ) c
1110wn 3 . . . . . . . 8  wff  -.  a
( le `  k
) c
12 vb . . . . . . . . . . 11  set  b
1312cv 1648 . . . . . . . . . 10  class  b
14 cjn 14364 . . . . . . . . . . 11  class  join
157, 14cfv 5421 . . . . . . . . . 10  class  ( join `  k )
165, 13, 15co 6048 . . . . . . . . 9  class  ( c ( join `  k
) b )
173, 16, 9wbr 4180 . . . . . . . 8  wff  a ( le `  k ) ( c ( join `  k ) b )
1811, 17wa 359 . . . . . . 7  wff  ( -.  a ( le `  k ) c  /\  a ( le `  k ) ( c ( join `  k
) b ) )
195, 3, 15co 6048 . . . . . . . 8  class  ( c ( join `  k
) a )
2013, 19, 9wbr 4180 . . . . . . 7  wff  b ( le `  k ) ( c ( join `  k ) a )
2118, 20wi 4 . . . . . 6  wff  ( ( -.  a ( le
`  k ) c  /\  a ( le
`  k ) ( c ( join `  k
) b ) )  ->  b ( le
`  k ) ( c ( join `  k
) a ) )
22 cbs 13432 . . . . . . 7  class  Base
237, 22cfv 5421 . . . . . 6  class  ( Base `  k )
2421, 4, 23wral 2674 . . . . 5  wff  A. c  e.  ( Base `  k
) ( ( -.  a ( le `  k ) c  /\  a ( le `  k ) ( c ( join `  k
) b ) )  ->  b ( le
`  k ) ( c ( join `  k
) a ) )
25 catm 29758 . . . . . 6  class  Atoms
267, 25cfv 5421 . . . . 5  class  ( Atoms `  k )
2724, 12, 26wral 2674 . . . 4  wff  A. b  e.  ( Atoms `  k ) A. c  e.  ( Base `  k ) ( ( -.  a ( le `  k ) c  /\  a ( le `  k ) ( c ( join `  k ) b ) )  ->  b ( le `  k ) ( c ( join `  k
) a ) )
2827, 2, 26wral 2674 . . 3  wff  A. a  e.  ( Atoms `  k ) A. b  e.  ( Atoms `  k ) A. c  e.  ( Base `  k ) ( ( -.  a ( le
`  k ) c  /\  a ( le
`  k ) ( c ( join `  k
) b ) )  ->  b ( le
`  k ) ( c ( join `  k
) a ) )
29 cal 29759 . . 3  class  AtLat
3028, 6, 29crab 2678 . 2  class  { k  e.  AtLat  |  A. a  e.  ( Atoms `  k ) A. b  e.  ( Atoms `  k ) A. c  e.  ( Base `  k ) ( ( -.  a ( le
`  k ) c  /\  a ( le
`  k ) ( c ( join `  k
) b ) )  ->  b ( le
`  k ) ( c ( join `  k
) a ) ) }
311, 30wceq 1649 1  wff  CvLat  =  {
k  e.  AtLat  |  A. a  e.  ( Atoms `  k ) A. b  e.  ( Atoms `  k ) A. c  e.  ( Base `  k ) ( ( -.  a ( le `  k ) c  /\  a ( le `  k ) ( c ( join `  k ) b ) )  ->  b ( le `  k ) ( c ( join `  k
) a ) ) }
Colors of variables: wff set class
This definition is referenced by:  iscvlat  29818
  Copyright terms: Public domain W3C validator