Step | Hyp | Ref
| Expression |
1 | | cvrat.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | cvrat.s |
. . . 4
β’ < =
(ltβπΎ) |
3 | | cvrat.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
4 | | cvrat.z |
. . . 4
β’ 0 =
(0.βπΎ) |
5 | | cvrat.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
6 | 1, 2, 3, 4, 5 | cvratlem 37930 |
. . 3
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β (Β¬ π(leβπΎ)π β π β π΄)) |
7 | | hllat 37871 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β Lat) |
8 | 7 | adantr 482 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β Lat) |
9 | | simpr2 1196 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
10 | 1, 5 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β π΅) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
12 | | simpr3 1197 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
13 | 1, 5 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β π΅) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
15 | 1, 3 | latjcom 18341 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
16 | 8, 11, 14, 15 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
17 | 16 | breq2d 5118 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π < (π β¨ π) β π < (π β¨ π))) |
18 | 17 | anbi2d 630 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β (π β 0 β§ π < (π β¨ π)))) |
19 | | simpl 484 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β HL) |
20 | | simpr1 1195 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
21 | 1, 2, 3, 4, 5 | cvratlem 37930 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β (Β¬ π(leβπΎ)π β π β π΄)) |
22 | 21 | ex 414 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β (Β¬ π(leβπΎ)π β π β π΄))) |
23 | 19, 20, 12, 9, 22 | syl13anc 1373 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β (Β¬ π(leβπΎ)π β π β π΄))) |
24 | 18, 23 | sylbid 239 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β (Β¬ π(leβπΎ)π β π β π΄))) |
25 | 24 | imp 408 |
. . 3
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β (Β¬ π(leβπΎ)π β π β π΄)) |
26 | | hlpos 37874 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β Poset) |
27 | 26 | adantr 482 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β Poset) |
28 | 1, 3 | latjcl 18333 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
29 | 8, 11, 14, 28 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β π΅) |
30 | | eqid 2733 |
. . . . . . . . . 10
β’
(leβπΎ) =
(leβπΎ) |
31 | 1, 30, 2 | pltnle 18232 |
. . . . . . . . 9
β’ (((πΎ β Poset β§ π β π΅ β§ (π β¨ π) β π΅) β§ π < (π β¨ π)) β Β¬ (π β¨ π)(leβπΎ)π) |
32 | 31 | ex 414 |
. . . . . . . 8
β’ ((πΎ β Poset β§ π β π΅ β§ (π β¨ π) β π΅) β (π < (π β¨ π) β Β¬ (π β¨ π)(leβπΎ)π)) |
33 | 27, 20, 29, 32 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π < (π β¨ π) β Β¬ (π β¨ π)(leβπΎ)π)) |
34 | 1, 30, 3 | latjle12 18344 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β (π β¨ π)(leβπΎ)π)) |
35 | 8, 11, 14, 20, 34 | syl13anc 1373 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β (π β¨ π)(leβπΎ)π)) |
36 | 35 | biimpd 228 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β (π β¨ π)(leβπΎ)π)) |
37 | 33, 36 | nsyld 156 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π < (π β¨ π) β Β¬ (π(leβπΎ)π β§ π(leβπΎ)π))) |
38 | | ianor 981 |
. . . . . 6
β’ (Β¬
(π(leβπΎ)π β§ π(leβπΎ)π) β (Β¬ π(leβπΎ)π β¨ Β¬ π(leβπΎ)π)) |
39 | 37, 38 | syl6ib 251 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π < (π β¨ π) β (Β¬ π(leβπΎ)π β¨ Β¬ π(leβπΎ)π))) |
40 | 39 | imp 408 |
. . . 4
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π < (π β¨ π)) β (Β¬ π(leβπΎ)π β¨ Β¬ π(leβπΎ)π)) |
41 | 40 | adantrl 715 |
. . 3
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β (Β¬ π(leβπΎ)π β¨ Β¬ π(leβπΎ)π)) |
42 | 6, 25, 41 | mpjaod 859 |
. 2
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β π β π΄) |
43 | 42 | ex 414 |
1
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β π β π΄)) |