Description: A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | cnflf2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnflf | |
|
2 | ffun | |
|
3 | eqid | |
|
4 | 3 | flimelbas | |
5 | 4 | ssriv | |
6 | fdm | |
|
7 | 6 | adantl | |
8 | toponuni | |
|
9 | 8 | ad2antrr | |
10 | 7 9 | eqtrd | |
11 | 5 10 | sseqtrrid | |
12 | funimass4 | |
|
13 | 2 11 12 | syl2an2 | |
14 | 13 | ralbidv | |
15 | 14 | pm5.32da | |
16 | 1 15 | bitr4d | |