Metamath Proof Explorer


Definition df-hlat

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 HL = l OML CLat CvLat | a Atoms l b Atoms l a b c Atoms l c a c b c l a join l b a Base l b Base l c Base l 0. l < l a a < l b b < l c c < l 1. l

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlt class HL
1 vl setvar l
2 coml class OML
3 ccla class CLat
4 2 3 cin class OML CLat
5 clc class CvLat
6 4 5 cin class OML CLat CvLat
7 va setvar a
8 catm class Atoms
9 1 cv setvar l
10 9 8 cfv class Atoms l
11 vb setvar b
12 7 cv setvar a
13 11 cv setvar b
14 12 13 wne wff a b
15 vc setvar c
16 15 cv setvar c
17 16 12 wne wff c a
18 16 13 wne wff c b
19 cple class le
20 9 19 cfv class l
21 cjn class join
22 9 21 cfv class join l
23 12 13 22 co class a join l b
24 16 23 20 wbr wff c l a join l b
25 17 18 24 w3a wff c a c b c l a join l b
26 25 15 10 wrex wff c Atoms l c a c b c l a join l b
27 14 26 wi wff a b c Atoms l c a c b c l a join l b
28 27 11 10 wral wff b Atoms l a b c Atoms l c a c b c l a join l b
29 28 7 10 wral wff a Atoms l b Atoms l a b c Atoms l c a c b c l a join l b
30 cbs class Base
31 9 30 cfv class Base l
32 cp0 class 0.
33 9 32 cfv class 0. l
34 cplt class lt
35 9 34 cfv class < l
36 33 12 35 wbr wff 0. l < l a
37 12 13 35 wbr wff a < l b
38 36 37 wa wff 0. l < l a a < l b
39 13 16 35 wbr wff b < l c
40 cp1 class 1.
41 9 40 cfv class 1. l
42 16 41 35 wbr wff c < l 1. l
43 39 42 wa wff b < l c c < l 1. l
44 38 43 wa wff 0. l < l a a < l b b < l c c < l 1. l
45 44 15 31 wrex wff c Base l 0. l < l a a < l b b < l c c < l 1. l
46 45 11 31 wrex wff b Base l c Base l 0. l < l a a < l b b < l c c < l 1. l
47 46 7 31 wrex wff a Base l b Base l c Base l 0. l < l a a < l b b < l c c < l 1. l
48 29 47 wa wff a Atoms l b Atoms l a b c Atoms l c a c b c l a join l b a Base l b Base l c Base l 0. l < l a a < l b b < l c c < l 1. l
49 48 1 6 crab class l OML CLat CvLat | a Atoms l b Atoms l a b c Atoms l c a c b c l a join l b a Base l b Base l c Base l 0. l < l a a < l b b < l c c < l 1. l
50 0 49 wceq wff HL = l OML CLat CvLat | a Atoms l b Atoms l a b c Atoms l c a c b c l a join l b a Base l b Base l c Base l 0. l < l a a < l b b < l c c < l 1. l