Step | Hyp | Ref
| Expression |
1 | | simp13 1206 |
. . . . . . 7
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β πΎ β CvLat) |
2 | | cvllat 37834 |
. . . . . . 7
β’ (πΎ β CvLat β πΎ β Lat) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β πΎ β Lat) |
4 | | simp2 1138 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β π β π΅) |
5 | | cvlcvr1.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
6 | | cvlcvr1.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
7 | 5, 6 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
8 | 7 | 3ad2ant3 1136 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β π β π΅) |
9 | | cvlcvr1.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
10 | | eqid 2733 |
. . . . . . 7
β’
(ltβπΎ) =
(ltβπΎ) |
11 | | cvlcvr1.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
12 | 5, 9, 10, 11 | latnle 18367 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β π(ltβπΎ)(π β¨ π))) |
13 | 3, 4, 8, 12 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β π(ltβπΎ)(π β¨ π))) |
14 | 13 | biimpd 228 |
. . . 4
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β π(ltβπΎ)(π β¨ π))) |
15 | | simpl13 1251 |
. . . . . . . . 9
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β πΎ β CvLat) |
16 | 15, 2 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β πΎ β Lat) |
17 | | simprll 778 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π§ β π΅) |
18 | | simpl2 1193 |
. . . . . . . . 9
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π β π΅) |
19 | | simpl3 1194 |
. . . . . . . . . 10
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π β π΄) |
20 | 19, 7 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π β π΅) |
21 | 5, 11 | latjcl 18333 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
22 | 16, 18, 20, 21 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β (π β¨ π) β π΅) |
23 | | simprrr 781 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π§ β€ (π β¨ π)) |
24 | | simprrl 780 |
. . . . . . . . . 10
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π(ltβπΎ)π§) |
25 | | simpl11 1249 |
. . . . . . . . . . 11
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β πΎ β OML) |
26 | | simpl12 1250 |
. . . . . . . . . . 11
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β πΎ β CLat) |
27 | | cvlatl 37833 |
. . . . . . . . . . . 12
β’ (πΎ β CvLat β πΎ β AtLat) |
28 | 15, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β πΎ β AtLat) |
29 | 5, 9, 10, 6 | atlrelat1 37829 |
. . . . . . . . . . 11
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π§ β π΅) β (π(ltβπΎ)π§ β βπ β π΄ (Β¬ π β€ π β§ π β€ π§))) |
30 | 25, 26, 28, 18, 17, 29 | syl311anc 1385 |
. . . . . . . . . 10
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β (π(ltβπΎ)π§ β βπ β π΄ (Β¬ π β€ π β§ π β€ π§))) |
31 | 24, 30 | mpd 15 |
. . . . . . . . 9
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β βπ β π΄ (Β¬ π β€ π β§ π β€ π§)) |
32 | 16 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β πΎ β Lat) |
33 | 5, 6 | atbase 37797 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π β π΅) |
34 | 33 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β π΅) |
35 | 17 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π§ β π΅) |
36 | 22 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β (π β¨ π) β π΅) |
37 | | simprrr 781 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β€ π§) |
38 | 23 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π§ β€ (π β¨ π)) |
39 | 5, 9, 32, 34, 35, 36, 37, 38 | lattrd 18340 |
. . . . . . . . . . . 12
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β€ (π β¨ π)) |
40 | 15 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β πΎ β CvLat) |
41 | | simprl 770 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β π΄) |
42 | | simpll3 1215 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β π΄) |
43 | | simpll2 1214 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β π΅) |
44 | | simprrl 780 |
. . . . . . . . . . . . 13
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β Β¬ π β€ π) |
45 | 5, 9, 11, 6 | cvlexch1 37836 |
. . . . . . . . . . . . 13
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
46 | 40, 41, 42, 43, 44, 45 | syl131anc 1384 |
. . . . . . . . . . . 12
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
47 | 39, 46 | mpd 15 |
. . . . . . . . . . 11
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β€ (π β¨ π)) |
48 | | simprlr 779 |
. . . . . . . . . . . . 13
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β Β¬ π β€ π) |
49 | 48 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β Β¬ π β€ π) |
50 | 5, 9, 11, 6 | cvlexchb1 37838 |
. . . . . . . . . . . 12
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) |
51 | 40, 42, 41, 43, 49, 50 | syl131anc 1384 |
. . . . . . . . . . 11
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) |
52 | 47, 51 | mpbid 231 |
. . . . . . . . . 10
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β (π β¨ π) = (π β¨ π)) |
53 | 9, 10 | pltle 18227 |
. . . . . . . . . . . . . 14
β’ ((πΎ β OML β§ π β π΅ β§ π§ β π΅) β (π(ltβπΎ)π§ β π β€ π§)) |
54 | 25, 18, 17, 53 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β (π(ltβπΎ)π§ β π β€ π§)) |
55 | 24, 54 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π β€ π§) |
56 | 55 | adantr 482 |
. . . . . . . . . . 11
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β π β€ π§) |
57 | 5, 9, 11 | latjle12 18344 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π§ β π΅)) β ((π β€ π§ β§ π β€ π§) β (π β¨ π) β€ π§)) |
58 | 32, 43, 34, 35, 57 | syl13anc 1373 |
. . . . . . . . . . 11
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β ((π β€ π§ β§ π β€ π§) β (π β¨ π) β€ π§)) |
59 | 56, 37, 58 | mpbi2and 711 |
. . . . . . . . . 10
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β (π β¨ π) β€ π§) |
60 | 52, 59 | eqbrtrd 5128 |
. . . . . . . . 9
β’
(((((πΎ β OML
β§ πΎ β CLat β§
πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β§ (π β π΄ β§ (Β¬ π β€ π β§ π β€ π§))) β (π β¨ π) β€ π§) |
61 | 31, 60 | rexlimddv 3155 |
. . . . . . . 8
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β (π β¨ π) β€ π§) |
62 | 5, 9, 16, 17, 22, 23, 61 | latasymd 18339 |
. . . . . . 7
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ((π§ β π΅ β§ Β¬ π β€ π) β§ (π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)))) β π§ = (π β¨ π)) |
63 | 62 | exp44 439 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (π§ β π΅ β (Β¬ π β€ π β ((π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)) β π§ = (π β¨ π))))) |
64 | 63 | imp 408 |
. . . . 5
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ π§ β π΅) β (Β¬ π β€ π β ((π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)) β π§ = (π β¨ π)))) |
65 | 64 | ralrimdva 3148 |
. . . 4
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β βπ§ β π΅ ((π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)) β π§ = (π β¨ π)))) |
66 | 14, 65 | jcad 514 |
. . 3
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β (π(ltβπΎ)(π β¨ π) β§ βπ§ β π΅ ((π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)) β π§ = (π β¨ π))))) |
67 | 3, 4, 8, 21 | syl3anc 1372 |
. . . 4
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (π β¨ π) β π΅) |
68 | | cvlcvr1.c |
. . . . 5
β’ πΆ = ( β βπΎ) |
69 | 5, 9, 10, 68 | cvrval2 37782 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (ππΆ(π β¨ π) β (π(ltβπΎ)(π β¨ π) β§ βπ§ β π΅ ((π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)) β π§ = (π β¨ π))))) |
70 | 3, 4, 67, 69 | syl3anc 1372 |
. . 3
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (ππΆ(π β¨ π) β (π(ltβπΎ)(π β¨ π) β§ βπ§ β π΅ ((π(ltβπΎ)π§ β§ π§ β€ (π β¨ π)) β π§ = (π β¨ π))))) |
71 | 66, 70 | sylibrd 259 |
. 2
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) |
72 | 3 | adantr 482 |
. . . . 5
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ππΆ(π β¨ π)) β πΎ β Lat) |
73 | | simpl2 1193 |
. . . . 5
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ππΆ(π β¨ π)) β π β π΅) |
74 | 67 | adantr 482 |
. . . . 5
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ππΆ(π β¨ π)) β (π β¨ π) β π΅) |
75 | | simpr 486 |
. . . . 5
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ππΆ(π β¨ π)) β ππΆ(π β¨ π)) |
76 | 5, 10, 68 | cvrlt 37778 |
. . . . 5
β’ (((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β§ ππΆ(π β¨ π)) β π(ltβπΎ)(π β¨ π)) |
77 | 72, 73, 74, 75, 76 | syl31anc 1374 |
. . . 4
β’ ((((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β§ ππΆ(π β¨ π)) β π(ltβπΎ)(π β¨ π)) |
78 | 77 | ex 414 |
. . 3
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (ππΆ(π β¨ π) β π(ltβπΎ)(π β¨ π))) |
79 | 78, 13 | sylibrd 259 |
. 2
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (ππΆ(π β¨ π) β Β¬ π β€ π)) |
80 | 71, 79 | impbid 211 |
1
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β CvLat) β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) |