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

Definition df-cvlat 30120
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 30063 . 2  class  CvLat
2 va . . . . . . . . . . 11  set  a
32cv 1651 . . . . . . . . . 10  class  a
4 vc . . . . . . . . . . 11  set  c
54cv 1651 . . . . . . . . . 10  class  c
6 vk . . . . . . . . . . . 12  set  k
76cv 1651 . . . . . . . . . . 11  class  k
8 cple 13536 . . . . . . . . . . 11  class  le
97, 8cfv 5454 . . . . . . . . . 10  class  ( le
`  k )
103, 5, 9wbr 4212 . . . . . . . . 9  wff  a ( le `  k ) c
1110wn 3 . . . . . . . 8  wff  -.  a
( le `  k
) c
12 vb . . . . . . . . . . 11  set  b
1312cv 1651 . . . . . . . . . 10  class  b
14 cjn 14401 . . . . . . . . . . 11  class  join
157, 14cfv 5454 . . . . . . . . . 10  class  ( join `  k )
165, 13, 15co 6081 . . . . . . . . 9  class  ( c ( join `  k
) b )
173, 16, 9wbr 4212 . . . . . . . 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 6081 . . . . . . . 8  class  ( c ( join `  k
) a )
2013, 19, 9wbr 4212 . . . . . . 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 13469 . . . . . . 7  class  Base
237, 22cfv 5454 . . . . . 6  class  ( Base `  k )
2421, 4, 23wral 2705 . . . . 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 30061 . . . . . 6  class  Atoms
267, 25cfv 5454 . . . . 5  class  ( Atoms `  k )
2724, 12, 26wral 2705 . . . 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 2705 . . 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 30062 . . 3  class  AtLat
3028, 6, 29crab 2709 . 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 1652 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  30121
  Copyright terms: Public domain W3C validator