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

Definition df-cvlat 30134
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 30077 . 2  class  CvLat
2 va . . . . . . . . . . 11  set  a
32cv 1631 . . . . . . . . . 10  class  a
4 vc . . . . . . . . . . 11  set  c
54cv 1631 . . . . . . . . . 10  class  c
6 vk . . . . . . . . . . . 12  set  k
76cv 1631 . . . . . . . . . . 11  class  k
8 cple 13231 . . . . . . . . . . 11  class  le
97, 8cfv 5271 . . . . . . . . . 10  class  ( le
`  k )
103, 5, 9wbr 4039 . . . . . . . . 9  wff  a ( le `  k ) c
1110wn 3 . . . . . . . 8  wff  -.  a
( le `  k
) c
12 vb . . . . . . . . . . 11  set  b
1312cv 1631 . . . . . . . . . 10  class  b
14 cjn 14094 . . . . . . . . . . 11  class  join
157, 14cfv 5271 . . . . . . . . . 10  class  ( join `  k )
165, 13, 15co 5874 . . . . . . . . 9  class  ( c ( join `  k
) b )
173, 16, 9wbr 4039 . . . . . . . 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 5874 . . . . . . . 8  class  ( c ( join `  k
) a )
2013, 19, 9wbr 4039 . . . . . . 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 13164 . . . . . . 7  class  Base
237, 22cfv 5271 . . . . . 6  class  ( Base `  k )
2421, 4, 23wral 2556 . . . . 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 30075 . . . . . 6  class  Atoms
267, 25cfv 5271 . . . . 5  class  ( Atoms `  k )
2724, 12, 26wral 2556 . . . 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 2556 . . 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 30076 . . 3  class  AtLat
3028, 6, 29crab 2560 . 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 1632 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  30135
  Copyright terms: Public domain W3C validator