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. ‘ 𝑙 ) ) ) ) } |