Step | Hyp | Ref
| Expression |
1 | | simp3r 1203 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π < π) |
2 | | breq1 5109 |
. . 3
β’ (π = π β (π < π β π < π)) |
3 | 1, 2 | syl5ibrcom 247 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β (π = π β π < π)) |
4 | | simp1 1137 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β πΎ β HL) |
5 | | simp21 1207 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π β π΄) |
6 | | simp22 1208 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π β π΄) |
7 | | atlelt.s |
. . . . 5
β’ < =
(ltβπΎ) |
8 | | eqid 2733 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
9 | | atlelt.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
10 | 7, 8, 9 | atlt 37946 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π < (π(joinβπΎ)π) β π β π)) |
11 | 4, 5, 6, 10 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β (π < (π(joinβπΎ)π) β π β π)) |
12 | | simp3l 1202 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π β€ π) |
13 | | simp23 1209 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π β π΅) |
14 | 4, 6, 13 | 3jca 1129 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β (πΎ β HL β§ π β π΄ β§ π β π΅)) |
15 | | atlelt.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
16 | 15, 7 | pltle 18227 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΅) β (π < π β π β€ π)) |
17 | 14, 1, 16 | sylc 65 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π β€ π) |
18 | | hllat 37871 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
19 | 18 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β πΎ β Lat) |
20 | | atlelt.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
21 | 20, 9 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
22 | 5, 21 | syl 17 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π β π΅) |
23 | 20, 9 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
24 | 6, 23 | syl 17 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π β π΅) |
25 | 20, 15, 8 | latjle12 18344 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β (π(joinβπΎ)π) β€ π)) |
26 | 19, 22, 24, 13, 25 | syl13anc 1373 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β ((π β€ π β§ π β€ π) β (π(joinβπΎ)π) β€ π)) |
27 | 12, 17, 26 | mpbi2and 711 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β (π(joinβπΎ)π) β€ π) |
28 | | hlpos 37874 |
. . . . . 6
β’ (πΎ β HL β πΎ β Poset) |
29 | 28 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β πΎ β Poset) |
30 | 20, 8 | latjcl 18333 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π(joinβπΎ)π) β π΅) |
31 | 19, 22, 24, 30 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β (π(joinβπΎ)π) β π΅) |
32 | 20, 15, 7 | pltletr 18237 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ (π(joinβπΎ)π) β π΅ β§ π β π΅)) β ((π < (π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β π < π)) |
33 | 29, 22, 31, 13, 32 | syl13anc 1373 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β ((π < (π(joinβπΎ)π) β§ (π(joinβπΎ)π) β€ π) β π < π)) |
34 | 27, 33 | mpan2d 693 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β (π < (π(joinβπΎ)π) β π < π)) |
35 | 11, 34 | sylbird 260 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β (π β π β π < π)) |
36 | 3, 35 | pm2.61dne 3028 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π < π) |