Step | Hyp | Ref
| Expression |
1 | | simp3r 1203 |
. . . 4
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β Β¬ π
β€ π) |
2 | | simp12 1205 |
. . . 4
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β π
β€ (π β¨ π)) |
3 | 1, 2 | jca 513 |
. . 3
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (Β¬ π
β€ π β§ π
β€ (π β¨ π))) |
4 | | simp3l 1202 |
. . . . . 6
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β π
β π΄) |
5 | | simp13 1206 |
. . . . . . 7
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
6 | | ralnex 3076 |
. . . . . . 7
β’
(βπ β
π΄ Β¬ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
7 | 5, 6 | sylibr 233 |
. . . . . 6
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β βπ β π΄ Β¬ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
8 | | breq1 5113 |
. . . . . . . . . 10
β’ (π = π
β (π β€ π β π
β€ π)) |
9 | 8 | notbid 318 |
. . . . . . . . 9
β’ (π = π
β (Β¬ π β€ π β Β¬ π
β€ π)) |
10 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π
β (π β¨ π) = (π β¨ π
)) |
11 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π
β (π β¨ π) = (π β¨ π
)) |
12 | 10, 11 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π = π
β ((π β¨ π) = (π β¨ π) β (π β¨ π
) = (π β¨ π
))) |
13 | 9, 12 | anbi12d 632 |
. . . . . . . 8
β’ (π = π
β ((Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β (Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
)))) |
14 | 13 | notbid 318 |
. . . . . . 7
β’ (π = π
β (Β¬ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β Β¬ (Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
)))) |
15 | 14 | rspcva 3582 |
. . . . . 6
β’ ((π
β π΄ β§ βπ β π΄ Β¬ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β Β¬ (Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
))) |
16 | 4, 7, 15 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β Β¬ (Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
))) |
17 | | simp11 1204 |
. . . . . . . 8
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β πΎ β HL) |
18 | | hlcvl 37850 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β CvLat) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β πΎ β CvLat) |
20 | | simp21 1207 |
. . . . . . 7
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β π β π΄) |
21 | | simp22 1208 |
. . . . . . 7
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β π β π΄) |
22 | | simp23 1209 |
. . . . . . 7
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β π β π) |
23 | | cdleme0nex.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
24 | | cdleme0nex.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
25 | | cdleme0nex.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
26 | 23, 24, 25 | cvlsupr2 37834 |
. . . . . . 7
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β ((π β¨ π
) = (π β¨ π
) β (π
β π β§ π
β π β§ π
β€ (π β¨ π)))) |
27 | 19, 20, 21, 4, 22, 26 | syl131anc 1384 |
. . . . . 6
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β ((π β¨ π
) = (π β¨ π
) β (π
β π β§ π
β π β§ π
β€ (π β¨ π)))) |
28 | 27 | anbi2d 630 |
. . . . 5
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β ((Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
)) β (Β¬ π
β€ π β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))))) |
29 | 16, 28 | mtbid 324 |
. . . 4
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β Β¬ (Β¬ π
β€ π β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π)))) |
30 | | ianor 981 |
. . . . 5
β’ (Β¬
((π
β π β§ π
β π) β§ (Β¬ π
β€ π β§ π
β€ (π β¨ π))) β (Β¬ (π
β π β§ π
β π) β¨ Β¬ (Β¬ π
β€ π β§ π
β€ (π β¨ π)))) |
31 | | df-3an 1090 |
. . . . . . . 8
β’ ((π
β π β§ π
β π β§ π
β€ (π β¨ π)) β ((π
β π β§ π
β π) β§ π
β€ (π β¨ π))) |
32 | 31 | anbi2i 624 |
. . . . . . 7
β’ ((Β¬
π
β€ π β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (Β¬ π
β€ π β§ ((π
β π β§ π
β π) β§ π
β€ (π β¨ π)))) |
33 | | an12 644 |
. . . . . . 7
β’ ((Β¬
π
β€ π β§ ((π
β π β§ π
β π) β§ π
β€ (π β¨ π))) β ((π
β π β§ π
β π) β§ (Β¬ π
β€ π β§ π
β€ (π β¨ π)))) |
34 | 32, 33 | bitri 275 |
. . . . . 6
β’ ((Β¬
π
β€ π β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β ((π
β π β§ π
β π) β§ (Β¬ π
β€ π β§ π
β€ (π β¨ π)))) |
35 | 34 | notbii 320 |
. . . . 5
β’ (Β¬
(Β¬ π
β€ π β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β Β¬ ((π
β π β§ π
β π) β§ (Β¬ π
β€ π β§ π
β€ (π β¨ π)))) |
36 | | pm4.62 855 |
. . . . 5
β’ (((π
β π β§ π
β π) β Β¬ (Β¬ π
β€ π β§ π
β€ (π β¨ π))) β (Β¬ (π
β π β§ π
β π) β¨ Β¬ (Β¬ π
β€ π β§ π
β€ (π β¨ π)))) |
37 | 30, 35, 36 | 3bitr4ri 304 |
. . . 4
β’ (((π
β π β§ π
β π) β Β¬ (Β¬ π
β€ π β§ π
β€ (π β¨ π))) β Β¬ (Β¬ π
β€ π β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π)))) |
38 | 29, 37 | sylibr 233 |
. . 3
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β ((π
β π β§ π
β π) β Β¬ (Β¬ π
β€ π β§ π
β€ (π β¨ π)))) |
39 | 3, 38 | mt2d 136 |
. 2
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β Β¬ (π
β π β§ π
β π)) |
40 | | neanior 3038 |
. . 3
β’ ((π
β π β§ π
β π) β Β¬ (π
= π β¨ π
= π)) |
41 | 40 | con2bii 358 |
. 2
β’ ((π
= π β¨ π
= π) β Β¬ (π
β π β§ π
β π)) |
42 | 39, 41 | sylibr 233 |
1
β’ (((πΎ β HL β§ π
β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β (π
= π β¨ π
= π)) |