Step | Hyp | Ref
| Expression |
1 | | simp2r 1201 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β€ π) |
2 | | simp3r 1203 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β€ π) |
3 | | simp1l 1198 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β πΎ β HL) |
4 | 3 | hllatd 37712 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β πΎ β Lat) |
5 | | simp2l 1200 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β π΄) |
6 | | eqid 2738 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | | lhp2lt.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
8 | 6, 7 | atbase 37637 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
9 | 5, 8 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β (BaseβπΎ)) |
10 | | simp3l 1202 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β π΄) |
11 | 6, 7 | atbase 37637 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β (BaseβπΎ)) |
13 | | simp1r 1199 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β π») |
14 | | lhp2lt.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
15 | 6, 14 | lhpbase 38347 |
. . . . 5
β’ (π β π» β π β (BaseβπΎ)) |
16 | 13, 15 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β (BaseβπΎ)) |
17 | | lhp2lt.l |
. . . . 5
β’ β€ =
(leβπΎ) |
18 | | lhp2lt.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
19 | 6, 17, 18 | latjle12 18274 |
. . . 4
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
20 | 4, 9, 12, 16, 19 | syl13anc 1373 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
21 | 1, 2, 20 | mpbi2and 711 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β¨ π) β€ π) |
22 | 18, 17, 7 | 3dim2 37817 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
23 | 3, 5, 10, 22 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
24 | | simp11l 1285 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β πΎ β HL) |
25 | | hlop 37710 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OP) |
26 | 24, 25 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β πΎ β OP) |
27 | 24 | hllatd 37712 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β πΎ β Lat) |
28 | | simp12l 1287 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β π β π΄) |
29 | | simp13l 1289 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β π β π΄) |
30 | 6, 18, 7 | hlatjcl 37715 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
31 | 24, 28, 29, 30 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β (π β¨ π) β (BaseβπΎ)) |
32 | | simp2l 1200 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β π β π΄) |
33 | 6, 7 | atbase 37637 |
. . . . . . . . . 10
β’ (π β π΄ β π β (BaseβπΎ)) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β π β (BaseβπΎ)) |
35 | 6, 18 | latjcl 18263 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
36 | 27, 31, 34, 35 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
37 | | simp2r 1201 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β π β π΄) |
38 | 6, 7 | atbase 37637 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β π β (BaseβπΎ)) |
40 | 6, 18 | latjcl 18263 |
. . . . . . . 8
β’ ((πΎ β Lat β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((π β¨ π) β¨ π) β¨ π ) β (BaseβπΎ)) |
41 | 27, 36, 39, 40 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β (((π β¨ π) β¨ π) β¨ π ) β (BaseβπΎ)) |
42 | | eqid 2738 |
. . . . . . . 8
β’
(1.βπΎ) =
(1.βπΎ) |
43 | | eqid 2738 |
. . . . . . . 8
β’ ( β
βπΎ) = ( β
βπΎ) |
44 | 6, 42, 43 | ncvr1 37620 |
. . . . . . 7
β’ ((πΎ β OP β§ (((π β¨ π) β¨ π) β¨ π ) β (BaseβπΎ)) β Β¬ (1.βπΎ)( β βπΎ)(((π β¨ π) β¨ π) β¨ π )) |
45 | 26, 41, 44 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β Β¬ (1.βπΎ)( β βπΎ)(((π β¨ π) β¨ π) β¨ π )) |
46 | | eqid 2738 |
. . . . . . . . . . . 12
β’
(lubβπΎ) =
(lubβπΎ) |
47 | | simpl1l 1225 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β πΎ β HL) |
48 | 47 | hllatd 37712 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β πΎ β Lat) |
49 | | simpl2l 1227 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β π β π΄) |
50 | | simpl3l 1229 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β π β π΄) |
51 | 47, 49, 50, 30 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (π β¨ π) β (BaseβπΎ)) |
52 | | simpr1l 1231 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β π β π΄) |
53 | 52, 33 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β π β (BaseβπΎ)) |
54 | 48, 51, 53, 35 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
55 | 47, 25 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β πΎ β OP) |
56 | | eqid 2738 |
. . . . . . . . . . . . . . 15
β’
(glbβπΎ) =
(glbβπΎ) |
57 | 6, 46, 56 | op01dm 37531 |
. . . . . . . . . . . . . 14
β’ (πΎ β OP β
((BaseβπΎ) β dom
(lubβπΎ) β§
(BaseβπΎ) β dom
(glbβπΎ))) |
58 | 57 | simpld 496 |
. . . . . . . . . . . . 13
β’ (πΎ β OP β
(BaseβπΎ) β dom
(lubβπΎ)) |
59 | 55, 58 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (BaseβπΎ) β dom (lubβπΎ)) |
60 | 6, 46, 17, 42, 47, 54, 59 | ple1 18254 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β ((π β¨ π) β¨ π) β€ (1.βπΎ)) |
61 | | hlpos 37714 |
. . . . . . . . . . . . 13
β’ (πΎ β HL β πΎ β Poset) |
62 | 47, 61 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β πΎ β Poset) |
63 | 6, 42 | op1cl 37533 |
. . . . . . . . . . . . 13
β’ (πΎ β OP β
(1.βπΎ) β
(BaseβπΎ)) |
64 | 55, 63 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (1.βπΎ) β (BaseβπΎ)) |
65 | | simpr2l 1233 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β Β¬ π β€ (π β¨ π)) |
66 | 6, 17, 18, 43, 7 | cvr1 37759 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β¨ π) β (BaseβπΎ) β§ π β π΄) β (Β¬ π β€ (π β¨ π) β (π β¨ π)( β βπΎ)((π β¨ π) β¨ π))) |
67 | 47, 51, 52, 66 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (Β¬ π β€ (π β¨ π) β (π β¨ π)( β βπΎ)((π β¨ π) β¨ π))) |
68 | 65, 67 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (π β¨ π)( β βπΎ)((π β¨ π) β¨ π)) |
69 | | simpr3 1197 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (π β¨ π) = π) |
70 | | simpl1r 1226 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β π β π») |
71 | 42, 43, 14 | lhp1cvr 38348 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ π β π») β π( β βπΎ)(1.βπΎ)) |
72 | 47, 70, 71 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β π( β βπΎ)(1.βπΎ)) |
73 | 69, 72 | eqbrtrd 5126 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (π β¨ π)( β βπΎ)(1.βπΎ)) |
74 | 6, 17, 43 | cvrcmp 37631 |
. . . . . . . . . . . 12
β’ ((πΎ β Poset β§ (((π β¨ π) β¨ π) β (BaseβπΎ) β§ (1.βπΎ) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ ((π β¨ π)( β βπΎ)((π β¨ π) β¨ π) β§ (π β¨ π)( β βπΎ)(1.βπΎ))) β (((π β¨ π) β¨ π) β€ (1.βπΎ) β ((π β¨ π) β¨ π) = (1.βπΎ))) |
75 | 62, 54, 64, 51, 68, 73, 74 | syl132anc 1389 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (((π β¨ π) β¨ π) β€ (1.βπΎ) β ((π β¨ π) β¨ π) = (1.βπΎ))) |
76 | 60, 75 | mpbid 231 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β ((π β¨ π) β¨ π) = (1.βπΎ)) |
77 | | simpr2r 1234 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β Β¬ π β€ ((π β¨ π) β¨ π)) |
78 | | simpr1r 1232 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β π β π΄) |
79 | 6, 17, 18, 43, 7 | cvr1 37759 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β π΄) β (Β¬ π β€ ((π β¨ π) β¨ π) β ((π β¨ π) β¨ π)( β βπΎ)(((π β¨ π) β¨ π) β¨ π ))) |
80 | 47, 54, 78, 79 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (Β¬ π β€ ((π β¨ π) β¨ π) β ((π β¨ π) β¨ π)( β βπΎ)(((π β¨ π) β¨ π) β¨ π ))) |
81 | 77, 80 | mpbid 231 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β ((π β¨ π) β¨ π)( β βπΎ)(((π β¨ π) β¨ π) β¨ π )) |
82 | 76, 81 | eqbrtrrd 5128 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β¨ π) = π)) β (1.βπΎ)( β βπΎ)(((π β¨ π) β¨ π) β¨ π )) |
83 | 82 | 3exp2 1355 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β π΄ β§ π β π΄) β ((Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β ((π β¨ π) = π β (1.βπΎ)( β βπΎ)(((π β¨ π) β¨ π) β¨ π ))))) |
84 | 83 | 3imp 1112 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β ((π β¨ π) = π β (1.βπΎ)( β βπΎ)(((π β¨ π) β¨ π) β¨ π ))) |
85 | 84 | necon3bd 2956 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β (Β¬ (1.βπΎ)( β βπΎ)(((π β¨ π) β¨ π) β¨ π ) β (π β¨ π) β π)) |
86 | 45, 85 | mpd 15 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) β (π β¨ π) β π) |
87 | 86 | 3exp 1120 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β π΄ β§ π β π΄) β ((Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β (π β¨ π) β π))) |
88 | 87 | rexlimdvv 3203 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β (βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β (π β¨ π) β π)) |
89 | 23, 88 | mpd 15 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β¨ π) β π) |
90 | 3, 5, 10, 30 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β¨ π) β (BaseβπΎ)) |
91 | | lhp2lt.s |
. . . 4
β’ < =
(ltβπΎ) |
92 | 17, 91 | pltval 18156 |
. . 3
β’ ((πΎ β HL β§ (π β¨ π) β (BaseβπΎ) β§ π β π») β ((π β¨ π) < π β ((π β¨ π) β€ π β§ (π β¨ π) β π))) |
93 | 3, 90, 13, 92 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β¨ π) < π β ((π β¨ π) β€ π β§ (π β¨ π) β π))) |
94 | 21, 89, 93 | mpbir2and 712 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β¨ π) < π) |