Metamath Proof Explorer


Theorem cnflf2

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 JTopOnXKTopOnYFJCnKF:XYfFilXFJfLimfKfLimffF

Proof

Step Hyp Ref Expression
1 cnflf JTopOnXKTopOnYFJCnKF:XYfFilXxJfLimfFxKfLimffF
2 ffun F:XYFunF
3 eqid J=J
4 3 flimelbas xJfLimfxJ
5 4 ssriv JfLimfJ
6 fdm F:XYdomF=X
7 6 adantl JTopOnXKTopOnYF:XYdomF=X
8 toponuni JTopOnXX=J
9 8 ad2antrr JTopOnXKTopOnYF:XYX=J
10 7 9 eqtrd JTopOnXKTopOnYF:XYdomF=J
11 5 10 sseqtrrid JTopOnXKTopOnYF:XYJfLimfdomF
12 funimass4 FunFJfLimfdomFFJfLimfKfLimffFxJfLimfFxKfLimffF
13 2 11 12 syl2an2 JTopOnXKTopOnYF:XYFJfLimfKfLimffFxJfLimfFxKfLimffF
14 13 ralbidv JTopOnXKTopOnYF:XYfFilXFJfLimfKfLimffFfFilXxJfLimfFxKfLimffF
15 14 pm5.32da JTopOnXKTopOnYF:XYfFilXFJfLimfKfLimffFF:XYfFilXxJfLimfFxKfLimffF
16 1 15 bitr4d JTopOnXKTopOnYFJCnKF:XYfFilXFJfLimfKfLimffF