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)
Ref | Expression | ||
---|---|---|---|
Assertion | df-hlat | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | chlt | |
|
1 | vl | |
|
2 | coml | |
|
3 | ccla | |
|
4 | 2 3 | cin | |
5 | clc | |
|
6 | 4 5 | cin | |
7 | va | |
|
8 | catm | |
|
9 | 1 | cv | |
10 | 9 8 | cfv | |
11 | vb | |
|
12 | 7 | cv | |
13 | 11 | cv | |
14 | 12 13 | wne | |
15 | vc | |
|
16 | 15 | cv | |
17 | 16 12 | wne | |
18 | 16 13 | wne | |
19 | cple | |
|
20 | 9 19 | cfv | |
21 | cjn | |
|
22 | 9 21 | cfv | |
23 | 12 13 22 | co | |
24 | 16 23 20 | wbr | |
25 | 17 18 24 | w3a | |
26 | 25 15 10 | wrex | |
27 | 14 26 | wi | |
28 | 27 11 10 | wral | |
29 | 28 7 10 | wral | |
30 | cbs | |
|
31 | 9 30 | cfv | |
32 | cp0 | |
|
33 | 9 32 | cfv | |
34 | cplt | |
|
35 | 9 34 | cfv | |
36 | 33 12 35 | wbr | |
37 | 12 13 35 | wbr | |
38 | 36 37 | wa | |
39 | 13 16 35 | wbr | |
40 | cp1 | |
|
41 | 9 40 | cfv | |
42 | 16 41 35 | wbr | |
43 | 39 42 | wa | |
44 | 38 43 | wa | |
45 | 44 15 31 | wrex | |
46 | 45 11 31 | wrex | |
47 | 46 7 31 | wrex | |
48 | 29 47 | wa | |
49 | 48 1 6 | crab | |
50 | 0 49 | wceq | |