Step | Hyp | Ref
| Expression |
1 | | hllat 37871 |
. . . 4
β’ (πΎ β HL β πΎ β Lat) |
2 | | hlrelat2.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | hlrelat2.l |
. . . . 5
β’ β€ =
(leβπΎ) |
4 | | eqid 2733 |
. . . . 5
β’
(ltβπΎ) =
(ltβπΎ) |
5 | | eqid 2733 |
. . . . 5
β’
(meetβπΎ) =
(meetβπΎ) |
6 | 2, 3, 4, 5 | latnlemlt 18366 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β (π(meetβπΎ)π)(ltβπΎ)π)) |
7 | 1, 6 | syl3an1 1164 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β (π(meetβπΎ)π)(ltβπΎ)π)) |
8 | | simp1 1137 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β HL) |
9 | 2, 5 | latmcl 18334 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π(meetβπΎ)π) β π΅) |
10 | 1, 9 | syl3an1 1164 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π(meetβπΎ)π) β π΅) |
11 | | simp2 1138 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β π β π΅) |
12 | | eqid 2733 |
. . . . . . 7
β’
(joinβπΎ) =
(joinβπΎ) |
13 | | hlrelat2.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
14 | 2, 3, 4, 12, 13 | hlrelat 37911 |
. . . . . 6
β’ (((πΎ β HL β§ (π(meetβπΎ)π) β π΅ β§ π β π΅) β§ (π(meetβπΎ)π)(ltβπΎ)π) β βπ β π΄ ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π)) |
15 | 14 | ex 414 |
. . . . 5
β’ ((πΎ β HL β§ (π(meetβπΎ)π) β π΅ β§ π β π΅) β ((π(meetβπΎ)π)(ltβπΎ)π β βπ β π΄ ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π))) |
16 | 8, 10, 11, 15 | syl3anc 1372 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π(meetβπΎ)π)(ltβπΎ)π β βπ β π΄ ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π))) |
17 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β πΎ β HL) |
18 | 17 | hllatd 37872 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β πΎ β Lat) |
19 | 10 | adantr 482 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (π(meetβπΎ)π) β π΅) |
20 | 2, 13 | atbase 37797 |
. . . . . . . . . 10
β’ (π β π΄ β π β π΅) |
21 | 20 | adantl 483 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
22 | | simpl2 1193 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
23 | 2, 3, 12 | latjle12 18344 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ ((π(meetβπΎ)π) β π΅ β§ π β π΅ β§ π β π΅)) β (((π(meetβπΎ)π) β€ π β§ π β€ π) β ((π(meetβπΎ)π)(joinβπΎ)π) β€ π)) |
24 | 18, 19, 21, 22, 23 | syl13anc 1373 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π) β€ π β§ π β€ π) β ((π(meetβπΎ)π)(joinβπΎ)π) β€ π)) |
25 | | simpr 486 |
. . . . . . . 8
β’ (((π(meetβπΎ)π) β€ π β§ π β€ π) β π β€ π) |
26 | 24, 25 | syl6bir 254 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π)(joinβπΎ)π) β€ π β π β€ π)) |
27 | 26 | adantld 492 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π) β π β€ π)) |
28 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
29 | 2, 3, 5 | latlem12 18360 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ (π(meetβπΎ)π))) |
30 | 18, 21, 22, 28, 29 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β ((π β€ π β§ π β€ π) β π β€ (π(meetβπΎ)π))) |
31 | 30 | notbid 318 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (Β¬ (π β€ π β§ π β€ π) β Β¬ π β€ (π(meetβπΎ)π))) |
32 | 2, 3, 4, 12 | latnle 18367 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π(meetβπΎ)π) β π΅ β§ π β π΅) β (Β¬ π β€ (π(meetβπΎ)π) β (π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π))) |
33 | 18, 19, 21, 32 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (Β¬ π β€ (π(meetβπΎ)π) β (π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π))) |
34 | 31, 33 | bitrd 279 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (Β¬ (π β€ π β§ π β€ π) β (π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π))) |
35 | 34, 24 | anbi12d 632 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β ((Β¬ (π β€ π β§ π β€ π) β§ ((π(meetβπΎ)π) β€ π β§ π β€ π)) β ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π))) |
36 | | pm3.21 473 |
. . . . . . . . . 10
β’ (π β€ π β (π β€ π β (π β€ π β§ π β€ π))) |
37 | | orcom 869 |
. . . . . . . . . . 11
β’ (((π β€ π β§ π β€ π) β¨ Β¬ π β€ π) β (Β¬ π β€ π β¨ (π β€ π β§ π β€ π))) |
38 | | pm4.55 987 |
. . . . . . . . . . 11
β’ (Β¬
(Β¬ (π β€ π β§ π β€ π) β§ π β€ π) β ((π β€ π β§ π β€ π) β¨ Β¬ π β€ π)) |
39 | | imor 852 |
. . . . . . . . . . 11
β’ ((π β€ π β (π β€ π β§ π β€ π)) β (Β¬ π β€ π β¨ (π β€ π β§ π β€ π))) |
40 | 37, 38, 39 | 3bitr4ri 304 |
. . . . . . . . . 10
β’ ((π β€ π β (π β€ π β§ π β€ π)) β Β¬ (Β¬ (π β€ π β§ π β€ π) β§ π β€ π)) |
41 | 36, 40 | sylib 217 |
. . . . . . . . 9
β’ (π β€ π β Β¬ (Β¬ (π β€ π β§ π β€ π) β§ π β€ π)) |
42 | 41 | con2i 139 |
. . . . . . . 8
β’ ((Β¬
(π β€ π β§ π β€ π) β§ π β€ π) β Β¬ π β€ π) |
43 | 42 | adantrl 715 |
. . . . . . 7
β’ ((Β¬
(π β€ π β§ π β€ π) β§ ((π(meetβπΎ)π) β€ π β§ π β€ π)) β Β¬ π β€ π) |
44 | 35, 43 | syl6bir 254 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π) β Β¬ π β€ π)) |
45 | 27, 44 | jcad 514 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π) β (π β€ π β§ Β¬ π β€ π))) |
46 | 45 | reximdva 3162 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (βπ β π΄ ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π) β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) |
47 | 16, 46 | syld 47 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π(meetβπΎ)π)(ltβπΎ)π β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) |
48 | 7, 47 | sylbid 239 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) |
49 | 2, 3 | lattr 18338 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ π)) |
50 | 18, 21, 22, 28, 49 | syl13anc 1373 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β ((π β€ π β§ π β€ π) β π β€ π)) |
51 | 50 | exp4b 432 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β π΄ β (π β€ π β (π β€ π β π β€ π)))) |
52 | 51 | com34 91 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β π΄ β (π β€ π β (π β€ π β π β€ π)))) |
53 | 52 | com23 86 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β (π β π΄ β (π β€ π β π β€ π)))) |
54 | 53 | ralrimdv 3146 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) |
55 | | iman 403 |
. . . . . 6
β’ ((π β€ π β π β€ π) β Β¬ (π β€ π β§ Β¬ π β€ π)) |
56 | 55 | ralbii 3093 |
. . . . 5
β’
(βπ β
π΄ (π β€ π β π β€ π) β βπ β π΄ Β¬ (π β€ π β§ Β¬ π β€ π)) |
57 | | ralnex 3072 |
. . . . 5
β’
(βπ β
π΄ Β¬ (π β€ π β§ Β¬ π β€ π) β Β¬ βπ β π΄ (π β€ π β§ Β¬ π β€ π)) |
58 | 56, 57 | bitri 275 |
. . . 4
β’
(βπ β
π΄ (π β€ π β π β€ π) β Β¬ βπ β π΄ (π β€ π β§ Β¬ π β€ π)) |
59 | 54, 58 | syl6ib 251 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β Β¬ βπ β π΄ (π β€ π β§ Β¬ π β€ π))) |
60 | 59 | con2d 134 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (βπ β π΄ (π β€ π β§ Β¬ π β€ π) β Β¬ π β€ π)) |
61 | 48, 60 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) |