Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β πΎ β HL) |
2 | 1 | hllatd 37855 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β πΎ β Lat) |
3 | | simpl2 1193 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β π β π΄) |
4 | | simpl3 1194 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β π β π΄) |
5 | | simprl 770 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β π β β
) |
6 | | inss2 4194 |
. . . . . 6
β’ (( β₯
βπ) β© π) β π |
7 | 6 | sseli 3945 |
. . . . 5
β’ (π β (( β₯ βπ) β© π) β π β π) |
8 | | pexmidlem.m |
. . . . 5
β’ π = (π + {π}) |
9 | 7, 8 | eleqtrdi 2848 |
. . . 4
β’ (π β (( β₯ βπ) β© π) β π β (π + {π})) |
10 | 9 | ad2antll 728 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β π β (π + {π})) |
11 | | pexmidlem.l |
. . . 4
β’ β€ =
(leβπΎ) |
12 | | pexmidlem.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
13 | | pexmidlem.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
14 | | pexmidlem.p |
. . . 4
β’ + =
(+πβπΎ) |
15 | 11, 12, 13, 14 | elpaddatiN 38297 |
. . 3
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (π + {π}))) β βπ β π π β€ (π β¨ π)) |
16 | 2, 3, 4, 5, 10, 15 | syl32anc 1379 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β βπ β π π β€ (π β¨ π)) |
17 | | simp1 1137 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π)) β§ (π β π β§ π β€ (π β¨ π))) β (πΎ β HL β§ π β π΄ β§ π β π΄)) |
18 | | simp3l 1202 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π)) β§ (π β π β§ π β€ (π β¨ π))) β π β π) |
19 | | inss1 4193 |
. . . . . . 7
β’ (( β₯
βπ) β© π) β ( β₯ βπ) |
20 | | simp2r 1201 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π)) β§ (π β π β§ π β€ (π β¨ π))) β π β (( β₯ βπ) β© π)) |
21 | 19, 20 | sselid 3947 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π)) β§ (π β π β§ π β€ (π β¨ π))) β π β ( β₯ βπ)) |
22 | | simp3r 1203 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π)) β§ (π β π β§ π β€ (π β¨ π))) β π β€ (π β¨ π)) |
23 | | pexmidlem.o |
. . . . . . 7
β’ β₯ =
(β₯πβπΎ) |
24 | 11, 12, 13, 14, 23, 8 | pexmidlem3N 38464 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β ( β₯ βπ)) β§ π β€ (π β¨ π)) β π β (π + ( β₯ βπ))) |
25 | 17, 18, 21, 22, 24 | syl121anc 1376 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π)) β§ (π β π β§ π β€ (π β¨ π))) β π β (π + ( β₯ βπ))) |
26 | 25 | 3expia 1122 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β ((π β π β§ π β€ (π β¨ π)) β π β (π + ( β₯ βπ)))) |
27 | 26 | expd 417 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β (π β π β (π β€ (π β¨ π) β π β (π + ( β₯ βπ))))) |
28 | 27 | rexlimdv 3151 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β (βπ β π π β€ (π β¨ π) β π β (π + ( β₯ βπ)))) |
29 | 16, 28 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ π β (( β₯ βπ) β© π))) β π β (π + ( β₯ βπ))) |