Step | Hyp | Ref
| Expression |
1 | | cdleme0.l |
. . 3
β’ β€ =
(leβπΎ) |
2 | | cdleme0.j |
. . 3
β’ β¨ =
(joinβπΎ) |
3 | | cdleme0.m |
. . 3
β’ β§ =
(meetβπΎ) |
4 | | cdleme0.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
5 | | cdleme0.h |
. . 3
β’ π» = (LHypβπΎ) |
6 | | cdleme0.u |
. . 3
β’ π = ((π β¨ π) β§ π) |
7 | 1, 2, 3, 4, 5, 6 | cdleme01N 39605 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((π β π β§ π β π β§ π β€ (π β¨ π)) β§ π β€ π)) |
8 | | simp1l 1194 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β πΎ β HL) |
9 | | hlcvl 38742 |
. . . . 5
β’ (πΎ β HL β πΎ β CvLat) |
10 | 8, 9 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β πΎ β CvLat) |
11 | | simp2ll 1237 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π΄) |
12 | | simp2rl 1239 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π΄) |
13 | | simp1 1133 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (πΎ β HL β§ π β π»)) |
14 | | simp2l 1196 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (π β π΄ β§ Β¬ π β€ π)) |
15 | | simp3 1135 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π) |
16 | 1, 2, 3, 4, 5, 6 | lhpat2 39429 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) |
17 | 13, 14, 12, 15, 16 | syl112anc 1371 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π΄) |
18 | 4, 1, 2 | cvlsupr2 38726 |
. . . 4
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π) = (π β¨ π) β (π β π β§ π β π β§ π β€ (π β¨ π)))) |
19 | 10, 11, 12, 17, 15, 18 | syl131anc 1380 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((π β¨ π) = (π β¨ π) β (π β π β§ π β π β§ π β€ (π β¨ π)))) |
20 | 19 | anbi1d 629 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (((π β¨ π) = (π β¨ π) β§ π β€ π) β ((π β π β§ π β π β§ π β€ (π β¨ π)) β§ π β€ π))) |
21 | 7, 20 | mpbird 257 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((π β¨ π) = (π β¨ π) β§ π β€ π)) |