Step | Hyp | Ref
| Expression |
1 | | lpcls.1 |
. . . . 5
β’ π = βͺ
π½ |
2 | 1 | lpcls 22738 |
. . . 4
β’ ((π½ β Fre β§ π β π) β ((limPtβπ½)β((clsβπ½)βπ)) = ((limPtβπ½)βπ)) |
3 | 2 | sseq2d 3980 |
. . 3
β’ ((π½ β Fre β§ π β π) β (((clsβπ½)βπ) β ((limPtβπ½)β((clsβπ½)βπ)) β ((clsβπ½)βπ) β ((limPtβπ½)βπ))) |
4 | | t1top 22704 |
. . . . . 6
β’ (π½ β Fre β π½ β Top) |
5 | 1 | clslp 22522 |
. . . . . 6
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) = (π βͺ ((limPtβπ½)βπ))) |
6 | 4, 5 | sylan 581 |
. . . . 5
β’ ((π½ β Fre β§ π β π) β ((clsβπ½)βπ) = (π βͺ ((limPtβπ½)βπ))) |
7 | 6 | sseq1d 3979 |
. . . 4
β’ ((π½ β Fre β§ π β π) β (((clsβπ½)βπ) β ((limPtβπ½)βπ) β (π βͺ ((limPtβπ½)βπ)) β ((limPtβπ½)βπ))) |
8 | | ssequn1 4144 |
. . . . 5
β’ (π β ((limPtβπ½)βπ) β (π βͺ ((limPtβπ½)βπ)) = ((limPtβπ½)βπ)) |
9 | | ssun2 4137 |
. . . . . 6
β’
((limPtβπ½)βπ) β (π βͺ ((limPtβπ½)βπ)) |
10 | | eqss 3963 |
. . . . . 6
β’ ((π βͺ ((limPtβπ½)βπ)) = ((limPtβπ½)βπ) β ((π βͺ ((limPtβπ½)βπ)) β ((limPtβπ½)βπ) β§ ((limPtβπ½)βπ) β (π βͺ ((limPtβπ½)βπ)))) |
11 | 9, 10 | mpbiran2 709 |
. . . . 5
β’ ((π βͺ ((limPtβπ½)βπ)) = ((limPtβπ½)βπ) β (π βͺ ((limPtβπ½)βπ)) β ((limPtβπ½)βπ)) |
12 | 8, 11 | bitri 275 |
. . . 4
β’ (π β ((limPtβπ½)βπ) β (π βͺ ((limPtβπ½)βπ)) β ((limPtβπ½)βπ)) |
13 | 7, 12 | bitr4di 289 |
. . 3
β’ ((π½ β Fre β§ π β π) β (((clsβπ½)βπ) β ((limPtβπ½)βπ) β π β ((limPtβπ½)βπ))) |
14 | 3, 13 | bitr2d 280 |
. 2
β’ ((π½ β Fre β§ π β π) β (π β ((limPtβπ½)βπ) β ((clsβπ½)βπ) β ((limPtβπ½)β((clsβπ½)βπ)))) |
15 | | eqid 2733 |
. . . 4
β’ (π½ βΎt π) = (π½ βΎt π) |
16 | 1, 15 | restperf 22558 |
. . 3
β’ ((π½ β Top β§ π β π) β ((π½ βΎt π) β Perf β π β ((limPtβπ½)βπ))) |
17 | 4, 16 | sylan 581 |
. 2
β’ ((π½ β Fre β§ π β π) β ((π½ βΎt π) β Perf β π β ((limPtβπ½)βπ))) |
18 | 1 | clsss3 22433 |
. . . 4
β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) β π) |
19 | | eqid 2733 |
. . . . 5
β’ (π½ βΎt
((clsβπ½)βπ)) = (π½ βΎt ((clsβπ½)βπ)) |
20 | 1, 19 | restperf 22558 |
. . . 4
β’ ((π½ β Top β§
((clsβπ½)βπ) β π) β ((π½ βΎt ((clsβπ½)βπ)) β Perf β ((clsβπ½)βπ) β ((limPtβπ½)β((clsβπ½)βπ)))) |
21 | 18, 20 | syldan 592 |
. . 3
β’ ((π½ β Top β§ π β π) β ((π½ βΎt ((clsβπ½)βπ)) β Perf β ((clsβπ½)βπ) β ((limPtβπ½)β((clsβπ½)βπ)))) |
22 | 4, 21 | sylan 581 |
. 2
β’ ((π½ β Fre β§ π β π) β ((π½ βΎt ((clsβπ½)βπ)) β Perf β ((clsβπ½)βπ) β ((limPtβπ½)β((clsβπ½)βπ)))) |
23 | 14, 17, 22 | 3bitr4d 311 |
1
β’ ((π½ β Fre β§ π β π) β ((π½ βΎt π) β Perf β (π½ βΎt ((clsβπ½)βπ)) β Perf)) |