| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ssid 4005 |
. . . . 5
β’ π β π |
| 2 | | lpfval.1 |
. . . . . 6
β’ π = βͺ
π½ |
| 3 | 2 | lpss 22646 |
. . . . 5
β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) β π) |
| 4 | 1, 3 | mpan2 690 |
. . . 4
β’ (π½ β Top β
((limPtβπ½)βπ) β π) |
| 5 | 4 | sseld 3982 |
. . 3
β’ (π½ β Top β (π β ((limPtβπ½)βπ) β π β π)) |
| 6 | 5 | pm4.71rd 564 |
. 2
β’ (π½ β Top β (π β ((limPtβπ½)βπ) β (π β π β§ π β ((limPtβπ½)βπ)))) |
| 7 | | simpl 484 |
. . . . 5
β’ ((π½ β Top β§ π β π) β π½ β Top) |
| 8 | 2 | islp 22644 |
. . . . 5
β’ ((π½ β Top β§ π β π) β (π β ((limPtβπ½)βπ) β π β ((clsβπ½)β(π β {π})))) |
| 9 | 7, 1, 8 | sylancl 587 |
. . . 4
β’ ((π½ β Top β§ π β π) β (π β ((limPtβπ½)βπ) β π β ((clsβπ½)β(π β {π})))) |
| 10 | | snssi 4812 |
. . . . . 6
β’ (π β π β {π} β π) |
| 11 | 2 | clsdif 22557 |
. . . . . 6
β’ ((π½ β Top β§ {π} β π) β ((clsβπ½)β(π β {π})) = (π β ((intβπ½)β{π}))) |
| 12 | 10, 11 | sylan2 594 |
. . . . 5
β’ ((π½ β Top β§ π β π) β ((clsβπ½)β(π β {π})) = (π β ((intβπ½)β{π}))) |
| 13 | 12 | eleq2d 2820 |
. . . 4
β’ ((π½ β Top β§ π β π) β (π β ((clsβπ½)β(π β {π})) β π β (π β ((intβπ½)β{π})))) |
| 14 | | eldif 3959 |
. . . . . . 7
β’ (π β (π β ((intβπ½)β{π})) β (π β π β§ Β¬ π β ((intβπ½)β{π}))) |
| 15 | 14 | baib 537 |
. . . . . 6
β’ (π β π β (π β (π β ((intβπ½)β{π})) β Β¬ π β ((intβπ½)β{π}))) |
| 16 | 15 | adantl 483 |
. . . . 5
β’ ((π½ β Top β§ π β π) β (π β (π β ((intβπ½)β{π})) β Β¬ π β ((intβπ½)β{π}))) |
| 17 | | snssi 4812 |
. . . . . . . . . 10
β’ (π β ((intβπ½)β{π}) β {π} β ((intβπ½)β{π})) |
| 18 | 17 | adantl 483 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β {π} β ((intβπ½)β{π})) |
| 19 | 2 | ntrss2 22561 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ {π} β π) β ((intβπ½)β{π}) β {π}) |
| 20 | 10, 19 | sylan2 594 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β π) β ((intβπ½)β{π}) β {π}) |
| 21 | 20 | adantr 482 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β ((intβπ½)β{π}) β {π}) |
| 22 | 18, 21 | eqssd 4000 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β {π} = ((intβπ½)β{π})) |
| 23 | 2 | ntropn 22553 |
. . . . . . . . . 10
β’ ((π½ β Top β§ {π} β π) β ((intβπ½)β{π}) β π½) |
| 24 | 10, 23 | sylan2 594 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β ((intβπ½)β{π}) β π½) |
| 25 | 24 | adantr 482 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β ((intβπ½)β{π}) β π½) |
| 26 | 22, 25 | eqeltrd 2834 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β {π} β π½) |
| 27 | | snidg 4663 |
. . . . . . . . 9
β’ (π β π β π β {π}) |
| 28 | 27 | ad2antlr 726 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ {π} β π½) β π β {π}) |
| 29 | | isopn3i 22586 |
. . . . . . . . 9
β’ ((π½ β Top β§ {π} β π½) β ((intβπ½)β{π}) = {π}) |
| 30 | 29 | adantlr 714 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ {π} β π½) β ((intβπ½)β{π}) = {π}) |
| 31 | 28, 30 | eleqtrrd 2837 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ {π} β π½) β π β ((intβπ½)β{π})) |
| 32 | 26, 31 | impbida 800 |
. . . . . 6
β’ ((π½ β Top β§ π β π) β (π β ((intβπ½)β{π}) β {π} β π½)) |
| 33 | 32 | notbid 318 |
. . . . 5
β’ ((π½ β Top β§ π β π) β (Β¬ π β ((intβπ½)β{π}) β Β¬ {π} β π½)) |
| 34 | 16, 33 | bitrd 279 |
. . . 4
β’ ((π½ β Top β§ π β π) β (π β (π β ((intβπ½)β{π})) β Β¬ {π} β π½)) |
| 35 | 9, 13, 34 | 3bitrd 305 |
. . 3
β’ ((π½ β Top β§ π β π) β (π β ((limPtβπ½)βπ) β Β¬ {π} β π½)) |
| 36 | 35 | pm5.32da 580 |
. 2
β’ (π½ β Top β ((π β π β§ π β ((limPtβπ½)βπ)) β (π β π β§ Β¬ {π} β π½))) |
| 37 | 6, 36 | bitrd 279 |
1
β’ (π½ β Top β (π β ((limPtβπ½)βπ) β (π β π β§ Β¬ {π} β π½))) |
