Description: A limit point of a filter is a limit point in a coarser topology. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | flimss1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | flimelbas | |
3 | 2 | adantl | |
4 | simpl2 | |
|
5 | filunibas | |
|
6 | 4 5 | syl | |
7 | 1 | flimfil | |
8 | 7 | adantl | |
9 | filunibas | |
|
10 | 8 9 | syl | |
11 | 6 10 | eqtr3d | |
12 | 3 11 | eleqtrrd | |
13 | simpl1 | |
|
14 | topontop | |
|
15 | 13 14 | syl | |
16 | flimtop | |
|
17 | 16 | adantl | |
18 | toponuni | |
|
19 | 13 18 | syl | |
20 | 19 11 | eqtr3d | |
21 | simpl3 | |
|
22 | eqid | |
|
23 | 22 1 | topssnei | |
24 | 15 17 20 21 23 | syl31anc | |
25 | flimneiss | |
|
26 | 25 | adantl | |
27 | 24 26 | sstrd | |
28 | elflim | |
|
29 | 13 4 28 | syl2anc | |
30 | 12 27 29 | mpbir2and | |
31 | 30 | ex | |
32 | 31 | ssrdv | |