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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlt	⊢ HL
1		vl	⊢ 𝑙
2		coml	⊢ OML
3		ccla	⊢ CLat
4	2 3	cin	⊢ ( OML ∩ CLat )
5		clc	⊢ CvLat
6	4 5	cin	⊢ ( ( OML ∩ CLat ) ∩ CvLat )
7		va	⊢ 𝑎
8		catm	⊢ Atoms
9	1	cv	⊢ 𝑙
10	9 8	cfv	⊢ ( Atoms ‘ 𝑙 )
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	⊢ le
20	9 19	cfv	⊢ ( le ‘ 𝑙 )
21		cjn	⊢ join
22	9 21	cfv	⊢ ( join ‘ 𝑙 )
23	12 13 22	co	⊢ ( 𝑎 ( join ‘ 𝑙 ) 𝑏 )
24	16 23 20	wbr	⊢ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 )
25	17 18 24	w3a	⊢ ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) )
26	25 15 10	wrex	⊢ ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) )
27	14 26	wi	⊢ ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) )
28	27 11 10	wral	⊢ ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) )
29	28 7 10	wral	⊢ ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) )
30		cbs	⊢ Base
31	9 30	cfv	⊢ ( Base ‘ 𝑙 )
32		cp0	⊢ 0.
33	9 32	cfv	⊢ ( 0. ‘ 𝑙 )
34		cplt	⊢ lt
35	9 34	cfv	⊢ ( lt ‘ 𝑙 )
36	33 12 35	wbr	⊢ ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎
37	12 13 35	wbr	⊢ 𝑎 ( lt ‘ 𝑙 ) 𝑏
38	36 37	wa	⊢ ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 )
39	13 16 35	wbr	⊢ 𝑏 ( lt ‘ 𝑙 ) 𝑐
40		cp1	⊢ 1.
41	9 40	cfv	⊢ ( 1. ‘ 𝑙 )
42	16 41 35	wbr	⊢ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 )
43	39 42	wa	⊢ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) )
44	38 43	wa	⊢ ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
45	44 15 31	wrex	⊢ ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
46	45 11 31	wrex	⊢ ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
47	46 7 31	wrex	⊢ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) )
48	29 47	wa	⊢ ( ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) ) ∧ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) ) )
49	48 1 6	crab	⊢ { 𝑙 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∣ ( ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) ) ∧ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) ) ) }
50	0 49	wceq	⊢ HL = { 𝑙 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∣ ( ∀ 𝑎 ∈ ( Atoms ‘ 𝑙 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑙 ) ( 𝑎 ≠ 𝑏 → ∃ 𝑐 ∈ ( Atoms ‘ 𝑙 ) ( 𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐 ( le ‘ 𝑙 ) ( 𝑎 ( join ‘ 𝑙 ) 𝑏 ) ) ) ∧ ∃ 𝑎 ∈ ( Base ‘ 𝑙 ) ∃ 𝑏 ∈ ( Base ‘ 𝑙 ) ∃ 𝑐 ∈ ( Base ‘ 𝑙 ) ( ( ( 0. ‘ 𝑙 ) ( lt ‘ 𝑙 ) 𝑎 ∧ 𝑎 ( lt ‘ 𝑙 ) 𝑏 ) ∧ ( 𝑏 ( lt ‘ 𝑙 ) 𝑐 ∧ 𝑐 ( lt ‘ 𝑙 ) ( 1. ‘ 𝑙 ) ) ) ) }