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

Definition df-hlat 29541
Description: Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.)
Assertion
Ref Expression
df-hlat  |-  HL  =  { l  e.  ( ( OML  i^i  CLat )  i^i  CvLat )  |  ( A. a  e.  (
Atoms `  l ) A. b  e.  ( Atoms `  l ) ( a  =/=  b  ->  E. c  e.  ( Atoms `  l )
( c  =/=  a  /\  c  =/=  b  /\  c ( le `  l ) ( a ( join `  l
) b ) ) )  /\  E. a  e.  ( Base `  l
) E. b  e.  ( Base `  l
) E. c  e.  ( Base `  l
) ( ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )  /\  ( b ( lt
`  l ) c  /\  c ( lt
`  l ) ( 1. `  l ) ) ) ) }
Distinct variable group:    c, l, a, b

Detailed syntax breakdown of Definition df-hlat
StepHypRef Expression
1 chlt 29540 . 2  class  HL
2 va . . . . . . . . 9  set  a
32cv 1622 . . . . . . . 8  class  a
4 vb . . . . . . . . 9  set  b
54cv 1622 . . . . . . . 8  class  b
63, 5wne 2446 . . . . . . 7  wff  a  =/=  b
7 vc . . . . . . . . . . 11  set  c
87cv 1622 . . . . . . . . . 10  class  c
98, 3wne 2446 . . . . . . . . 9  wff  c  =/=  a
108, 5wne 2446 . . . . . . . . 9  wff  c  =/=  b
11 vl . . . . . . . . . . . . 13  set  l
1211cv 1622 . . . . . . . . . . . 12  class  l
13 cjn 14078 . . . . . . . . . . . 12  class  join
1412, 13cfv 5255 . . . . . . . . . . 11  class  ( join `  l )
153, 5, 14co 5858 . . . . . . . . . 10  class  ( a ( join `  l
) b )
16 cple 13215 . . . . . . . . . . 11  class  le
1712, 16cfv 5255 . . . . . . . . . 10  class  ( le
`  l )
188, 15, 17wbr 4023 . . . . . . . . 9  wff  c ( le `  l ) ( a ( join `  l ) b )
199, 10, 18w3a 934 . . . . . . . 8  wff  ( c  =/=  a  /\  c  =/=  b  /\  c
( le `  l
) ( a (
join `  l )
b ) )
20 catm 29453 . . . . . . . . 9  class  Atoms
2112, 20cfv 5255 . . . . . . . 8  class  ( Atoms `  l )
2219, 7, 21wrex 2544 . . . . . . 7  wff  E. c  e.  ( Atoms `  l )
( c  =/=  a  /\  c  =/=  b  /\  c ( le `  l ) ( a ( join `  l
) b ) )
236, 22wi 4 . . . . . 6  wff  ( a  =/=  b  ->  E. c  e.  ( Atoms `  l )
( c  =/=  a  /\  c  =/=  b  /\  c ( le `  l ) ( a ( join `  l
) b ) ) )
2423, 4, 21wral 2543 . . . . 5  wff  A. b  e.  ( Atoms `  l )
( a  =/=  b  ->  E. c  e.  (
Atoms `  l ) ( c  =/=  a  /\  c  =/=  b  /\  c
( le `  l
) ( a (
join `  l )
b ) ) )
2524, 2, 21wral 2543 . . . 4  wff  A. a  e.  ( Atoms `  l ) A. b  e.  ( Atoms `  l ) ( a  =/=  b  ->  E. c  e.  ( Atoms `  l ) ( c  =/=  a  /\  c  =/=  b  /\  c
( le `  l
) ( a (
join `  l )
b ) ) )
26 cp0 14143 . . . . . . . . . . 11  class  0.
2712, 26cfv 5255 . . . . . . . . . 10  class  ( 0.
`  l )
28 cplt 14075 . . . . . . . . . . 11  class  lt
2912, 28cfv 5255 . . . . . . . . . 10  class  ( lt
`  l )
3027, 3, 29wbr 4023 . . . . . . . . 9  wff  ( 0.
`  l ) ( lt `  l ) a
313, 5, 29wbr 4023 . . . . . . . . 9  wff  a ( lt `  l ) b
3230, 31wa 358 . . . . . . . 8  wff  ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )
335, 8, 29wbr 4023 . . . . . . . . 9  wff  b ( lt `  l ) c
34 cp1 14144 . . . . . . . . . . 11  class  1.
3512, 34cfv 5255 . . . . . . . . . 10  class  ( 1.
`  l )
368, 35, 29wbr 4023 . . . . . . . . 9  wff  c ( lt `  l ) ( 1. `  l
)
3733, 36wa 358 . . . . . . . 8  wff  ( b ( lt `  l
) c  /\  c
( lt `  l
) ( 1. `  l ) )
3832, 37wa 358 . . . . . . 7  wff  ( ( ( 0. `  l
) ( lt `  l ) a  /\  a ( lt `  l ) b )  /\  ( b ( lt `  l ) c  /\  c ( lt `  l ) ( 1. `  l
) ) )
39 cbs 13148 . . . . . . . 8  class  Base
4012, 39cfv 5255 . . . . . . 7  class  ( Base `  l )
4138, 7, 40wrex 2544 . . . . . 6  wff  E. c  e.  ( Base `  l
) ( ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )  /\  ( b ( lt
`  l ) c  /\  c ( lt
`  l ) ( 1. `  l ) ) )
4241, 4, 40wrex 2544 . . . . 5  wff  E. b  e.  ( Base `  l
) E. c  e.  ( Base `  l
) ( ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )  /\  ( b ( lt
`  l ) c  /\  c ( lt
`  l ) ( 1. `  l ) ) )
4342, 2, 40wrex 2544 . . . 4  wff  E. a  e.  ( Base `  l
) E. b  e.  ( Base `  l
) E. c  e.  ( Base `  l
) ( ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )  /\  ( b ( lt
`  l ) c  /\  c ( lt
`  l ) ( 1. `  l ) ) )
4425, 43wa 358 . . 3  wff  ( A. a  e.  ( Atoms `  l ) A. b  e.  ( Atoms `  l )
( a  =/=  b  ->  E. c  e.  (
Atoms `  l ) ( c  =/=  a  /\  c  =/=  b  /\  c
( le `  l
) ( a (
join `  l )
b ) ) )  /\  E. a  e.  ( Base `  l
) E. b  e.  ( Base `  l
) E. c  e.  ( Base `  l
) ( ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )  /\  ( b ( lt
`  l ) c  /\  c ( lt
`  l ) ( 1. `  l ) ) ) )
45 coml 29365 . . . . 5  class  OML
46 ccla 14213 . . . . 5  class  CLat
4745, 46cin 3151 . . . 4  class  ( OML 
i^i  CLat )
48 clc 29455 . . . 4  class  CvLat
4947, 48cin 3151 . . 3  class  ( ( OML  i^i  CLat )  i^i  CvLat )
5044, 11, 49crab 2547 . 2  class  { l  e.  ( ( OML 
i^i  CLat )  i^i  CvLat )  |  ( A. a  e.  ( Atoms `  l ) A. b  e.  ( Atoms `  l ) ( a  =/=  b  ->  E. c  e.  ( Atoms `  l ) ( c  =/=  a  /\  c  =/=  b  /\  c
( le `  l
) ( a (
join `  l )
b ) ) )  /\  E. a  e.  ( Base `  l
) E. b  e.  ( Base `  l
) E. c  e.  ( Base `  l
) ( ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )  /\  ( b ( lt
`  l ) c  /\  c ( lt
`  l ) ( 1. `  l ) ) ) ) }
511, 50wceq 1623 1  wff  HL  =  { l  e.  ( ( OML  i^i  CLat )  i^i  CvLat )  |  ( A. a  e.  (
Atoms `  l ) A. b  e.  ( Atoms `  l ) ( a  =/=  b  ->  E. c  e.  ( Atoms `  l )
( c  =/=  a  /\  c  =/=  b  /\  c ( le `  l ) ( a ( join `  l
) b ) ) )  /\  E. a  e.  ( Base `  l
) E. b  e.  ( Base `  l
) E. c  e.  ( Base `  l
) ( ( ( 0. `  l ) ( lt `  l
) a  /\  a
( lt `  l
) b )  /\  ( b ( lt
`  l ) c  /\  c ( lt
`  l ) ( 1. `  l ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  ishlat1  29542
  Copyright terms: Public domain W3C validator