Step | Hyp | Ref
| Expression |
1 | | pexmidlem.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
2 | | pexmidlem.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
3 | | pexmidlem.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
4 | | pexmidlem.p |
. . . . . . . 8
β’ + =
(+πβπΎ) |
5 | | pexmidlem.o |
. . . . . . . 8
β’ β₯ =
(β₯πβπΎ) |
6 | | pexmidlem.m |
. . . . . . . 8
β’ π = (π + {π}) |
7 | 1, 2, 3, 4, 5, 6 | pexmidlem5N 38483 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (( β₯
βπ) β© π) = β
) |
8 | 7 | 3adantr1 1170 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (( β₯
βπ) β© π) = β
) |
9 | 8 | fveq2d 6847 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β ( β₯ β(( β₯
βπ) β© π)) = ( β₯
ββ
)) |
10 | | simpl1 1192 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β πΎ β HL) |
11 | 3, 5 | pol0N 38418 |
. . . . . 6
β’ (πΎ β HL β ( β₯
ββ
) = π΄) |
12 | 10, 11 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β ( β₯ ββ
) =
π΄) |
13 | 9, 12 | eqtrd 2773 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β ( β₯ β(( β₯
βπ) β© π)) = π΄) |
14 | 13 | ineq1d 4172 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (( β₯
β(( β₯ βπ) β© π)) β© π) = (π΄ β© π)) |
15 | | simpl2 1193 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π β π΄) |
16 | | simpl3 1194 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π β π΄) |
17 | 16 | snssd 4770 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β {π} β π΄) |
18 | 3, 4 | paddssat 38323 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ {π} β π΄) β (π + {π}) β π΄) |
19 | 10, 15, 17, 18 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (π + {π}) β π΄) |
20 | 6, 19 | eqsstrid 3993 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π β π΄) |
21 | 10, 15, 20 | 3jca 1129 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (πΎ β HL β§ π β π΄ β§ π β π΄)) |
22 | 3, 4 | sspadd1 38324 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ {π} β π΄) β π β (π + {π})) |
23 | 10, 15, 17, 22 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π β (π + {π})) |
24 | 23, 6 | sseqtrrdi 3996 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π β π) |
25 | | simpr1 1195 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β ( β₯ β( β₯
βπ)) = π) |
26 | | eqid 2733 |
. . . . . . . . . . 11
β’
(PSubClβπΎ) =
(PSubClβπΎ) |
27 | 3, 5, 26 | ispsubclN 38446 |
. . . . . . . . . 10
β’ (πΎ β HL β (π β (PSubClβπΎ) β (π β π΄ β§ ( β₯ β( β₯
βπ)) = π))) |
28 | 10, 27 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (π β (PSubClβπΎ) β (π β π΄ β§ ( β₯ β( β₯
βπ)) = π))) |
29 | 15, 25, 28 | mpbir2and 712 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π β (PSubClβπΎ)) |
30 | 3, 4, 26 | paddatclN 38458 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β (PSubClβπΎ) β§ π β π΄) β (π + {π}) β (PSubClβπΎ)) |
31 | 10, 29, 16, 30 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (π + {π}) β (PSubClβπΎ)) |
32 | 6, 31 | eqeltrid 2838 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π β (PSubClβπΎ)) |
33 | 5, 26 | psubcli2N 38448 |
. . . . . 6
β’ ((πΎ β HL β§ π β (PSubClβπΎ)) β ( β₯ β( β₯
βπ)) = π) |
34 | 10, 32, 33 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β ( β₯ β( β₯
βπ)) = π) |
35 | 24, 34 | jca 513 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (π β π β§ ( β₯ β( β₯
βπ)) = π)) |
36 | 3, 5 | poml4N 38462 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π β π β§ ( β₯ β( β₯
βπ)) = π) β (( β₯ β(( β₯
βπ) β© π)) β© π) = ( β₯ β( β₯
βπ)))) |
37 | 21, 35, 36 | sylc 65 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (( β₯
β(( β₯ βπ) β© π)) β© π) = ( β₯ β( β₯
βπ))) |
38 | | sseqin2 4176 |
. . . 4
β’ (π β π΄ β (π΄ β© π) = π) |
39 | 20, 38 | sylib 217 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β (π΄ β© π) = π) |
40 | 14, 37, 39 | 3eqtr3rd 2782 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π = ( β₯ β( β₯
βπ))) |
41 | 40, 25 | eqtrd 2773 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯
βπ)) = π β§ π β β
β§ Β¬ π β (π + ( β₯ βπ)))) β π = π) |