Step | Hyp | Ref
| Expression |
1 | | restcls.2 |
. . . 4
β’ πΎ = (π½ βΎt π) |
2 | | perftop 22660 |
. . . . . . 7
β’ (π½ β Perf β π½ β Top) |
3 | 2 | adantr 482 |
. . . . . 6
β’ ((π½ β Perf β§ π β π½) β π½ β Top) |
4 | | restcls.1 |
. . . . . . 7
β’ π = βͺ
π½ |
5 | 4 | toptopon 22419 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnβπ)) |
6 | 3, 5 | sylib 217 |
. . . . 5
β’ ((π½ β Perf β§ π β π½) β π½ β (TopOnβπ)) |
7 | | elssuni 4942 |
. . . . . . 7
β’ (π β π½ β π β βͺ π½) |
8 | 7 | adantl 483 |
. . . . . 6
β’ ((π½ β Perf β§ π β π½) β π β βͺ π½) |
9 | 8, 4 | sseqtrrdi 4034 |
. . . . 5
β’ ((π½ β Perf β§ π β π½) β π β π) |
10 | | resttopon 22665 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π) β (π½ βΎt π) β (TopOnβπ)) |
11 | 6, 9, 10 | syl2anc 585 |
. . . 4
β’ ((π½ β Perf β§ π β π½) β (π½ βΎt π) β (TopOnβπ)) |
12 | 1, 11 | eqeltrid 2838 |
. . 3
β’ ((π½ β Perf β§ π β π½) β πΎ β (TopOnβπ)) |
13 | | topontop 22415 |
. . 3
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
14 | 12, 13 | syl 17 |
. 2
β’ ((π½ β Perf β§ π β π½) β πΎ β Top) |
15 | 9 | sselda 3983 |
. . . . . 6
β’ (((π½ β Perf β§ π β π½) β§ π₯ β π) β π₯ β π) |
16 | 4 | perfi 22659 |
. . . . . . 7
β’ ((π½ β Perf β§ π₯ β π) β Β¬ {π₯} β π½) |
17 | 16 | adantlr 714 |
. . . . . 6
β’ (((π½ β Perf β§ π β π½) β§ π₯ β π) β Β¬ {π₯} β π½) |
18 | 15, 17 | syldan 592 |
. . . . 5
β’ (((π½ β Perf β§ π β π½) β§ π₯ β π) β Β¬ {π₯} β π½) |
19 | 1 | eleq2i 2826 |
. . . . . 6
β’ ({π₯} β πΎ β {π₯} β (π½ βΎt π)) |
20 | | restopn2 22681 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π½) β ({π₯} β (π½ βΎt π) β ({π₯} β π½ β§ {π₯} β π))) |
21 | 2, 20 | sylan 581 |
. . . . . . . 8
β’ ((π½ β Perf β§ π β π½) β ({π₯} β (π½ βΎt π) β ({π₯} β π½ β§ {π₯} β π))) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ (((π½ β Perf β§ π β π½) β§ π₯ β π) β ({π₯} β (π½ βΎt π) β ({π₯} β π½ β§ {π₯} β π))) |
23 | | simpl 484 |
. . . . . . 7
β’ (({π₯} β π½ β§ {π₯} β π) β {π₯} β π½) |
24 | 22, 23 | syl6bi 253 |
. . . . . 6
β’ (((π½ β Perf β§ π β π½) β§ π₯ β π) β ({π₯} β (π½ βΎt π) β {π₯} β π½)) |
25 | 19, 24 | biimtrid 241 |
. . . . 5
β’ (((π½ β Perf β§ π β π½) β§ π₯ β π) β ({π₯} β πΎ β {π₯} β π½)) |
26 | 18, 25 | mtod 197 |
. . . 4
β’ (((π½ β Perf β§ π β π½) β§ π₯ β π) β Β¬ {π₯} β πΎ) |
27 | 26 | ralrimiva 3147 |
. . 3
β’ ((π½ β Perf β§ π β π½) β βπ₯ β π Β¬ {π₯} β πΎ) |
28 | | toponuni 22416 |
. . . . 5
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
29 | 12, 28 | syl 17 |
. . . 4
β’ ((π½ β Perf β§ π β π½) β π = βͺ πΎ) |
30 | 29 | raleqdv 3326 |
. . 3
β’ ((π½ β Perf β§ π β π½) β (βπ₯ β π Β¬ {π₯} β πΎ β βπ₯ β βͺ πΎ Β¬ {π₯} β πΎ)) |
31 | 27, 30 | mpbid 231 |
. 2
β’ ((π½ β Perf β§ π β π½) β βπ₯ β βͺ πΎ Β¬ {π₯} β πΎ) |
32 | | eqid 2733 |
. . 3
β’ βͺ πΎ =
βͺ πΎ |
33 | 32 | isperf3 22657 |
. 2
β’ (πΎ β Perf β (πΎ β Top β§ βπ₯ β βͺ πΎ
Β¬ {π₯} β πΎ)) |
34 | 14, 31, 33 | sylanbrc 584 |
1
β’ ((π½ β Perf β§ π β π½) β πΎ β Perf) |