Description: Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 23-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | flimcf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplll | |
|
2 | simprl | |
|
3 | simplr | |
|
4 | flimss1 | |
|
5 | 1 2 3 4 | syl3anc | |
6 | simprr | |
|
7 | 5 6 | sseldd | |
8 | 7 | expr | |
9 | 8 | ssrdv | |
10 | 9 | ralrimiva | |
11 | oveq2 | |
|
12 | oveq2 | |
|
13 | 11 12 | sseq12d | |
14 | simplr | |
|
15 | simpllr | |
|
16 | simplll | |
|
17 | simprl | |
|
18 | toponss | |
|
19 | 16 17 18 | syl2anc | |
20 | simprr | |
|
21 | 19 20 | sseldd | |
22 | 21 | snssd | |
23 | 20 | snn0d | |
24 | neifil | |
|
25 | 15 22 23 24 | syl3anc | |
26 | 13 14 25 | rspcdva | |
27 | neiflim | |
|
28 | 15 21 27 | syl2anc | |
29 | 26 28 | sseldd | |
30 | flimneiss | |
|
31 | 29 30 | syl | |
32 | topontop | |
|
33 | 16 32 | syl | |
34 | opnneip | |
|
35 | 33 17 20 34 | syl3anc | |
36 | 31 35 | sseldd | |
37 | 36 | anassrs | |
38 | 37 | ralrimiva | |
39 | simpllr | |
|
40 | topontop | |
|
41 | opnnei | |
|
42 | 39 40 41 | 3syl | |
43 | 38 42 | mpbird | |
44 | 43 | ex | |
45 | 44 | ssrdv | |
46 | 10 45 | impbida | |