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 = { 𝑙 ∈ ( ( 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. ‘ 𝑙 ) ) ) ) }