Step | Hyp | Ref
| Expression |
1 | | simp111 1303 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β (πΎ β HL β§ π β π»)) |
2 | | simp112 1304 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
3 | | simp113 1305 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
4 | | simp12 1205 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β (π
β π΄ β§ Β¬ π
β€ π)) |
5 | | simp2l 1200 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β π β π΄) |
6 | | simp3ll 1245 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β Β¬ π β€ π) |
7 | 5, 6 | jca 513 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
8 | | simp2r 1201 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β π‘ β π΄) |
9 | | simp3rl 1247 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β Β¬ π‘ β€ π) |
10 | 8, 9 | jca 513 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β (π‘ β π΄ β§ Β¬ π‘ β€ π)) |
11 | | simp13l 1289 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β π β π) |
12 | | simp3lr 1246 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β Β¬ π β€ (π β¨ π)) |
13 | | simp3rr 1248 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β Β¬ π‘ β€ (π β¨ π)) |
14 | | simp13r 1290 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β π
β€ (π β¨ π)) |
15 | 12, 13, 14 | 3jca 1129 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β (Β¬ π β€ (π β¨ π) β§ Β¬ π‘ β€ (π β¨ π) β§ π
β€ (π β¨ π))) |
16 | | cdleme24.l |
. . . . 5
β’ β€ =
(leβπΎ) |
17 | | cdleme24.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
18 | | cdleme24.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
19 | | cdleme24.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
20 | | cdleme24.h |
. . . . 5
β’ π» = (LHypβπΎ) |
21 | | cdleme24.u |
. . . . 5
β’ π = ((π β¨ π) β§ π) |
22 | | cdleme24.f |
. . . . 5
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
23 | | cdleme24.g |
. . . . 5
β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
24 | | eqid 2737 |
. . . . 5
β’ ((π
β¨ π ) β§ π) = ((π
β¨ π ) β§ π) |
25 | | eqid 2737 |
. . . . 5
β’ ((π
β¨ π‘) β§ π) = ((π
β¨ π‘) β§ π) |
26 | | cdleme24.n |
. . . . 5
β’ π = ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π ) β§ π))) |
27 | | cdleme24.o |
. . . . 5
β’ π = ((π β¨ π) β§ (πΊ β¨ ((π
β¨ π‘) β§ π))) |
28 | 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 | cdleme21k 38830 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β π β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π‘ β€ (π β¨ π) β§ π
β€ (π β¨ π)))) β π = π) |
29 | 1, 2, 3, 4, 7, 10,
11, 15, 28 | syl332anc 1402 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β§ (π β π΄ β§ π‘ β π΄) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) β π = π) |
30 | 29 | 3exp 1120 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β ((π β π΄ β§ π‘ β π΄) β (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π))) β π = π))) |
31 | 30 | ralrimivv 3196 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π))) β π = π)) |