Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . 3
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
2 | 1 | eleq1d 2819 |
. 2
β’ (π₯ = π β ((πΉβπ₯) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ) β (πΉβπ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))) |
3 | | oveq2 7369 |
. . . 4
β’ (π = (((neiβπ½)β{π}) βΎt π΄) β ((π½ βΎt π΄) fLim π) = ((π½ βΎt π΄) fLim (((neiβπ½)β{π}) βΎt π΄))) |
4 | | oveq2 7369 |
. . . . . 6
β’ (π = (((neiβπ½)β{π}) βΎt π΄) β (πΎ fLimf π) = (πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))) |
5 | 4 | fveq1d 6848 |
. . . . 5
β’ (π = (((neiβπ½)β{π}) βΎt π΄) β ((πΎ fLimf π)βπΉ) = ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
6 | 5 | eleq2d 2820 |
. . . 4
β’ (π = (((neiβπ½)β{π}) βΎt π΄) β ((πΉβπ₯) β ((πΎ fLimf π)βπΉ) β (πΉβπ₯) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))) |
7 | 3, 6 | raleqbidv 3318 |
. . 3
β’ (π = (((neiβπ½)β{π}) βΎt π΄) β (βπ₯ β ((π½ βΎt π΄) fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ) β βπ₯ β ((π½ βΎt π΄) fLim (((neiβπ½)β{π}) βΎt π΄))(πΉβπ₯) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ))) |
8 | | flfcntr.1 |
. . . . 5
β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) |
9 | | flfcntr.j |
. . . . . . . 8
β’ (π β π½ β Top) |
10 | | flfcntr.c |
. . . . . . . . 9
β’ πΆ = βͺ
π½ |
11 | 10 | toptopon 22289 |
. . . . . . . 8
β’ (π½ β Top β π½ β (TopOnβπΆ)) |
12 | 9, 11 | sylib 217 |
. . . . . . 7
β’ (π β π½ β (TopOnβπΆ)) |
13 | | flfcntr.a |
. . . . . . 7
β’ (π β π΄ β πΆ) |
14 | | resttopon 22535 |
. . . . . . 7
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ) β (π½ βΎt π΄) β (TopOnβπ΄)) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . . 6
β’ (π β (π½ βΎt π΄) β (TopOnβπ΄)) |
16 | | cntop2 22615 |
. . . . . . . 8
β’ (πΉ β ((π½ βΎt π΄) Cn πΎ) β πΎ β Top) |
17 | 8, 16 | syl 17 |
. . . . . . 7
β’ (π β πΎ β Top) |
18 | | flfcntr.b |
. . . . . . . 8
β’ π΅ = βͺ
πΎ |
19 | 18 | toptopon 22289 |
. . . . . . 7
β’ (πΎ β Top β πΎ β (TopOnβπ΅)) |
20 | 17, 19 | sylib 217 |
. . . . . 6
β’ (π β πΎ β (TopOnβπ΅)) |
21 | | cnflf 23376 |
. . . . . 6
β’ (((π½ βΎt π΄) β (TopOnβπ΄) β§ πΎ β (TopOnβπ΅)) β (πΉ β ((π½ βΎt π΄) Cn πΎ) β (πΉ:π΄βΆπ΅ β§ βπ β (Filβπ΄)βπ₯ β ((π½ βΎt π΄) fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
22 | 15, 20, 21 | syl2anc 585 |
. . . . 5
β’ (π β (πΉ β ((π½ βΎt π΄) Cn πΎ) β (πΉ:π΄βΆπ΅ β§ βπ β (Filβπ΄)βπ₯ β ((π½ βΎt π΄) fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) |
23 | 8, 22 | mpbid 231 |
. . . 4
β’ (π β (πΉ:π΄βΆπ΅ β§ βπ β (Filβπ΄)βπ₯ β ((π½ βΎt π΄) fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ))) |
24 | 23 | simprd 497 |
. . 3
β’ (π β βπ β (Filβπ΄)βπ₯ β ((π½ βΎt π΄) fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)) |
25 | 10 | sscls 22430 |
. . . . . 6
β’ ((π½ β Top β§ π΄ β πΆ) β π΄ β ((clsβπ½)βπ΄)) |
26 | 9, 13, 25 | syl2anc 585 |
. . . . 5
β’ (π β π΄ β ((clsβπ½)βπ΄)) |
27 | | flfcntr.y |
. . . . 5
β’ (π β π β π΄) |
28 | 26, 27 | sseldd 3949 |
. . . 4
β’ (π β π β ((clsβπ½)βπ΄)) |
29 | 13, 27 | sseldd 3949 |
. . . . 5
β’ (π β π β πΆ) |
30 | | trnei 23266 |
. . . . 5
β’ ((π½ β (TopOnβπΆ) β§ π΄ β πΆ β§ π β πΆ) β (π β ((clsβπ½)βπ΄) β (((neiβπ½)β{π}) βΎt π΄) β (Filβπ΄))) |
31 | 12, 13, 29, 30 | syl3anc 1372 |
. . . 4
β’ (π β (π β ((clsβπ½)βπ΄) β (((neiβπ½)β{π}) βΎt π΄) β (Filβπ΄))) |
32 | 28, 31 | mpbid 231 |
. . 3
β’ (π β (((neiβπ½)β{π}) βΎt π΄) β (Filβπ΄)) |
33 | 7, 24, 32 | rspcdva 3584 |
. 2
β’ (π β βπ₯ β ((π½ βΎt π΄) fLim (((neiβπ½)β{π}) βΎt π΄))(πΉβπ₯) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |
34 | | neiflim 23348 |
. . . 4
β’ (((π½ βΎt π΄) β (TopOnβπ΄) β§ π β π΄) β π β ((π½ βΎt π΄) fLim ((neiβ(π½ βΎt π΄))β{π}))) |
35 | 15, 27, 34 | syl2anc 585 |
. . 3
β’ (π β π β ((π½ βΎt π΄) fLim ((neiβ(π½ βΎt π΄))β{π}))) |
36 | 27 | snssd 4773 |
. . . . 5
β’ (π β {π} β π΄) |
37 | 10 | neitr 22554 |
. . . . 5
β’ ((π½ β Top β§ π΄ β πΆ β§ {π} β π΄) β ((neiβ(π½ βΎt π΄))β{π}) = (((neiβπ½)β{π}) βΎt π΄)) |
38 | 9, 13, 36, 37 | syl3anc 1372 |
. . . 4
β’ (π β ((neiβ(π½ βΎt π΄))β{π}) = (((neiβπ½)β{π}) βΎt π΄)) |
39 | 38 | oveq2d 7377 |
. . 3
β’ (π β ((π½ βΎt π΄) fLim ((neiβ(π½ βΎt π΄))β{π})) = ((π½ βΎt π΄) fLim (((neiβπ½)β{π}) βΎt π΄))) |
40 | 35, 39 | eleqtrd 2836 |
. 2
β’ (π β π β ((π½ βΎt π΄) fLim (((neiβπ½)β{π}) βΎt π΄))) |
41 | 2, 33, 40 | rspcdva 3584 |
1
β’ (π β (πΉβπ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) |