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