Step | Hyp | Ref
| Expression |
1 | | chlt 38268 |
. 2
class
HL |
2 | | va |
. . . . . . . . 9
setvar π |
3 | 2 | cv 1541 |
. . . . . . . 8
class π |
4 | | vb |
. . . . . . . . 9
setvar π |
5 | 4 | cv 1541 |
. . . . . . . 8
class π |
6 | 3, 5 | wne 2941 |
. . . . . . 7
wff π β π |
7 | | vc |
. . . . . . . . . . 11
setvar π |
8 | 7 | cv 1541 |
. . . . . . . . . 10
class π |
9 | 8, 3 | wne 2941 |
. . . . . . . . 9
wff π β π |
10 | 8, 5 | wne 2941 |
. . . . . . . . 9
wff π β π |
11 | | vl |
. . . . . . . . . . . . 13
setvar π |
12 | 11 | cv 1541 |
. . . . . . . . . . . 12
class π |
13 | | cjn 18264 |
. . . . . . . . . . . 12
class
join |
14 | 12, 13 | cfv 6544 |
. . . . . . . . . . 11
class
(joinβπ) |
15 | 3, 5, 14 | co 7409 |
. . . . . . . . . 10
class (π(joinβπ)π) |
16 | | cple 17204 |
. . . . . . . . . . 11
class
le |
17 | 12, 16 | cfv 6544 |
. . . . . . . . . 10
class
(leβπ) |
18 | 8, 15, 17 | wbr 5149 |
. . . . . . . . 9
wff π(leβπ)(π(joinβπ)π) |
19 | 9, 10, 18 | w3a 1088 |
. . . . . . . 8
wff (π β π β§ π β π β§ π(leβπ)(π(joinβπ)π)) |
20 | | catm 38181 |
. . . . . . . . 9
class
Atoms |
21 | 12, 20 | cfv 6544 |
. . . . . . . 8
class
(Atomsβπ) |
22 | 19, 7, 21 | wrex 3071 |
. . . . . . 7
wff
βπ β
(Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π)) |
23 | 6, 22 | wi 4 |
. . . . . 6
wff (π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) |
24 | 23, 4, 21 | wral 3062 |
. . . . 5
wff
βπ β
(Atomsβπ)(π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) |
25 | 24, 2, 21 | wral 3062 |
. . . 4
wff
βπ β
(Atomsβπ)βπ β (Atomsβπ)(π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) |
26 | | cp0 18376 |
. . . . . . . . . . 11
class
0. |
27 | 12, 26 | cfv 6544 |
. . . . . . . . . 10
class
(0.βπ) |
28 | | cplt 18261 |
. . . . . . . . . . 11
class
lt |
29 | 12, 28 | cfv 6544 |
. . . . . . . . . 10
class
(ltβπ) |
30 | 27, 3, 29 | wbr 5149 |
. . . . . . . . 9
wff
(0.βπ)(ltβπ)π |
31 | 3, 5, 29 | wbr 5149 |
. . . . . . . . 9
wff π(ltβπ)π |
32 | 30, 31 | wa 397 |
. . . . . . . 8
wff
((0.βπ)(ltβπ)π β§ π(ltβπ)π) |
33 | 5, 8, 29 | wbr 5149 |
. . . . . . . . 9
wff π(ltβπ)π |
34 | | cp1 18377 |
. . . . . . . . . . 11
class
1. |
35 | 12, 34 | cfv 6544 |
. . . . . . . . . 10
class
(1.βπ) |
36 | 8, 35, 29 | wbr 5149 |
. . . . . . . . 9
wff π(ltβπ)(1.βπ) |
37 | 33, 36 | wa 397 |
. . . . . . . 8
wff (π(ltβπ)π β§ π(ltβπ)(1.βπ)) |
38 | 32, 37 | wa 397 |
. . . . . . 7
wff
(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))) |
39 | | cbs 17144 |
. . . . . . . 8
class
Base |
40 | 12, 39 | cfv 6544 |
. . . . . . 7
class
(Baseβπ) |
41 | 38, 7, 40 | wrex 3071 |
. . . . . 6
wff
βπ β
(Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))) |
42 | 41, 4, 40 | wrex 3071 |
. . . . 5
wff
βπ β
(Baseβπ)βπ β (Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))) |
43 | 42, 2, 40 | wrex 3071 |
. . . 4
wff
βπ β
(Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))) |
44 | 25, 43 | wa 397 |
. . 3
wff
(βπ β
(Atomsβπ)βπ β (Atomsβπ)(π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) β§ βπ β (Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ)))) |
45 | | coml 38093 |
. . . . 5
class
OML |
46 | | ccla 18451 |
. . . . 5
class
CLat |
47 | 45, 46 | cin 3948 |
. . . 4
class (OML
β© CLat) |
48 | | clc 38183 |
. . . 4
class
CvLat |
49 | 47, 48 | cin 3948 |
. . 3
class ((OML
β© CLat) β© CvLat) |
50 | 44, 11, 49 | crab 3433 |
. 2
class {π β ((OML β© CLat) β©
CvLat) β£ (βπ
β (Atomsβπ)βπ β (Atomsβπ)(π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) β§ βπ β (Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))))} |
51 | 1, 50 | wceq 1542 |
1
wff HL = {π β ((OML β© CLat) β©
CvLat) β£ (βπ
β (Atomsβπ)βπ β (Atomsβπ)(π β π β βπ β (Atomsβπ)(π β π β§ π β π β§ π(leβπ)(π(joinβπ)π))) β§ βπ β (Baseβπ)βπ β (Baseβπ)βπ β (Baseβπ)(((0.βπ)(ltβπ)π β§ π(ltβπ)π) β§ (π(ltβπ)π β§ π(ltβπ)(1.βπ))))} |