Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | dalawlem.l |
. 2
β’ β€ =
(leβπΎ) |
3 | | simp11 1204 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β HL) |
4 | 3 | hllatd 37829 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β Lat) |
5 | | simp22 1208 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
6 | | simp32 1211 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
7 | | dalawlem.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
8 | | dalawlem.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
9 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
10 | 3, 5, 6, 9 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
11 | | simp21 1207 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
12 | 1, 8 | atbase 37754 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
14 | 1, 7 | latjcl 18329 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
15 | 4, 10, 13, 14 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
16 | | simp31 1210 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
17 | 1, 8 | atbase 37754 |
. . . 4
β’ (π β π΄ β π β (BaseβπΎ)) |
18 | 16, 17 | syl 17 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
19 | | dalawlem.m |
. . . 4
β’ β§ =
(meetβπΎ) |
20 | 1, 19 | latmcl 18330 |
. . 3
β’ ((πΎ β Lat β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((π β¨ π) β¨ π) β§ π) β (BaseβπΎ)) |
21 | 4, 15, 18, 20 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β (BaseβπΎ)) |
22 | | simp23 1209 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π
β π΄) |
23 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β (π β¨ π
) β (BaseβπΎ)) |
24 | 3, 5, 22, 23 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π
) β (BaseβπΎ)) |
25 | | simp33 1212 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
26 | 1, 8 | atbase 37754 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
27 | 25, 26 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
28 | 1, 19 | latmcl 18330 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ π
) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π
) β§ π) β (BaseβπΎ)) |
29 | 4, 24, 27, 28 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ π) β (BaseβπΎ)) |
30 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β¨ π) β (BaseβπΎ)) |
31 | 3, 22, 11, 30 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ π) β (BaseβπΎ)) |
32 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
33 | 3, 25, 16, 32 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
34 | 1, 19 | latmcl 18330 |
. . . 4
β’ ((πΎ β Lat β§ (π
β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
35 | 4, 31, 33, 34 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
36 | 1, 7 | latjcl 18329 |
. . 3
β’ ((πΎ β Lat β§ ((π β¨ π
) β§ π) β (BaseβπΎ) β§ ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
37 | 4, 29, 35, 36 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
38 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
39 | 3, 6, 25, 38 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
40 | 1, 19 | latmcl 18330 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ π
) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) |
41 | 4, 24, 39, 40 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) |
42 | 1, 7 | latjcl 18329 |
. . 3
β’ ((πΎ β Lat β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ) β§ ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) β (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
43 | 4, 41, 35, 42 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
44 | 1, 8 | atbase 37754 |
. . . . . . . . . 10
β’ (π β π΄ β π β (BaseβπΎ)) |
45 | 5, 44 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
46 | 1, 19 | latmcl 18330 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β§ π) β (BaseβπΎ)) |
47 | 4, 45, 27, 46 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β§ π) β (BaseβπΎ)) |
48 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
49 | 3, 11, 16, 48 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
50 | 1, 19 | latmcl 18330 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π) β§ π) β (BaseβπΎ)) |
51 | 4, 49, 45, 50 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ π) β (BaseβπΎ)) |
52 | 1, 7 | latjcl 18329 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β§ π) β (BaseβπΎ) β§ ((π β¨ π) β§ π) β (BaseβπΎ)) β ((π β§ π) β¨ ((π β¨ π) β§ π)) β (BaseβπΎ)) |
53 | 4, 47, 51, 52 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ ((π β¨ π) β§ π)) β (BaseβπΎ)) |
54 | 1, 7 | latjcl 18329 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((π β§ π) β¨ ((π β¨ π) β§ π)) β (BaseβπΎ)) β (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π))) β (BaseβπΎ)) |
55 | 4, 13, 53, 54 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π))) β (BaseβπΎ)) |
56 | 1, 8 | atbase 37754 |
. . . . . . . . 9
β’ (π
β π΄ β π
β (BaseβπΎ)) |
57 | 22, 56 | syl 17 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π
β (BaseβπΎ)) |
58 | 1, 7 | latjcl 18329 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π
β (BaseβπΎ) β§ ((π β¨ π
) β§ π) β (BaseβπΎ)) β (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ)) |
59 | 4, 57, 29, 58 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ)) |
60 | 1, 7 | latjcl 18329 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ)) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) β (BaseβπΎ)) |
61 | 4, 13, 59, 60 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) β (BaseβπΎ)) |
62 | 1, 7 | latjcl 18329 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β§ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β§ π) β¨ π) β (BaseβπΎ)) |
63 | 4, 47, 13, 62 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ π) β (BaseβπΎ)) |
64 | 1, 2, 7, 19 | latmlej22 18371 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ ((π β§ π) β¨ π) β (BaseβπΎ))) β (((π β¨ π) β¨ π) β§ π) β€ (((π β§ π) β¨ π) β¨ π)) |
65 | 4, 18, 15, 63, 64 | syl13anc 1373 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β§ π) β¨ π) β¨ π)) |
66 | 1, 7 | latjass 18373 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ ((π β§ π) β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β§ π) β¨ π) β¨ π) = ((π β§ π) β¨ (π β¨ π))) |
67 | 4, 47, 13, 18, 66 | syl13anc 1373 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β§ π) β¨ π) β¨ π) = ((π β§ π) β¨ (π β¨ π))) |
68 | 65, 67 | breqtrd 5132 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ ((π β§ π) β¨ (π β¨ π))) |
69 | 1, 19 | latmcl 18330 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
70 | 4, 10, 49, 69 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
71 | 1, 7 | latjcl 18329 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((π β¨ π) β§ (π β¨ π)) β¨ π) β (BaseβπΎ)) |
72 | 4, 70, 13, 71 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β§ (π β¨ π)) β¨ π) β (BaseβπΎ)) |
73 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
74 | 3, 11, 5, 73 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
75 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
76 | 3, 11, 16, 75 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
77 | 1, 2, 19 | latmlem2 18360 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ ((π β¨ π) β¨ π) β (BaseβπΎ))) β (π β€ (π β¨ π) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π) β¨ π) β§ (π β¨ π)))) |
78 | 4, 18, 49, 15, 77 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π) β¨ π) β§ (π β¨ π)))) |
79 | 76, 78 | mpd 15 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π) β¨ π) β§ (π β¨ π))) |
80 | 2, 7, 8 | hlatlej1 37840 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
81 | 3, 11, 16, 80 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
82 | 1, 2, 7, 19, 8 | atmod4i1 38332 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ π β€ (π β¨ π)) β (((π β¨ π) β§ (π β¨ π)) β¨ π) = (((π β¨ π) β¨ π) β§ (π β¨ π))) |
83 | 3, 11, 10, 49, 81, 82 | syl131anc 1384 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β§ (π β¨ π)) β¨ π) = (((π β¨ π) β¨ π) β§ (π β¨ π))) |
84 | 79, 83 | breqtrrd 5134 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π) β§ (π β¨ π)) β¨ π)) |
85 | 1, 19 | latmcom 18353 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) = ((π β¨ π) β§ (π β¨ π))) |
86 | 4, 10, 49, 85 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) = ((π β¨ π) β§ (π β¨ π))) |
87 | | simp12 1205 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
88 | 86, 87 | eqbrtrd 5128 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
89 | 2, 7, 8 | hlatlej1 37840 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
90 | 3, 11, 5, 89 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
91 | 1, 2, 7 | latjle12 18340 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ) β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ π β€ (π β¨ π)) β (((π β¨ π) β§ (π β¨ π)) β¨ π) β€ (π β¨ π))) |
92 | 4, 70, 13, 74, 91 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ π β€ (π β¨ π)) β (((π β¨ π) β§ (π β¨ π)) β¨ π) β€ (π β¨ π))) |
93 | 88, 90, 92 | mpbi2and 711 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β§ (π β¨ π)) β¨ π) β€ (π β¨ π)) |
94 | 1, 2, 4, 21, 72, 74, 84, 93 | lattrd 18336 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) |
95 | 1, 7 | latjcl 18329 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π β§ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β§ π) β¨ (π β¨ π)) β (BaseβπΎ)) |
96 | 4, 47, 49, 95 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ (π β¨ π)) β (BaseβπΎ)) |
97 | 1, 2, 19 | latlem12 18356 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ ((((π β¨ π) β¨ π) β§ π) β (BaseβπΎ) β§ ((π β§ π) β¨ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β (((((π β¨ π) β¨ π) β§ π) β€ ((π β§ π) β¨ (π β¨ π)) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β§ π) β¨ (π β¨ π)) β§ (π β¨ π)))) |
98 | 4, 21, 96, 74, 97 | syl13anc 1373 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((((π β¨ π) β¨ π) β§ π) β€ ((π β§ π) β¨ (π β¨ π)) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β§ π) β¨ (π β¨ π)) β§ (π β¨ π)))) |
99 | 68, 94, 98 | mpbi2and 711 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β§ π) β¨ (π β¨ π)) β§ (π β¨ π))) |
100 | 1, 2, 7, 19, 8 | atmod3i1 38330 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ π β€ (π β¨ π)) β (π β¨ ((π β¨ π) β§ π)) = ((π β¨ π) β§ (π β¨ π))) |
101 | 3, 11, 49, 45, 81, 100 | syl131anc 1384 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ π)) = ((π β¨ π) β§ (π β¨ π))) |
102 | 101 | oveq2d 7374 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ (π β¨ ((π β¨ π) β§ π))) = ((π β§ π) β¨ ((π β¨ π) β§ (π β¨ π)))) |
103 | 1, 7 | latj12 18374 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ ((π β§ π) β (BaseβπΎ) β§ π β (BaseβπΎ) β§ ((π β¨ π) β§ π) β (BaseβπΎ))) β ((π β§ π) β¨ (π β¨ ((π β¨ π) β§ π))) = (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π)))) |
104 | 4, 47, 13, 51, 103 | syl13anc 1373 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ (π β¨ ((π β¨ π) β§ π))) = (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π)))) |
105 | 1, 2, 7, 19 | latmlej12 18369 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β (π β§ π) β€ (π β¨ π)) |
106 | 4, 45, 27, 13, 105 | syl13anc 1373 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β§ π) β€ (π β¨ π)) |
107 | 1, 2, 7, 19, 8 | atmod1i1m 38324 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄) β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ (π β§ π) β€ (π β¨ π)) β ((π β§ π) β¨ ((π β¨ π) β§ (π β¨ π))) = (((π β§ π) β¨ (π β¨ π)) β§ (π β¨ π))) |
108 | 3, 25, 45, 49, 74, 106, 107 | syl231anc 1391 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ ((π β¨ π) β§ (π β¨ π))) = (((π β§ π) β¨ (π β¨ π)) β§ (π β¨ π))) |
109 | 102, 104,
108 | 3eqtr3rd 2786 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β§ π) β¨ (π β¨ π)) β§ (π β¨ π)) = (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π)))) |
110 | 99, 109 | breqtrd 5132 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π)))) |
111 | 2, 7, 8 | hlatlej1 37840 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β π β€ (π β¨ π
)) |
112 | 3, 5, 22, 111 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π
)) |
113 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β π β€ (π
β¨ π)) |
114 | 3, 22, 25, 113 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π
β¨ π)) |
115 | 1, 19 | latmcl 18330 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
116 | 4, 49, 10, 115 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
117 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β¨ π) β (BaseβπΎ)) |
118 | 3, 22, 25, 117 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ π) β (BaseβπΎ)) |
119 | 2, 7, 8 | hlatlej1 37840 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
120 | 3, 5, 6, 119 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
121 | 1, 2, 19 | latmlem2 18360 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β (π β€ (π β¨ π) β ((π β¨ π) β§ π) β€ ((π β¨ π) β§ (π β¨ π)))) |
122 | 4, 45, 10, 49, 121 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β ((π β¨ π) β§ π) β€ ((π β¨ π) β§ (π β¨ π)))) |
123 | 120, 122 | mpd 15 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ π) β€ ((π β¨ π) β§ (π β¨ π))) |
124 | | simp13 1206 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) |
125 | 1, 2, 4, 51, 116, 118, 123, 124 | lattrd 18336 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ π) β€ (π
β¨ π)) |
126 | 1, 2, 7 | latjle12 18340 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ ((π β¨ π) β§ π) β (BaseβπΎ) β§ (π
β¨ π) β (BaseβπΎ))) β ((π β€ (π
β¨ π) β§ ((π β¨ π) β§ π) β€ (π
β¨ π)) β (π β¨ ((π β¨ π) β§ π)) β€ (π
β¨ π))) |
127 | 4, 27, 51, 118, 126 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β€ (π
β¨ π) β§ ((π β¨ π) β§ π) β€ (π
β¨ π)) β (π β¨ ((π β¨ π) β§ π)) β€ (π
β¨ π))) |
128 | 114, 125,
127 | mpbi2and 711 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ π)) β€ (π
β¨ π)) |
129 | 1, 7 | latjcl 18329 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((π β¨ π) β§ π) β (BaseβπΎ)) β (π β¨ ((π β¨ π) β§ π)) β (BaseβπΎ)) |
130 | 4, 27, 51, 129 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ π)) β (BaseβπΎ)) |
131 | 1, 2, 19 | latmlem12 18361 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ)) β§ ((π β¨ ((π β¨ π) β§ π)) β (BaseβπΎ) β§ (π
β¨ π) β (BaseβπΎ))) β ((π β€ (π β¨ π
) β§ (π β¨ ((π β¨ π) β§ π)) β€ (π
β¨ π)) β (π β§ (π β¨ ((π β¨ π) β§ π))) β€ ((π β¨ π
) β§ (π
β¨ π)))) |
132 | 4, 45, 24, 130, 118, 131 | syl122anc 1380 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β€ (π β¨ π
) β§ (π β¨ ((π β¨ π) β§ π)) β€ (π
β¨ π)) β (π β§ (π β¨ ((π β¨ π) β§ π))) β€ ((π β¨ π
) β§ (π
β¨ π)))) |
133 | 112, 128,
132 | mp2and 698 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β§ (π β¨ ((π β¨ π) β§ π))) β€ ((π β¨ π
) β§ (π
β¨ π))) |
134 | 1, 2, 19 | latmle2 18355 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π) β§ π) β€ π) |
135 | 4, 49, 45, 134 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ π) β€ π) |
136 | 1, 2, 7, 19, 8 | atmod2i2 38328 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΄ β§ π β (BaseβπΎ) β§ ((π β¨ π) β§ π) β (BaseβπΎ)) β§ ((π β¨ π) β§ π) β€ π) β ((π β§ π) β¨ ((π β¨ π) β§ π)) = (π β§ (π β¨ ((π β¨ π) β§ π)))) |
137 | 3, 25, 45, 51, 135, 136 | syl131anc 1384 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ ((π β¨ π) β§ π)) = (π β§ (π β¨ ((π β¨ π) β§ π)))) |
138 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β π
β€ (π β¨ π
)) |
139 | 3, 5, 22, 138 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π
β€ (π β¨ π
)) |
140 | 1, 2, 7, 19, 8 | atmod3i2 38331 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΄ β§ π
β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ)) β§ π
β€ (π β¨ π
)) β (π
β¨ ((π β¨ π
) β§ π)) = ((π β¨ π
) β§ (π
β¨ π))) |
141 | 3, 25, 57, 24, 139, 140 | syl131anc 1384 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ ((π β¨ π
) β§ π)) = ((π β¨ π
) β§ (π
β¨ π))) |
142 | 133, 137,
141 | 3brtr4d 5138 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ π) β¨ ((π β¨ π) β§ π)) β€ (π
β¨ ((π β¨ π
) β§ π))) |
143 | 1, 2, 7 | latjlej2 18344 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (((π β§ π) β¨ ((π β¨ π) β§ π)) β (BaseβπΎ) β§ (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β§ π) β¨ ((π β¨ π) β§ π)) β€ (π
β¨ ((π β¨ π
) β§ π)) β (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π))) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π))))) |
144 | 4, 53, 59, 13, 143 | syl13anc 1373 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β§ π) β¨ ((π β¨ π) β§ π)) β€ (π
β¨ ((π β¨ π
) β§ π)) β (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π))) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π))))) |
145 | 142, 144 | mpd 15 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β§ π) β¨ ((π β¨ π) β§ π))) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π)))) |
146 | 1, 2, 4, 21, 55, 61, 110, 145 | lattrd 18336 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π)))) |
147 | 1, 7 | latj13 18376 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π
β (BaseβπΎ) β§ ((π β¨ π
) β§ π) β (BaseβπΎ))) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) = (((π β¨ π
) β§ π) β¨ (π
β¨ π))) |
148 | 4, 13, 57, 29, 147 | syl13anc 1373 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) = (((π β¨ π
) β§ π) β¨ (π
β¨ π))) |
149 | 146, 148 | breqtrd 5132 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ (π
β¨ π))) |
150 | 1, 2, 7, 19 | latmlej22 18371 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) |
151 | 4, 18, 15, 27, 150 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) |
152 | 1, 7 | latjcl 18329 |
. . . . . 6
β’ ((πΎ β Lat β§ ((π β¨ π
) β§ π) β (BaseβπΎ) β§ (π
β¨ π) β (BaseβπΎ)) β (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β (BaseβπΎ)) |
153 | 4, 29, 31, 152 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β (BaseβπΎ)) |
154 | 1, 2, 19 | latlem12 18356 |
. . . . 5
β’ ((πΎ β Lat β§ ((((π β¨ π) β¨ π) β§ π) β (BaseβπΎ) β§ (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β (((((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) β (((π β¨ π) β¨ π) β§ π) β€ ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π)))) |
155 | 4, 21, 153, 33, 154 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) β (((π β¨ π) β¨ π) β§ π) β€ ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π)))) |
156 | 149, 151,
155 | mpbi2and 711 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π))) |
157 | 1, 2, 7, 19 | latmlej21 18370 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β¨ π
) β§ π) β€ (π β¨ π)) |
158 | 4, 27, 24, 18, 157 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ π) β€ (π β¨ π)) |
159 | 1, 2, 7, 19, 8 | atmod1i1m 38324 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ ((π β¨ π
) β (BaseβπΎ) β§ (π
β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ ((π β¨ π
) β§ π) β€ (π β¨ π)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) = ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π))) |
160 | 3, 25, 24, 31, 33, 158, 159 | syl231anc 1391 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) = ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π))) |
161 | 156, 160 | breqtrrd 5134 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π)))) |
162 | 2, 7, 8 | hlatlej2 37841 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
163 | 3, 6, 25, 162 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
164 | 1, 2, 19 | latmlem2 18360 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ))) β (π β€ (π β¨ π) β ((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)))) |
165 | 4, 27, 39, 24, 164 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β ((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)))) |
166 | 163, 165 | mpd 15 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π))) |
167 | 1, 2, 7 | latjlej1 18343 |
. . . 4
β’ ((πΎ β Lat β§ (((π β¨ π
) β§ π) β (BaseβπΎ) β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ) β§ ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ))) β (((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))))) |
168 | 4, 29, 41, 35, 167 | syl13anc 1373 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))))) |
169 | 166, 168 | mpd 15 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π)))) |
170 | 1, 2, 4, 21, 37, 43, 161, 169 | lattrd 18336 |
1
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π)))) |