Definition df-hlat 37292

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 = {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙))))}

Distinct variable group:   𝑐,𝑙,𝑎,𝑏

Detailed syntax breakdown of Definition df-hlat

Step	Hyp	Ref	Expression
1		chlt 37291	. 2 class HL
2		va	. . . . . . . . 9 setvar 𝑎
3	2	cv 1538	. . . . . . . 8 class 𝑎
4		vb	. . . . . . . . 9 setvar 𝑏
5	4	cv 1538	. . . . . . . 8 class 𝑏
6	3, 5	wne 2942	. . . . . . 7 wff 𝑎 ≠ 𝑏
7		vc	. . . . . . . . . . 11 setvar 𝑐
8	7	cv 1538	. . . . . . . . . 10 class 𝑐
9	8, 3	wne 2942	. . . . . . . . 9 wff 𝑐 ≠ 𝑎
10	8, 5	wne 2942	. . . . . . . . 9 wff 𝑐 ≠ 𝑏
11		vl	. . . . . . . . . . . . 13 setvar 𝑙
12	11	cv 1538	. . . . . . . . . . . 12 class 𝑙
13		cjn 17944	. . . . . . . . . . . 12 class join
14	12, 13	cfv 6418	. . . . . . . . . . 11 class (join‘𝑙)
15	3, 5, 14	co 7255	. . . . . . . . . 10 class (𝑎(join‘𝑙)𝑏)
16		cple 16895	. . . . . . . . . . 11 class le
17	12, 16	cfv 6418	. . . . . . . . . 10 class (le‘𝑙)
18	8, 15, 17	wbr 5070	. . . . . . . . 9 wff 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)
19	9, 10, 18	w3a 1085	. . . . . . . 8 wff (𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))
20		catm 37204	. . . . . . . . 9 class Atoms
21	12, 20	cfv 6418	. . . . . . . 8 class (Atoms‘𝑙)
22	19, 7, 21	wrex 3064	. . . . . . 7 wff ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))
23	6, 22	wi 4	. . . . . 6 wff (𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
24	23, 4, 21	wral 3063	. . . . 5 wff ∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
25	24, 2, 21	wral 3063	. . . 4 wff ∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
26		cp0 18056	. . . . . . . . . . 11 class 0.
27	12, 26	cfv 6418	. . . . . . . . . 10 class (0.‘𝑙)
28		cplt 17941	. . . . . . . . . . 11 class lt
29	12, 28	cfv 6418	. . . . . . . . . 10 class (lt‘𝑙)
30	27, 3, 29	wbr 5070	. . . . . . . . 9 wff (0.‘𝑙)(lt‘𝑙)𝑎
31	3, 5, 29	wbr 5070	. . . . . . . . 9 wff 𝑎(lt‘𝑙)𝑏
32	30, 31	wa 395	. . . . . . . 8 wff ((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏)
33	5, 8, 29	wbr 5070	. . . . . . . . 9 wff 𝑏(lt‘𝑙)𝑐
34		cp1 18057	. . . . . . . . . . 11 class 1.
35	12, 34	cfv 6418	. . . . . . . . . 10 class (1.‘𝑙)
36	8, 35, 29	wbr 5070	. . . . . . . . 9 wff 𝑐(lt‘𝑙)(1.‘𝑙)
37	33, 36	wa 395	. . . . . . . 8 wff (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙))
38	32, 37	wa 395	. . . . . . 7 wff (((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙)))
39		cbs 16840	. . . . . . . 8 class Base
40	12, 39	cfv 6418	. . . . . . 7 class (Base‘𝑙)
41	38, 7, 40	wrex 3064	. . . . . 6 wff ∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙)))
42	41, 4, 40	wrex 3064	. . . . 5 wff ∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙)))
43	42, 2, 40	wrex 3064	. . . 4 wff ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙)))
44	25, 43	wa 395	. . 3 wff (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙))))
45		coml 37116	. . . . 5 class OML
46		ccla 18131	. . . . 5 class CLat
47	45, 46	cin 3882	. . . 4 class (OML ∩ CLat)
48		clc 37206	. . . 4 class CvLat
49	47, 48	cin 3882	. . 3 class ((OML ∩ CLat) ∩ CvLat)
50	44, 11, 49	crab 3067	. 2 class {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙))))}
51	1, 50	wceq 1539	1 wff HL = {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙))))}

This definition is referenced by:  ishlat1  37293