Description: A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | flfcntr.c | |
|
flfcntr.b | |
||
flfcntr.j | |
||
flfcntr.a | |
||
flfcntr.1 | |
||
flfcntr.y | |
||
Assertion | flfcntr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flfcntr.c | |
|
2 | flfcntr.b | |
|
3 | flfcntr.j | |
|
4 | flfcntr.a | |
|
5 | flfcntr.1 | |
|
6 | flfcntr.y | |
|
7 | fveq2 | |
|
8 | 7 | eleq1d | |
9 | oveq2 | |
|
10 | oveq2 | |
|
11 | 10 | fveq1d | |
12 | 11 | eleq2d | |
13 | 9 12 | raleqbidv | |
14 | 1 | toptopon | |
15 | 3 14 | sylib | |
16 | resttopon | |
|
17 | 15 4 16 | syl2anc | |
18 | cntop2 | |
|
19 | 5 18 | syl | |
20 | 2 | toptopon | |
21 | 19 20 | sylib | |
22 | cnflf | |
|
23 | 17 21 22 | syl2anc | |
24 | 5 23 | mpbid | |
25 | 24 | simprd | |
26 | 1 | sscls | |
27 | 3 4 26 | syl2anc | |
28 | 27 6 | sseldd | |
29 | 4 6 | sseldd | |
30 | trnei | |
|
31 | 15 4 29 30 | syl3anc | |
32 | 28 31 | mpbid | |
33 | 13 25 32 | rspcdva | |
34 | neiflim | |
|
35 | 17 6 34 | syl2anc | |
36 | 6 | snssd | |
37 | 1 | neitr | |
38 | 3 4 36 37 | syl3anc | |
39 | 38 | oveq2d | |
40 | 35 39 | eleqtrd | |
41 | 8 33 40 | rspcdva | |