Step | Hyp | Ref
| Expression |
1 | | ssid 4000 |
. . . . 5
β’ π β π |
2 | | lpfval.1 |
. . . . . 6
β’ π = βͺ
π½ |
3 | 2 | lpss 23033 |
. . . . 5
β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) β π) |
4 | 1, 3 | mpan2 690 |
. . . 4
β’ (π½ β Top β
((limPtβπ½)βπ) β π) |
5 | 4 | sseld 3977 |
. . 3
β’ (π½ β Top β (π β ((limPtβπ½)βπ) β π β π)) |
6 | 5 | pm4.71rd 562 |
. 2
β’ (π½ β Top β (π β ((limPtβπ½)βπ) β (π β π β§ π β ((limPtβπ½)βπ)))) |
7 | | simpl 482 |
. . . . 5
β’ ((π½ β Top β§ π β π) β π½ β Top) |
8 | 2 | islp 23031 |
. . . . 5
β’ ((π½ β Top β§ π β π) β (π β ((limPtβπ½)βπ) β π β ((clsβπ½)β(π β {π})))) |
9 | 7, 1, 8 | sylancl 585 |
. . . 4
β’ ((π½ β Top β§ π β π) β (π β ((limPtβπ½)βπ) β π β ((clsβπ½)β(π β {π})))) |
10 | | snssi 4807 |
. . . . . 6
β’ (π β π β {π} β π) |
11 | 2 | clsdif 22944 |
. . . . . 6
β’ ((π½ β Top β§ {π} β π) β ((clsβπ½)β(π β {π})) = (π β ((intβπ½)β{π}))) |
12 | 10, 11 | sylan2 592 |
. . . . 5
β’ ((π½ β Top β§ π β π) β ((clsβπ½)β(π β {π})) = (π β ((intβπ½)β{π}))) |
13 | 12 | eleq2d 2814 |
. . . 4
β’ ((π½ β Top β§ π β π) β (π β ((clsβπ½)β(π β {π})) β π β (π β ((intβπ½)β{π})))) |
14 | | eldif 3954 |
. . . . . . 7
β’ (π β (π β ((intβπ½)β{π})) β (π β π β§ Β¬ π β ((intβπ½)β{π}))) |
15 | 14 | baib 535 |
. . . . . 6
β’ (π β π β (π β (π β ((intβπ½)β{π})) β Β¬ π β ((intβπ½)β{π}))) |
16 | 15 | adantl 481 |
. . . . 5
β’ ((π½ β Top β§ π β π) β (π β (π β ((intβπ½)β{π})) β Β¬ π β ((intβπ½)β{π}))) |
17 | | snssi 4807 |
. . . . . . . . . 10
β’ (π β ((intβπ½)β{π}) β {π} β ((intβπ½)β{π})) |
18 | 17 | adantl 481 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β {π} β ((intβπ½)β{π})) |
19 | 2 | ntrss2 22948 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ {π} β π) β ((intβπ½)β{π}) β {π}) |
20 | 10, 19 | sylan2 592 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β π) β ((intβπ½)β{π}) β {π}) |
21 | 20 | adantr 480 |
. . . . . . . . 9
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β ((intβπ½)β{π}) β {π}) |
22 | 18, 21 | eqssd 3995 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β {π} = ((intβπ½)β{π})) |
23 | 2 | ntropn 22940 |
. . . . . . . . . 10
β’ ((π½ β Top β§ {π} β π) β ((intβπ½)β{π}) β π½) |
24 | 10, 23 | sylan2 592 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β ((intβπ½)β{π}) β π½) |
25 | 24 | adantr 480 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β ((intβπ½)β{π}) β π½) |
26 | 22, 25 | eqeltrd 2828 |
. . . . . . 7
β’ (((π½ β Top β§ π β π) β§ π β ((intβπ½)β{π})) β {π} β π½) |
27 | | snidg 4658 |
. . . . . . . . 9
β’ (π β π β π β {π}) |
28 | 27 | ad2antlr 726 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ {π} β π½) β π β {π}) |
29 | | isopn3i 22973 |
. . . . . . . . 9
β’ ((π½ β Top β§ {π} β π½) β ((intβπ½)β{π}) = {π}) |
30 | 29 | adantlr 714 |
. . . . . . . 8
β’ (((π½ β Top β§ π β π) β§ {π} β π½) β ((intβπ½)β{π}) = {π}) |
31 | 28, 30 | eleqtrrd 2831 |
. . . . . . 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 578 |
. 2
β’ (π½ β Top β ((π β π β§ π β ((limPtβπ½)βπ)) β (π β π β§ Β¬ {π} β π½))) |
37 | 6, 36 | bitrd 279 |
1
β’ (π½ β Top β (π β ((limPtβπ½)βπ) β (π β π β§ Β¬ {π} β π½))) |