Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ)) β§ π β€ (π β¨ π)) β (πΎ β HL β§ π β π΄ β§ π β π΄)) |
2 | | simp2l 1200 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ)) β§ π β€ (π β¨ π)) β π β π) |
3 | | simp2r 1201 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ)) β§ π β€ (π β¨ π)) β π β ( β₯ βπ)) |
4 | | simpl1 1192 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β πΎ β HL) |
5 | | simpl2 1193 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β π΄) |
6 | | pexmidlem.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
7 | | pexmidlem.o |
. . . . . . 7
β’ β₯ =
(β₯πβπΎ) |
8 | 6, 7 | polssatN 38779 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
9 | 4, 5, 8 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β ( β₯ βπ) β π΄) |
10 | | simprr 772 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β ( β₯ βπ)) |
11 | 9, 10 | sseldd 3984 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β π΄) |
12 | | simpl3 1194 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β π΄) |
13 | | simprl 770 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β π) |
14 | 5, 13 | sseldd 3984 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β π΄) |
15 | | pexmidlem.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
16 | | pexmidlem.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
17 | | pexmidlem.p |
. . . . . 6
β’ + =
(+πβπΎ) |
18 | | pexmidlem.m |
. . . . . 6
β’ π = (π + {π}) |
19 | 15, 16, 6, 17, 7, 18 | pexmidlem1N 38841 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β π) |
20 | 19 | 3adantl3 1169 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β π β π) |
21 | 15, 16, 6 | hlatexch1 38266 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
22 | 4, 11, 12, 14, 20, 21 | syl131anc 1384 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ))) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
23 | 22 | 3impia 1118 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ)) β§ π β€ (π β¨ π)) β π β€ (π β¨ π)) |
24 | 15, 16, 6, 17, 7, 18 | pexmidlem2N 38842 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ) β§ π β€ (π β¨ π))) β π β (π + ( β₯ βπ))) |
25 | 1, 2, 3, 23, 24 | syl13anc 1373 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ)) β§ π β€ (π β¨ π)) β π β (π + ( β₯ βπ))) |