Step |
Hyp |
Ref |
Expression |
0 |
|
chlt |
|- HL |
1 |
|
vl |
|- l |
2 |
|
coml |
|- OML |
3 |
|
ccla |
|- CLat |
4 |
2 3
|
cin |
|- ( OML i^i CLat ) |
5 |
|
clc |
|- CvLat |
6 |
4 5
|
cin |
|- ( ( OML i^i CLat ) i^i CvLat ) |
7 |
|
va |
|- a |
8 |
|
catm |
|- Atoms |
9 |
1
|
cv |
|- l |
10 |
9 8
|
cfv |
|- ( Atoms ` l ) |
11 |
|
vb |
|- b |
12 |
7
|
cv |
|- a |
13 |
11
|
cv |
|- b |
14 |
12 13
|
wne |
|- a =/= b |
15 |
|
vc |
|- c |
16 |
15
|
cv |
|- c |
17 |
16 12
|
wne |
|- c =/= a |
18 |
16 13
|
wne |
|- c =/= b |
19 |
|
cple |
|- le |
20 |
9 19
|
cfv |
|- ( le ` l ) |
21 |
|
cjn |
|- join |
22 |
9 21
|
cfv |
|- ( join ` l ) |
23 |
12 13 22
|
co |
|- ( a ( join ` l ) b ) |
24 |
16 23 20
|
wbr |
|- c ( le ` l ) ( a ( join ` l ) b ) |
25 |
17 18 24
|
w3a |
|- ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) |
26 |
25 15 10
|
wrex |
|- E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) |
27 |
14 26
|
wi |
|- ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) |
28 |
27 11 10
|
wral |
|- A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) |
29 |
28 7 10
|
wral |
|- A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) |
30 |
|
cbs |
|- Base |
31 |
9 30
|
cfv |
|- ( Base ` l ) |
32 |
|
cp0 |
|- 0. |
33 |
9 32
|
cfv |
|- ( 0. ` l ) |
34 |
|
cplt |
|- lt |
35 |
9 34
|
cfv |
|- ( lt ` l ) |
36 |
33 12 35
|
wbr |
|- ( 0. ` l ) ( lt ` l ) a |
37 |
12 13 35
|
wbr |
|- a ( lt ` l ) b |
38 |
36 37
|
wa |
|- ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) |
39 |
13 16 35
|
wbr |
|- b ( lt ` l ) c |
40 |
|
cp1 |
|- 1. |
41 |
9 40
|
cfv |
|- ( 1. ` l ) |
42 |
16 41 35
|
wbr |
|- c ( lt ` l ) ( 1. ` l ) |
43 |
39 42
|
wa |
|- ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) |
44 |
38 43
|
wa |
|- ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) |
45 |
44 15 31
|
wrex |
|- E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) |
46 |
45 11 31
|
wrex |
|- E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) |
47 |
46 7 31
|
wrex |
|- E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) |
48 |
29 47
|
wa |
|- ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) ) |
49 |
48 1 6
|
crab |
|- { l e. ( ( OML i^i CLat ) i^i CvLat ) | ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) ) } |
50 |
0 49
|
wceq |
|- HL = { l e. ( ( OML i^i CLat ) i^i CvLat ) | ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) ) } |