Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β (πΎ β HL β§ π β π»)) |
2 | | lhpex1.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | lhpex1.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
4 | | lhpex1.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | 2, 3, 4 | lhpexle2 38519 |
. . . 4
β’ ((πΎ β HL β§ π β π») β βπ β π΄ (π β€ π β§ π β π β§ π β π)) |
6 | 1, 5 | syl 17 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β βπ β π΄ (π β€ π β§ π β π β§ π β π)) |
7 | | simp31 1210 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β§ π β π΄ β§ (π β€ π β§ π β π β§ π β π)) β π β€ π) |
8 | | simp32 1211 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β§ π β π΄ β§ (π β€ π β§ π β π β§ π β π)) β π β π) |
9 | | simp1r 1199 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β§ π β π΄ β§ (π β€ π β§ π β π β§ π β π)) β π = π) |
10 | 8, 9 | neeqtrd 3010 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β§ π β π΄ β§ (π β€ π β§ π β π β§ π β π)) β π β π) |
11 | | simp33 1212 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β§ π β π΄ β§ (π β€ π β§ π β π β§ π β π)) β π β π) |
12 | 8, 10, 11 | 3jca 1129 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β§ π β π΄ β§ (π β€ π β§ π β π β§ π β π)) β (π β π β§ π β π β§ π β π)) |
13 | 7, 12 | jca 513 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β§ π β π΄ β§ (π β€ π β§ π β π β§ π β π)) β (π β€ π β§ (π β π β§ π β π β§ π β π))) |
14 | 13 | 3exp 1120 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β (π β π΄ β ((π β€ π β§ π β π β§ π β π) β (π β€ π β§ (π β π β§ π β π β§ π β π))))) |
15 | 14 | reximdvai 3159 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β (βπ β π΄ (π β€ π β§ π β π β§ π β π) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π)))) |
16 | 6, 15 | mpd 15 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π = π) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) |
17 | | simprrr 781 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β€ π) |
18 | | simp11l 1285 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β πΎ β HL) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β πΎ β HL) |
20 | 19 | hllatd 37872 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β πΎ β Lat) |
21 | | eqid 2733 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
22 | 21, 3 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
23 | 22 | ad2antrl 727 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β (BaseβπΎ)) |
24 | | simp121 1306 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β π β π΄) |
25 | 24 | adantr 482 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β π΄) |
26 | 21, 3 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β (BaseβπΎ)) |
28 | | simp122 1307 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β π β π΄) |
29 | 28 | adantr 482 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β π΄) |
30 | 21, 3 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β (BaseβπΎ)) |
32 | | simprrl 780 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β Β¬ π β€ (π(joinβπΎ)π)) |
33 | | eqid 2733 |
. . . . . . . . 9
β’
(joinβπΎ) =
(joinβπΎ) |
34 | 21, 2, 33 | latnlej1l 18351 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π) |
35 | 20, 23, 27, 31, 32, 34 | syl131anc 1384 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β π) |
36 | 21, 2, 33 | latnlej1r 18352 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π) |
37 | 20, 23, 27, 31, 32, 36 | syl131anc 1384 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β π) |
38 | | simpl3 1194 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β€ (π(joinβπΎ)π)) |
39 | | nbrne2 5126 |
. . . . . . . . 9
β’ ((π β€ (π(joinβπΎ)π) β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π) |
40 | 39 | necomd 2996 |
. . . . . . . 8
β’ ((π β€ (π(joinβπΎ)π) β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π) |
41 | 38, 32, 40 | syl2anc 585 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β π β π) |
42 | 35, 37, 41 | 3jca 1129 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β (π β π β§ π β π β§ π β π)) |
43 | 17, 42 | jca 513 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) β (π β€ π β§ (π β π β§ π β π β§ π β π))) |
44 | | simp11 1204 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β (πΎ β HL β§ π β π»)) |
45 | | simp131 1309 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β π β€ π) |
46 | | simp132 1310 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β π β€ π) |
47 | | eqid 2733 |
. . . . . . . 8
β’
(ltβπΎ) =
(ltβπΎ) |
48 | 2, 47, 33, 3, 4 | lhp2lt 38510 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π(joinβπΎ)π)(ltβπΎ)π) |
49 | 44, 24, 45, 28, 46, 48 | syl122anc 1380 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β (π(joinβπΎ)π)(ltβπΎ)π) |
50 | 21, 33, 3 | hlatjcl 37875 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π(joinβπΎ)π) β (BaseβπΎ)) |
51 | 18, 24, 28, 50 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β (π(joinβπΎ)π) β (BaseβπΎ)) |
52 | | simp11r 1286 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β π β π») |
53 | 21, 4 | lhpbase 38507 |
. . . . . . . 8
β’ (π β π» β π β (BaseβπΎ)) |
54 | 52, 53 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β π β (BaseβπΎ)) |
55 | 21, 2, 47, 3 | hlrelat1 37909 |
. . . . . . 7
β’ ((πΎ β HL β§ (π(joinβπΎ)π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π(joinβπΎ)π)(ltβπΎ)π β βπ β π΄ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) |
56 | 18, 51, 54, 55 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β ((π(joinβπΎ)π)(ltβπΎ)π β βπ β π΄ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π))) |
57 | 49, 56 | mpd 15 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β βπ β π΄ (Β¬ π β€ (π(joinβπΎ)π) β§ π β€ π)) |
58 | 43, 57 | reximddv 3165 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ π β€ (π(joinβπΎ)π)) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) |
59 | 58 | 3expa 1119 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π) β§ π β€ (π(joinβπΎ)π)) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) |
60 | | simp11l 1285 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β πΎ β HL) |
61 | 60 | adantr 482 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β πΎ β HL) |
62 | 61 | hllatd 37872 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β πΎ β Lat) |
63 | 22 | ad2antrl 727 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β (BaseβπΎ)) |
64 | | simp121 1306 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π΄) |
65 | 64 | adantr 482 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β π΄) |
66 | | simp122 1307 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π΄) |
67 | 66 | adantr 482 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β π΄) |
68 | 61, 65, 67, 50 | syl3anc 1372 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β (π(joinβπΎ)π) β (BaseβπΎ)) |
69 | | simp11r 1286 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π») |
70 | 69 | adantr 482 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β π») |
71 | 70, 53 | syl 17 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β (BaseβπΎ)) |
72 | | simprr3 1224 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β€ (π(joinβπΎ)π)) |
73 | | simp131 1309 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β π β€ π) |
74 | 73 | adantr 482 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β€ π) |
75 | | simp132 1310 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β π β€ π) |
76 | 75 | adantr 482 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β€ π) |
77 | 65, 26 | syl 17 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β (BaseβπΎ)) |
78 | 67, 30 | syl 17 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β (BaseβπΎ)) |
79 | 21, 2, 33 | latjle12 18344 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β€ π β§ π β€ π) β (π(joinβπΎ)π) β€ π)) |
80 | 62, 77, 78, 71, 79 | syl13anc 1373 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β ((π β€ π β§ π β€ π) β (π(joinβπΎ)π) β€ π)) |
81 | 74, 76, 80 | mpbi2and 711 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β (π(joinβπΎ)π) β€ π) |
82 | 21, 2, 62, 63, 68, 71, 72, 81 | lattrd 18340 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β€ π) |
83 | | simprr1 1222 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β π) |
84 | | simprr2 1223 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β π) |
85 | | simpl3 1194 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β Β¬ π β€ (π(joinβπΎ)π)) |
86 | | nbrne2 5126 |
. . . . . . . 8
β’ ((π β€ (π(joinβπΎ)π) β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π) |
87 | 72, 85, 86 | syl2anc 585 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β π β π) |
88 | 83, 84, 87 | 3jca 1129 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β (π β π β§ π β π β§ π β π)) |
89 | 82, 88 | jca 513 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π)))) β (π β€ π β§ (π β π β§ π β π β§ π β π))) |
90 | | simp2 1138 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β π β π) |
91 | 2, 33, 3 | hlsupr 37895 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β βπ β π΄ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π))) |
92 | 60, 64, 66, 90, 91 | syl31anc 1374 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β βπ β π΄ (π β π β§ π β π β§ π β€ (π(joinβπΎ)π))) |
93 | 89, 92 | reximddv 3165 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π β§ Β¬ π β€ (π(joinβπΎ)π)) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) |
94 | 93 | 3expa 1119 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π) β§ Β¬ π β€ (π(joinβπΎ)π)) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) |
95 | 59, 94 | pm2.61dan 812 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β§ π β π) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) |
96 | 16, 95 | pm2.61dane 3029 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) |