Step | Hyp | Ref
| Expression |
1 | | hllat 38746 |
. . . 4
β’ (πΎ β HL β πΎ β Lat) |
2 | | hlrelat2.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | hlrelat2.l |
. . . . 5
β’ β€ =
(leβπΎ) |
4 | | eqid 2726 |
. . . . 5
β’
(ltβπΎ) =
(ltβπΎ) |
5 | | eqid 2726 |
. . . . 5
β’
(meetβπΎ) =
(meetβπΎ) |
6 | 2, 3, 4, 5 | latnlemlt 18437 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β (π(meetβπΎ)π)(ltβπΎ)π)) |
7 | 1, 6 | syl3an1 1160 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β (π(meetβπΎ)π)(ltβπΎ)π)) |
8 | | simp1 1133 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β HL) |
9 | 2, 5 | latmcl 18405 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π(meetβπΎ)π) β π΅) |
10 | 1, 9 | syl3an1 1160 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π(meetβπΎ)π) β π΅) |
11 | | simp2 1134 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β π β π΅) |
12 | | eqid 2726 |
. . . . . . 7
β’
(joinβπΎ) =
(joinβπΎ) |
13 | | hlrelat2.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
14 | 2, 3, 4, 12, 13 | hlrelat 38786 |
. . . . . 6
β’ (((πΎ β HL β§ (π(meetβπΎ)π) β π΅ β§ π β π΅) β§ (π(meetβπΎ)π)(ltβπΎ)π) β βπ β π΄ ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π)) |
15 | 14 | ex 412 |
. . . . 5
β’ ((πΎ β HL β§ (π(meetβπΎ)π) β π΅ β§ π β π΅) β ((π(meetβπΎ)π)(ltβπΎ)π β βπ β π΄ ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π))) |
16 | 8, 10, 11, 15 | syl3anc 1368 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π(meetβπΎ)π)(ltβπΎ)π β βπ β π΄ ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π))) |
17 | | simpl1 1188 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β πΎ β HL) |
18 | 17 | hllatd 38747 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β πΎ β Lat) |
19 | 10 | adantr 480 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (π(meetβπΎ)π) β π΅) |
20 | 2, 13 | atbase 38672 |
. . . . . . . . . 10
β’ (π β π΄ β π β π΅) |
21 | 20 | adantl 481 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
22 | | simpl2 1189 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
23 | 2, 3, 12 | latjle12 18415 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ ((π(meetβπΎ)π) β π΅ β§ π β π΅ β§ π β π΅)) β (((π(meetβπΎ)π) β€ π β§ π β€ π) β ((π(meetβπΎ)π)(joinβπΎ)π) β€ π)) |
24 | 18, 19, 21, 22, 23 | syl13anc 1369 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π) β€ π β§ π β€ π) β ((π(meetβπΎ)π)(joinβπΎ)π) β€ π)) |
25 | | simpr 484 |
. . . . . . . 8
β’ (((π(meetβπΎ)π) β€ π β§ π β€ π) β π β€ π) |
26 | 24, 25 | syl6bir 254 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π)(joinβπΎ)π) β€ π β π β€ π)) |
27 | 26 | adantld 490 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π) β π β€ π)) |
28 | | simpl3 1190 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
29 | 2, 3, 5 | latlem12 18431 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ (π(meetβπΎ)π))) |
30 | 18, 21, 22, 28, 29 | syl13anc 1369 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β ((π β€ π β§ π β€ π) β π β€ (π(meetβπΎ)π))) |
31 | 30 | notbid 318 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (Β¬ (π β€ π β§ π β€ π) β Β¬ π β€ (π(meetβπΎ)π))) |
32 | 2, 3, 4, 12 | latnle 18438 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π(meetβπΎ)π) β π΅ β§ π β π΅) β (Β¬ π β€ (π(meetβπΎ)π) β (π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π))) |
33 | 18, 19, 21, 32 | syl3anc 1368 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (Β¬ π β€ (π(meetβπΎ)π) β (π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π))) |
34 | 31, 33 | bitrd 279 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (Β¬ (π β€ π β§ π β€ π) β (π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π))) |
35 | 34, 24 | anbi12d 630 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β ((Β¬ (π β€ π β§ π β€ π) β§ ((π(meetβπΎ)π) β€ π β§ π β€ π)) β ((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π))) |
36 | | pm3.21 471 |
. . . . . . . . . 10
β’ (π β€ π β (π β€ π β (π β€ π β§ π β€ π))) |
37 | | orcom 867 |
. . . . . . . . . . 11
β’ (((π β€ π β§ π β€ π) β¨ Β¬ π β€ π) β (Β¬ π β€ π β¨ (π β€ π β§ π β€ π))) |
38 | | pm4.55 984 |
. . . . . . . . . . 11
β’ (Β¬
(Β¬ (π β€ π β§ π β€ π) β§ π β€ π) β ((π β€ π β§ π β€ π) β¨ Β¬ π β€ π)) |
39 | | imor 850 |
. . . . . . . . . . 11
β’ ((π β€ π β (π β€ π β§ π β€ π)) β (Β¬ π β€ π β¨ (π β€ π β§ π β€ π))) |
40 | 37, 38, 39 | 3bitr4ri 304 |
. . . . . . . . . 10
β’ ((π β€ π β (π β€ π β§ π β€ π)) β Β¬ (Β¬ (π β€ π β§ π β€ π) β§ π β€ π)) |
41 | 36, 40 | sylib 217 |
. . . . . . . . 9
β’ (π β€ π β Β¬ (Β¬ (π β€ π β§ π β€ π) β§ π β€ π)) |
42 | 41 | con2i 139 |
. . . . . . . 8
β’ ((Β¬
(π β€ π β§ π β€ π) β§ π β€ π) β Β¬ π β€ π) |
43 | 42 | adantrl 713 |
. . . . . . 7
β’ ((Β¬
(π β€ π β§ π β€ π) β§ ((π(meetβπΎ)π) β€ π β§ π β€ π)) β Β¬ π β€ π) |
44 | 35, 43 | syl6bir 254 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β (((π(meetβπΎ)π)(ltβπΎ)((π(meetβπΎ)π)(joinβπΎ)π) β§ ((π(meetβπΎ)π)(joinβπΎ)π) β€ π) β Β¬ π β€ π)) |
45 | 27, 44 | jcad 512 |
. . . . 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 18409 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ π)) |
50 | 18, 21, 22, 28, 49 | syl13anc 1369 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΄) β ((π β€ π β§ π β€ π) β π β€ π)) |
51 | 50 | exp4b 430 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β π΄ β (π β€ π β (π β€ π β π β€ π)))) |
52 | 51 | com34 91 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β π΄ β (π β€ π β (π β€ π β π β€ π)))) |
53 | 52 | com23 86 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β (π β π΄ β (π β€ π β π β€ π)))) |
54 | 53 | ralrimdv 3146 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) |
55 | | iman 401 |
. . . . . 6
β’ ((π β€ π β π β€ π) β Β¬ (π β€ π β§ Β¬ π β€ π)) |
56 | 55 | ralbii 3087 |
. . . . 5
β’
(βπ β
π΄ (π β€ π β π β€ π) β βπ β π΄ Β¬ (π β€ π β§ Β¬ π β€ π)) |
57 | | ralnex 3066 |
. . . . 5
β’
(βπ β
π΄ Β¬ (π β€ π β§ Β¬ π β€ π) β Β¬ βπ β π΄ (π β€ π β§ Β¬ π β€ π)) |
58 | 56, 57 | bitri 275 |
. . . 4
β’
(βπ β
π΄ (π β€ π β π β€ π) β Β¬ βπ β π΄ (π β€ π β§ Β¬ π β€ π)) |
59 | 54, 58 | imbitrdi 250 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β Β¬ βπ β π΄ (π β€ π β§ Β¬ π β€ π))) |
60 | 59 | con2d 134 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (βπ β π΄ (π β€ π β§ Β¬ π β€ π) β Β¬ π β€ π)) |
61 | 48, 60 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) |