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

Definition df-cvlat 29512
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 29455 . 2  class  CvLat
2 va . . . . . . . . . . 11  set  a
32cv 1622 . . . . . . . . . 10  class  a
4 vc . . . . . . . . . . 11  set  c
54cv 1622 . . . . . . . . . 10  class  c
6 vk . . . . . . . . . . . 12  set  k
76cv 1622 . . . . . . . . . . 11  class  k
8 cple 13215 . . . . . . . . . . 11  class  le
97, 8cfv 5255 . . . . . . . . . 10  class  ( le
`  k )
103, 5, 9wbr 4023 . . . . . . . . 9  wff  a ( le `  k ) c
1110wn 3 . . . . . . . 8  wff  -.  a
( le `  k
) c
12 vb . . . . . . . . . . 11  set  b
1312cv 1622 . . . . . . . . . 10  class  b
14 cjn 14078 . . . . . . . . . . 11  class  join
157, 14cfv 5255 . . . . . . . . . 10  class  ( join `  k )
165, 13, 15co 5858 . . . . . . . . 9  class  ( c ( join `  k
) b )
173, 16, 9wbr 4023 . . . . . . . 8  wff  a ( le `  k ) ( c ( join `  k ) b )
1811, 17wa 358 . . . . . . 7  wff  ( -.  a ( le `  k ) c  /\  a ( le `  k ) ( c ( join `  k
) b ) )
195, 3, 15co 5858 . . . . . . . 8  class  ( c ( join `  k
) a )
2013, 19, 9wbr 4023 . . . . . . 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 13148 . . . . . . 7  class  Base
237, 22cfv 5255 . . . . . 6  class  ( Base `  k )
2421, 4, 23wral 2543 . . . . 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 29453 . . . . . 6  class  Atoms
267, 25cfv 5255 . . . . 5  class  ( Atoms `  k )
2724, 12, 26wral 2543 . . . 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 2543 . . 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 29454 . . 3  class  AtLat
3028, 6, 29crab 2547 . 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 1623 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  29513
  Copyright terms: Public domain W3C validator