Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β π β π) |
2 | | simpl1 1192 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β πΎ β HL) |
3 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
4 | | lplnexat.p |
. . . . . 6
β’ π = (LPlanesβπΎ) |
5 | 3, 4 | lplnbase 38043 |
. . . . 5
β’ (π β π β π β (BaseβπΎ)) |
6 | 1, 5 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β π β (BaseβπΎ)) |
7 | | lplnexat.l |
. . . . 5
β’ β€ =
(leβπΎ) |
8 | | lplnexat.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
9 | | lplnexat.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
10 | | lplnexat.n |
. . . . 5
β’ π = (LLinesβπΎ) |
11 | 3, 7, 8, 9, 10, 4 | islpln3 38042 |
. . . 4
β’ ((πΎ β HL β§ π β (BaseβπΎ)) β (π β π β βπ§ β π βπ β π΄ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) |
12 | 2, 6, 11 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β (π β π β βπ§ β π βπ β π΄ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) |
13 | 1, 12 | mpbid 231 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β βπ§ β π βπ β π΄ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) |
14 | | simpll1 1213 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β πΎ β HL) |
15 | | simpr2l 1233 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π§ β π) |
16 | | simpll3 1215 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β π΄) |
17 | | simpr1 1195 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β€ π§) |
18 | 7, 8, 9, 10 | llnexatN 38030 |
. . . . . . 7
β’ (((πΎ β HL β§ π§ β π β§ π β π΄) β§ π β€ π§) β βπ β π΄ (π β π β§ π§ = (π β¨ π ))) |
19 | 14, 15, 16, 17, 18 | syl31anc 1374 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β βπ β π΄ (π β π β§ π§ = (π β¨ π ))) |
20 | | simp1l1 1267 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β πΎ β HL) |
21 | | simp22r 1294 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β π΄) |
22 | | simp3l 1202 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β π΄) |
23 | | simp1l3 1269 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β π΄) |
24 | | simp23l 1295 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β Β¬ π β€ π§) |
25 | | simp3rr 1248 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π§ = (π β¨ π )) |
26 | 25 | breq2d 5118 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β (π β€ π§ β π β€ (π β¨ π ))) |
27 | 24, 26 | mtbid 324 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β Β¬ π β€ (π β¨ π )) |
28 | 7, 8, 9 | atnlej2 37889 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π )) β π β π ) |
29 | 20, 21, 23, 22, 27, 28 | syl131anc 1384 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β π ) |
30 | 8, 9, 10 | llni2 38021 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β¨ π ) β π) |
31 | 20, 21, 22, 29, 30 | syl31anc 1374 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β (π β¨ π ) β π) |
32 | | simp3rl 1247 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β π ) |
33 | 7, 8, 9 | hlatcon2 37961 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π ))) β Β¬ π β€ (π β¨ π )) |
34 | 20, 23, 22, 21, 32, 27, 33 | syl132anc 1389 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β Β¬ π β€ (π β¨ π )) |
35 | | simp23r 1296 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π = (π§ β¨ π)) |
36 | 25 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β (π§ β¨ π) = ((π β¨ π ) β¨ π)) |
37 | 20 | hllatd 37872 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β πΎ β Lat) |
38 | 3, 9 | atbase 37797 |
. . . . . . . . . . . . 13
β’ (π β π΄ β π β (BaseβπΎ)) |
39 | 23, 38 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β (BaseβπΎ)) |
40 | 3, 9 | atbase 37797 |
. . . . . . . . . . . . 13
β’ (π β π΄ β π β (BaseβπΎ)) |
41 | 22, 40 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β (BaseβπΎ)) |
42 | 3, 9 | atbase 37797 |
. . . . . . . . . . . . 13
β’ (π β π΄ β π β (BaseβπΎ)) |
43 | 21, 42 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π β (BaseβπΎ)) |
44 | 3, 8 | latj31 18381 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β¨ π ) β¨ π) = ((π β¨ π ) β¨ π)) |
45 | 37, 39, 41, 43, 44 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β ((π β¨ π ) β¨ π) = ((π β¨ π ) β¨ π)) |
46 | 35, 36, 45 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β π = ((π β¨ π ) β¨ π)) |
47 | | breq2 5110 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β¨ π ) β (π β€ π¦ β π β€ (π β¨ π ))) |
48 | 47 | notbid 318 |
. . . . . . . . . . . 12
β’ (π¦ = (π β¨ π ) β (Β¬ π β€ π¦ β Β¬ π β€ (π β¨ π ))) |
49 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π¦ = (π β¨ π ) β (π¦ β¨ π) = ((π β¨ π ) β¨ π)) |
50 | 49 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π¦ = (π β¨ π ) β (π = (π¦ β¨ π) β π = ((π β¨ π ) β¨ π))) |
51 | 48, 50 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π¦ = (π β¨ π ) β ((Β¬ π β€ π¦ β§ π = (π¦ β¨ π)) β (Β¬ π β€ (π β¨ π ) β§ π = ((π β¨ π ) β¨ π)))) |
52 | 51 | rspcev 3580 |
. . . . . . . . . 10
β’ (((π β¨ π ) β π β§ (Β¬ π β€ (π β¨ π ) β§ π = ((π β¨ π ) β¨ π))) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) |
53 | 31, 34, 46, 52 | syl12anc 836 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β§ (π β π΄ β§ (π β π β§ π§ = (π β¨ π )))) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) |
54 | 53 | 3expia 1122 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β ((π β π΄ β§ (π β π β§ π§ = (π β¨ π ))) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) |
55 | 54 | expd 417 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β (π β π΄ β ((π β π β§ π§ = (π β¨ π )) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
56 | 55 | rexlimdv 3147 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β (βπ β π΄ (π β π β§ π§ = (π β¨ π )) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) |
57 | 19, 56 | mpd 15 |
. . . . 5
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) |
58 | 57 | 3exp2 1355 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β (π β€ π§ β ((π§ β π β§ π β π΄) β ((Β¬ π β€ π§ β§ π = (π§ β¨ π)) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))))) |
59 | | simpr2l 1233 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π§ β π) |
60 | | simpr1 1195 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β Β¬ π β€ π§) |
61 | | simpll1 1213 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β πΎ β HL) |
62 | 61 | hllatd 37872 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β πΎ β Lat) |
63 | 3, 10 | llnbase 38018 |
. . . . . . . . . . . 12
β’ (π§ β π β π§ β (BaseβπΎ)) |
64 | 59, 63 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π§ β (BaseβπΎ)) |
65 | | simpr2r 1234 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β π΄) |
66 | 65, 42 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β (BaseβπΎ)) |
67 | 3, 7, 8 | latlej1 18342 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π§ β (BaseβπΎ) β§ π β (BaseβπΎ)) β π§ β€ (π§ β¨ π)) |
68 | 62, 64, 66, 67 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π§ β€ (π§ β¨ π)) |
69 | | simpr3r 1236 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π = (π§ β¨ π)) |
70 | 68, 69 | breqtrrd 5134 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π§ β€ π) |
71 | | simplr 768 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β€ π) |
72 | | simpll3 1215 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β π΄) |
73 | 72, 38 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β (BaseβπΎ)) |
74 | | simpll2 1214 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β π) |
75 | 74, 5 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π β (BaseβπΎ)) |
76 | 3, 7, 8 | latjle12 18344 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π§ β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π§ β€ π β§ π β€ π) β (π§ β¨ π) β€ π)) |
77 | 62, 64, 73, 75, 76 | syl13anc 1373 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β ((π§ β€ π β§ π β€ π) β (π§ β¨ π) β€ π)) |
78 | 70, 71, 77 | mpbi2and 711 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β (π§ β¨ π) β€ π) |
79 | 3, 8 | latjcl 18333 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π§ β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π§ β¨ π) β (BaseβπΎ)) |
80 | 62, 64, 73, 79 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β (π§ β¨ π) β (BaseβπΎ)) |
81 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ ( β
βπΎ) = ( β
βπΎ) |
82 | 3, 7, 8, 81, 9 | cvr1 37919 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π§ β (BaseβπΎ) β§ π β π΄) β (Β¬ π β€ π§ β π§( β βπΎ)(π§ β¨ π))) |
83 | 61, 64, 72, 82 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β (Β¬ π β€ π§ β π§( β βπΎ)(π§ β¨ π))) |
84 | 60, 83 | mpbid 231 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π§( β βπΎ)(π§ β¨ π)) |
85 | 3, 81, 10, 4 | lplni 38041 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π§ β¨ π) β (BaseβπΎ) β§ π§ β π) β§ π§( β βπΎ)(π§ β¨ π)) β (π§ β¨ π) β π) |
86 | 61, 80, 59, 84, 85 | syl31anc 1374 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β (π§ β¨ π) β π) |
87 | 7, 4 | lplncmp 38071 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π§ β¨ π) β π β§ π β π) β ((π§ β¨ π) β€ π β (π§ β¨ π) = π)) |
88 | 61, 86, 74, 87 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β ((π§ β¨ π) β€ π β (π§ β¨ π) = π)) |
89 | 78, 88 | mpbid 231 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β (π§ β¨ π) = π) |
90 | 89 | eqcomd 2739 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β π = (π§ β¨ π)) |
91 | | breq2 5110 |
. . . . . . . . 9
β’ (π¦ = π§ β (π β€ π¦ β π β€ π§)) |
92 | 91 | notbid 318 |
. . . . . . . 8
β’ (π¦ = π§ β (Β¬ π β€ π¦ β Β¬ π β€ π§)) |
93 | | oveq1 7365 |
. . . . . . . . 9
β’ (π¦ = π§ β (π¦ β¨ π) = (π§ β¨ π)) |
94 | 93 | eqeq2d 2744 |
. . . . . . . 8
β’ (π¦ = π§ β (π = (π¦ β¨ π) β π = (π§ β¨ π))) |
95 | 92, 94 | anbi12d 632 |
. . . . . . 7
β’ (π¦ = π§ β ((Β¬ π β€ π¦ β§ π = (π¦ β¨ π)) β (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) |
96 | 95 | rspcev 3580 |
. . . . . 6
β’ ((π§ β π β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π))) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) |
97 | 59, 60, 90, 96 | syl12anc 836 |
. . . . 5
β’ ((((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β§ (Β¬ π β€ π§ β§ (π§ β π β§ π β π΄) β§ (Β¬ π β€ π§ β§ π = (π§ β¨ π)))) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) |
98 | 97 | 3exp2 1355 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β (Β¬ π β€ π§ β ((π§ β π β§ π β π΄) β ((Β¬ π β€ π§ β§ π = (π§ β¨ π)) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))))) |
99 | 58, 98 | pm2.61d 179 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β ((π§ β π β§ π β π΄) β ((Β¬ π β€ π§ β§ π = (π§ β¨ π)) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))))) |
100 | 99 | rexlimdvv 3201 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β (βπ§ β π βπ β π΄ (Β¬ π β€ π§ β§ π = (π§ β¨ π)) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) |
101 | 13, 100 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) |