Step | Hyp | Ref
| Expression |
1 | | simp11l 1283 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β πΎ β HL) |
2 | | simp11r 1284 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β π β π») |
3 | 1, 2 | jca 511 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (πΎ β HL β§ π β π»)) |
4 | | simp13 1204 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (π β π΄ β§ Β¬ π β€ π)) |
5 | | simp31 1208 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β π£ β (π
βπΉ)) |
6 | 5 | necomd 2995 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (π
βπΉ) β π£) |
7 | | simp12 1203 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (π β π΄ β§ Β¬ π β€ π)) |
8 | | simp2r 1199 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β πΉ β π) |
9 | | simp32 1209 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (πΉβπ) β π) |
10 | | cdlemg12.l |
. . . . 5
β’ β€ =
(leβπΎ) |
11 | | cdlemg12.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
12 | | cdlemg12.h |
. . . . 5
β’ π» = (LHypβπΎ) |
13 | | cdlemg12.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
14 | | cdlemg12b.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
15 | 10, 11, 12, 13, 14 | trlat 39344 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) β π)) β (π
βπΉ) β π΄) |
16 | 3, 7, 8, 9, 15 | syl112anc 1373 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (π
βπΉ) β π΄) |
17 | 10, 12, 13, 14 | trlle 39359 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β€ π) |
18 | 3, 8, 17 | syl2anc 583 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (π
βπΉ) β€ π) |
19 | | simp2l 1198 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β (π£ β π΄ β§ π£ β€ π)) |
20 | | cdlemg12.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
21 | 10, 20, 11, 12 | lhp2atnle 39208 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) β π£) β§ ((π
βπΉ) β π΄ β§ (π
βπΉ) β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β Β¬ π£ β€ (π β¨ (π
βπΉ))) |
22 | 3, 4, 6, 16, 18, 19, 21 | syl321anc 1391 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β Β¬ π£ β€ (π β¨ (π
βπΉ))) |
23 | | simp12l 1285 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β π β π΄) |
24 | | simp13l 1287 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β π β π΄) |
25 | | simp2ll 1239 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β π£ β π΄) |
26 | | cdlemg12.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
27 | | cdlemg31.n |
. . . . . . 7
β’ π = ((π β¨ π£) β§ (π β¨ (π
βπΉ))) |
28 | 10, 20, 26, 11, 12, 13, 14, 27 | cdlemg31a 39872 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ π£)) |
29 | 1, 2, 23, 24, 25, 8, 28 | syl222anc 1385 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β π β€ (π β¨ π£)) |
30 | 29 | adantr 480 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π) β π β€ (π β¨ π£)) |
31 | | simp111 1301 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β (πΎ β HL β§ π β π»)) |
32 | | simp112 1302 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β (π β π΄ β§ Β¬ π β€ π)) |
33 | | simp3 1137 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β π β π£) |
34 | 33 | necomd 2995 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β π£ β π) |
35 | | simp12l 1285 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β (π£ β π΄ β§ π£ β€ π)) |
36 | | simp133 1309 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β π β π΄) |
37 | | simp2 1136 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β π β€ π) |
38 | 10, 20, 11, 12 | lhp2atnle 39208 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π£ β π) β§ (π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π β€ π)) β Β¬ π β€ (π β¨ π£)) |
39 | 31, 32, 34, 35, 36, 37, 38 | syl312anc 1390 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π β§ π β π£) β Β¬ π β€ (π β¨ π£)) |
40 | 39 | 3expia 1120 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π) β (π β π£ β Β¬ π β€ (π β¨ π£))) |
41 | 40 | necon4ad 2958 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π) β (π β€ (π β¨ π£) β π = π£)) |
42 | 30, 41 | mpd 15 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π) β π = π£) |
43 | 10, 20, 26, 11, 12, 13, 14, 27 | cdlemg31b 39873 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ (π
βπΉ))) |
44 | 1, 2, 23, 24, 25, 8, 43 | syl222anc 1385 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β π β€ (π β¨ (π
βπΉ))) |
45 | 44 | adantr 480 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π) β π β€ (π β¨ (π
βπΉ))) |
46 | 42, 45 | eqbrtrrd 5172 |
. 2
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β§ π β€ π) β π£ β€ (π β¨ (π
βπΉ))) |
47 | 22, 46 | mtand 813 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β Β¬ π β€ π) |