Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (πΎ β HL β§ π β π»)) |
2 | | simp21l 1291 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
3 | | simp23 1209 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
4 | | simp22l 1293 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
5 | | simp22r 1294 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ π) |
6 | | cdleme11.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
7 | | cdleme11.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
8 | | cdleme11.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
9 | | cdleme11.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
10 | | cdleme11.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
11 | | cdleme11.c |
. . . . . 6
β’ πΆ = ((π β¨ π) β§ π) |
12 | 6, 7, 8, 9, 10, 11 | cdleme0c 38722 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π)) β πΆ β π) |
13 | 1, 2, 3, 4, 5, 12 | syl122anc 1380 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ β π) |
14 | 13 | necomd 2996 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β πΆ) |
15 | | simp1l 1198 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΎ β HL) |
16 | | simp21 1207 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
17 | | simp3r 1203 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) |
18 | 6, 7, 8, 9 | cdleme00a 38718 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β π β π) |
19 | 15, 2, 4, 3, 17, 18 | syl131anc 1384 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) |
20 | 19 | necomd 2996 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) |
21 | 6, 7, 8, 9, 10, 11 | cdleme9a 38760 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β πΆ β π΄) |
22 | 1, 16, 3, 20, 21 | syl112anc 1375 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ β π΄) |
23 | 7, 9 | lnnat 37936 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ πΆ β π΄) β (π β πΆ β Β¬ (π β¨ πΆ) β π΄)) |
24 | 15, 4, 22, 23 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β πΆ β Β¬ (π β¨ πΆ) β π΄)) |
25 | 14, 24 | mpbid 231 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ (π β¨ πΆ) β π΄) |
26 | 7, 9 | hlatjidm 37877 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
27 | 15, 4, 26 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) = π) |
28 | 27, 4 | eqeltrd 2834 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β π΄) |
29 | | oveq2 7366 |
. . . . . 6
β’ (πΉ = π β (π β¨ πΉ) = (π β¨ π)) |
30 | 29 | eleq1d 2819 |
. . . . 5
β’ (πΉ = π β ((π β¨ πΉ) β π΄ β (π β¨ π) β π΄)) |
31 | 28, 30 | syl5ibrcom 247 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (πΉ = π β (π β¨ πΉ) β π΄)) |
32 | | simp22 1208 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
33 | | simp3l 1202 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) |
34 | | cdleme11.u |
. . . . . . 7
β’ π = ((π β¨ π) β§ π) |
35 | | cdleme11.f |
. . . . . . 7
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) |
36 | 6, 7, 8, 9, 10, 34, 11, 34, 35 | cdleme11g 38774 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ π β π) β (π β¨ πΉ) = (π β¨ πΆ)) |
37 | 1, 2, 32, 3, 33, 36 | syl131anc 1384 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ πΉ) = (π β¨ πΆ)) |
38 | 37 | eleq1d 2819 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β ((π β¨ πΉ) β π΄ β (π β¨ πΆ) β π΄)) |
39 | 31, 38 | sylibd 238 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (πΉ = π β (π β¨ πΆ) β π΄)) |
40 | 39 | necon3bd 2954 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (Β¬ (π β¨ πΆ) β π΄ β πΉ β π)) |
41 | 25, 40 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π) |