Step | Hyp | Ref
| Expression |
1 | | cvllat 37834 |
. . . . . . . . 9
β’ (πΎ β CvLat β πΎ β Lat) |
2 | 1 | adantr 482 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β πΎ β Lat) |
3 | | simpr3 1197 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β π΅) |
4 | | simpr2 1196 |
. . . . . . . . 9
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β π΄) |
5 | | cvlexch.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΎ) |
6 | | cvlexch.a |
. . . . . . . . . 10
β’ π΄ = (AtomsβπΎ) |
7 | 5, 6 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β π΅) |
8 | 4, 7 | syl 17 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β π΅) |
9 | | cvlexch.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
10 | | cvlexch.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
11 | 5, 9, 10 | latlej1 18342 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β€ (π β¨ π)) |
12 | 2, 3, 8, 11 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β€ (π β¨ π)) |
13 | 12 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β π β€ (π β¨ π)) |
14 | 13 | adantr 482 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β π β€ (π β¨ π)) |
15 | | simpr 486 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β π β€ (π β¨ π)) |
16 | | simpr1 1195 |
. . . . . . . . 9
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β π΄) |
17 | 5, 6 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β π΅) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β π΅) |
19 | 5, 10 | latjcl 18333 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
20 | 2, 3, 8, 19 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β (π β¨ π) β π΅) |
21 | 5, 9, 10 | latjle12 18344 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ (π β¨ π) β π΅)) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
22 | 2, 3, 18, 20, 21 | syl13anc 1373 |
. . . . . . 7
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
23 | 22 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
24 | 23 | adantr 482 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
25 | 14, 15, 24 | mpbi2and 711 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π)) |
26 | 5, 9, 10 | latlej1 18342 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β€ (π β¨ π)) |
27 | 2, 3, 18, 26 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β€ (π β¨ π)) |
28 | 27 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β π β€ (π β¨ π)) |
29 | 28 | adantr 482 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β π β€ (π β¨ π)) |
30 | 5, 9, 10, 6 | cvlexch1 37836 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
31 | 30 | imp 408 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β π β€ (π β¨ π)) |
32 | 5, 10 | latjcl 18333 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
33 | 2, 3, 18, 32 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β (π β¨ π) β π΅) |
34 | 5, 9, 10 | latjle12 18344 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ (π β¨ π) β π΅)) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
35 | 2, 3, 8, 33, 34 | syl13anc 1373 |
. . . . . . 7
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
36 | 35 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
37 | 36 | adantr 482 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π))) |
38 | 29, 31, 37 | mpbi2and 711 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ π)) |
39 | 5, 9 | latasymb 18336 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ (π β¨ π) β π΅) β (((π β¨ π) β€ (π β¨ π) β§ (π β¨ π) β€ (π β¨ π)) β (π β¨ π) = (π β¨ π))) |
40 | 2, 33, 20, 39 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β (((π β¨ π) β€ (π β¨ π) β§ (π β¨ π) β€ (π β¨ π)) β (π β¨ π) = (π β¨ π))) |
41 | 40 | 3adant3 1133 |
. . . . 5
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (((π β¨ π) β€ (π β¨ π) β§ (π β¨ π) β€ (π β¨ π)) β (π β¨ π) = (π β¨ π))) |
42 | 41 | adantr 482 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β (((π β¨ π) β€ (π β¨ π) β§ (π β¨ π) β€ (π β¨ π)) β (π β¨ π) = (π β¨ π))) |
43 | 25, 38, 42 | mpbi2and 711 |
. . 3
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β (π β¨ π) = (π β¨ π)) |
44 | 43 | ex 414 |
. 2
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) |
45 | 5, 9, 10 | latlej2 18343 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β€ (π β¨ π)) |
46 | 2, 3, 18, 45 | syl3anc 1372 |
. . . 4
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β π β€ (π β¨ π)) |
47 | | breq2 5110 |
. . . 4
β’ ((π β¨ π) = (π β¨ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
48 | 46, 47 | syl5ibcom 244 |
. . 3
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅)) β ((π β¨ π) = (π β¨ π) β π β€ (π β¨ π))) |
49 | 48 | 3adant3 1133 |
. 2
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β ((π β¨ π) = (π β¨ π) β π β€ (π β¨ π))) |
50 | 44, 49 | impbid 211 |
1
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) |