Step | Hyp | Ref
| Expression |
1 | | cdleme39.l |
. . 3
β’ β€ =
(leβπΎ) |
2 | | cdleme39.j |
. . 3
β’ β¨ =
(joinβπΎ) |
3 | | cdleme39.m |
. . 3
β’ β§ =
(meetβπΎ) |
4 | | cdleme39.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
5 | | cdleme39.h |
. . 3
β’ π» = (LHypβπΎ) |
6 | | cdleme39.u |
. . 3
β’ π = ((π β¨ π) β§ π) |
7 | | cdleme39.e |
. . 3
β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
8 | | cdleme39.y |
. . 3
β’ π = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) |
9 | | eqid 2726 |
. . 3
β’ ((π‘ β¨ πΈ) β§ π) = ((π‘ β¨ πΈ) β§ π) |
10 | | eqid 2726 |
. . 3
β’ ((π’ β¨ π) β§ π) = ((π’ β¨ π) β§ π) |
11 | | eqid 2726 |
. . 3
β’ ((π
β¨ ((π‘ β¨ πΈ) β§ π)) β§ (πΈ β¨ ((π‘ β¨ π
) β§ π))) = ((π
β¨ ((π‘ β¨ πΈ) β§ π)) β§ (πΈ β¨ ((π‘ β¨ π
) β§ π))) |
12 | | eqid 2726 |
. . 3
β’ ((π β¨ ((π’ β¨ π) β§ π)) β§ (π β¨ ((π’ β¨ π) β§ π))) = ((π β¨ ((π’ β¨ π) β§ π)) β§ (π β¨ ((π’ β¨ π) β§ π))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cdleme38n 39848 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β ((π
β¨ ((π‘ β¨ πΈ) β§ π)) β§ (πΈ β¨ ((π‘ β¨ π
) β§ π))) β ((π β¨ ((π’ β¨ π) β§ π)) β§ (π β¨ ((π’ β¨ π) β§ π)))) |
14 | | simp11 1200 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β (πΎ β HL β§ π β π»)) |
15 | | simp12l 1283 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π β π΄) |
16 | | simp13l 1285 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π β π΄) |
17 | | simp22l 1289 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π
β π΄) |
18 | | simp22r 1290 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β Β¬ π
β€ π) |
19 | | simp311 1317 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π
β€ (π β¨ π)) |
20 | | simp32l 1295 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β (π‘ β π΄ β§ Β¬ π‘ β€ π)) |
21 | | cdleme39.g |
. . . 4
β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π
β¨ π‘) β§ π))) |
22 | 1, 2, 3, 4, 5, 6, 7, 21, 9 | cdleme39a 39849 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π
β€ (π β¨ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π))) β πΊ = ((π
β¨ ((π‘ β¨ πΈ) β§ π)) β§ (πΈ β¨ ((π‘ β¨ π
) β§ π)))) |
23 | 14, 15, 16, 17, 18, 19, 20, 22 | syl322anc 1395 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β πΊ = ((π
β¨ ((π‘ β¨ πΈ) β§ π)) β§ (πΈ β¨ ((π‘ β¨ π
) β§ π)))) |
24 | | simp23l 1291 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π β π΄) |
25 | | simp23r 1292 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β Β¬ π β€ π) |
26 | | simp312 1318 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π β€ (π β¨ π)) |
27 | | simp33l 1297 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β (π’ β π΄ β§ Β¬ π’ β€ π)) |
28 | | cdleme39.z |
. . . 4
β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) |
29 | 1, 2, 3, 4, 5, 6, 8, 28, 10 | cdleme39a 39849 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ (π’ β π΄ β§ Β¬ π’ β€ π))) β π = ((π β¨ ((π’ β¨ π) β§ π)) β§ (π β¨ ((π’ β¨ π) β§ π)))) |
30 | 14, 15, 16, 24, 25, 26, 27, 29 | syl322anc 1395 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π = ((π β¨ ((π’ β¨ π) β§ π)) β§ (π β¨ ((π’ β¨ π) β§ π)))) |
31 | 13, 23, 30 | 3netr4d 3012 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β πΊ β π) |