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 30194
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 30137 . 2  class  CvLat
2 va . . . . . . . . . . 11  set  a
32cv 1652 . . . . . . . . . 10  class  a
4 vc . . . . . . . . . . 11  set  c
54cv 1652 . . . . . . . . . 10  class  c
6 vk . . . . . . . . . . . 12  set  k
76cv 1652 . . . . . . . . . . 11  class  k
8 cple 13541 . . . . . . . . . . 11  class  le
97, 8cfv 5457 . . . . . . . . . 10  class  ( le
`  k )
103, 5, 9wbr 4215 . . . . . . . . 9  wff  a ( le `  k ) c
1110wn 3 . . . . . . . 8  wff  -.  a
( le `  k
) c
12 vb . . . . . . . . . . 11  set  b
1312cv 1652 . . . . . . . . . 10  class  b
14 cjn 14406 . . . . . . . . . . 11  class  join
157, 14cfv 5457 . . . . . . . . . 10  class  ( join `  k )
165, 13, 15co 6084 . . . . . . . . 9  class  ( c ( join `  k
) b )
173, 16, 9wbr 4215 . . . . . . . 8  wff  a ( le `  k ) ( c ( join `  k ) b )
1811, 17wa 360 . . . . . . 7  wff  ( -.  a ( le `  k ) c  /\  a ( le `  k ) ( c ( join `  k
) b ) )
195, 3, 15co 6084 . . . . . . . 8  class  ( c ( join `  k
) a )
2013, 19, 9wbr 4215 . . . . . . 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 13474 . . . . . . 7  class  Base
237, 22cfv 5457 . . . . . 6  class  ( Base `  k )
2421, 4, 23wral 2707 . . . . 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 30135 . . . . . 6  class  Atoms
267, 25cfv 5457 . . . . 5  class  ( Atoms `  k )
2724, 12, 26wral 2707 . . . 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 2707 . . 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 30136 . . 3  class  AtLat
3028, 6, 29crab 2711 . 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 1653 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  30195
  Copyright terms: Public domain W3C validator