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=lOMLCLatCvLat|aAtomslbAtomslabcAtomslcacbclajoinlbaBaselbBaselcBasel0.l<laa<lbb<lcc<l1.l

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlt classHL
1 vl setvarl
2 coml classOML
3 ccla classCLat
4 2 3 cin classOMLCLat
5 clc classCvLat
6 4 5 cin classOMLCLatCvLat
7 va setvara
8 catm classAtoms
9 1 cv setvarl
10 9 8 cfv classAtomsl
11 vb setvarb
12 7 cv setvara
13 11 cv setvarb
14 12 13 wne wffab
15 vc setvarc
16 15 cv setvarc
17 16 12 wne wffca
18 16 13 wne wffcb
19 cple classle
20 9 19 cfv classl
21 cjn classjoin
22 9 21 cfv classjoinl
23 12 13 22 co classajoinlb
24 16 23 20 wbr wffclajoinlb
25 17 18 24 w3a wffcacbclajoinlb
26 25 15 10 wrex wffcAtomslcacbclajoinlb
27 14 26 wi wffabcAtomslcacbclajoinlb
28 27 11 10 wral wffbAtomslabcAtomslcacbclajoinlb
29 28 7 10 wral wffaAtomslbAtomslabcAtomslcacbclajoinlb
30 cbs classBase
31 9 30 cfv classBasel
32 cp0 class0.
33 9 32 cfv class0.l
34 cplt classlt
35 9 34 cfv class<l
36 33 12 35 wbr wff0.l<la
37 12 13 35 wbr wffa<lb
38 36 37 wa wff0.l<laa<lb
39 13 16 35 wbr wffb<lc
40 cp1 class1.
41 9 40 cfv class1.l
42 16 41 35 wbr wffc<l1.l
43 39 42 wa wffb<lcc<l1.l
44 38 43 wa wff0.l<laa<lbb<lcc<l1.l
45 44 15 31 wrex wffcBasel0.l<laa<lbb<lcc<l1.l
46 45 11 31 wrex wffbBaselcBasel0.l<laa<lbb<lcc<l1.l
47 46 7 31 wrex wffaBaselbBaselcBasel0.l<laa<lbb<lcc<l1.l
48 29 47 wa wffaAtomslbAtomslabcAtomslcacbclajoinlbaBaselbBaselcBasel0.l<laa<lbb<lcc<l1.l
49 48 1 6 crab classlOMLCLatCvLat|aAtomslbAtomslabcAtomslcacbclajoinlbaBaselbBaselcBasel0.l<laa<lbb<lcc<l1.l
50 0 49 wceq wffHL=lOMLCLatCvLat|aAtomslbAtomslabcAtomslcacbclajoinlbaBaselbBaselcBasel0.l<laa<lbb<lcc<l1.l