Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (πΎ β HL β§ π β π»)) |
2 | | simp12 1205 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π β π΄ β§ Β¬ π β€ π)) |
3 | | simp31 1210 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π£ β (π
βπΉ)) |
4 | | simp13 1206 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π£ β π΄ β§ π£ β€ π)) |
5 | | simp2r 1201 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β πΉ β π) |
6 | | simp33 1212 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (πΉβπ) β π) |
7 | | cdlemg12.l |
. . . . 5
β’ β€ =
(leβπΎ) |
8 | | cdlemg12.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
9 | | cdlemg12.h |
. . . . 5
β’ π» = (LHypβπΎ) |
10 | | cdlemg12.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
11 | | cdlemg12b.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
12 | 7, 8, 9, 10, 11 | trlat 38661 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) β π)) β (π
βπΉ) β π΄) |
13 | 1, 2, 5, 6, 12 | syl112anc 1375 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π
βπΉ) β π΄) |
14 | 7, 9, 10, 11 | trlle 38676 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β€ π) |
15 | 1, 5, 14 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π
βπΉ) β€ π) |
16 | | cdlemg12.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
17 | 7, 16, 8, 9 | lhp2atnle 38525 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π£ β (π
βπΉ)) β§ (π£ β π΄ β§ π£ β€ π) β§ ((π
βπΉ) β π΄ β§ (π
βπΉ) β€ π)) β Β¬ (π
βπΉ) β€ (π β¨ π£)) |
18 | 1, 2, 3, 4, 13, 15, 17 | syl312anc 1392 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π
βπΉ) β€ (π β¨ π£)) |
19 | | simp11l 1285 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β πΎ β HL) |
20 | | simp12l 1287 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π β π΄) |
21 | | simp13l 1289 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π£ β π΄) |
22 | 7, 16, 8 | hlatlej1 37866 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π£ β π΄) β π β€ (π β¨ π£)) |
23 | 19, 20, 21, 22 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π β€ (π β¨ π£)) |
24 | | simp32 1211 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π§ β€ (π β¨ π£)) |
25 | 19 | hllatd 37855 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β πΎ β Lat) |
26 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
27 | 26, 8 | atbase 37780 |
. . . . . 6
β’ (π β π΄ β π β (BaseβπΎ)) |
28 | 20, 27 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π β (BaseβπΎ)) |
29 | | simp2l 1200 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π§ β π΄) |
30 | 26, 8 | atbase 37780 |
. . . . . 6
β’ (π§ β π΄ β π§ β (BaseβπΎ)) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β π§ β (BaseβπΎ)) |
32 | 26, 16, 8 | hlatjcl 37858 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π£ β π΄) β (π β¨ π£) β (BaseβπΎ)) |
33 | 19, 20, 21, 32 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π β¨ π£) β (BaseβπΎ)) |
34 | 26, 7, 16 | latjle12 18346 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π§ β (BaseβπΎ) β§ (π β¨ π£) β (BaseβπΎ))) β ((π β€ (π β¨ π£) β§ π§ β€ (π β¨ π£)) β (π β¨ π§) β€ (π β¨ π£))) |
35 | 25, 28, 31, 33, 34 | syl13anc 1373 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β ((π β€ (π β¨ π£) β§ π§ β€ (π β¨ π£)) β (π β¨ π§) β€ (π β¨ π£))) |
36 | 23, 24, 35 | mpbi2and 711 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π β¨ π§) β€ (π β¨ π£)) |
37 | 26, 8 | atbase 37780 |
. . . . 5
β’ ((π
βπΉ) β π΄ β (π
βπΉ) β (BaseβπΎ)) |
38 | 13, 37 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π
βπΉ) β (BaseβπΎ)) |
39 | 26, 16, 8 | hlatjcl 37858 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π§ β π΄) β (π β¨ π§) β (BaseβπΎ)) |
40 | 19, 20, 29, 39 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (π β¨ π§) β (BaseβπΎ)) |
41 | 26, 7 | lattr 18340 |
. . . 4
β’ ((πΎ β Lat β§ ((π
βπΉ) β (BaseβπΎ) β§ (π β¨ π§) β (BaseβπΎ) β§ (π β¨ π£) β (BaseβπΎ))) β (((π
βπΉ) β€ (π β¨ π§) β§ (π β¨ π§) β€ (π β¨ π£)) β (π
βπΉ) β€ (π β¨ π£))) |
42 | 25, 38, 40, 33, 41 | syl13anc 1373 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β (((π
βπΉ) β€ (π β¨ π§) β§ (π β¨ π§) β€ (π β¨ π£)) β (π
βπΉ) β€ (π β¨ π£))) |
43 | 36, 42 | mpan2d 693 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β ((π
βπΉ) β€ (π β¨ π§) β (π
βπΉ) β€ (π β¨ π£))) |
44 | 18, 43 | mtod 197 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π
βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π
βπΉ) β€ (π β¨ π§)) |