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 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( F " ( J fLim f ) ) C_ ( ( K fLimf f ) ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 cnflf 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) A. x e. ( J fLim f ) ( F ` x ) e. ( ( K fLimf f ) ` F ) ) ) )
2 ffun 
 |-  ( F : X --> Y -> Fun F )
3 eqid 
 |-  U. J = U. J
4 3 flimelbas 
 |-  ( x e. ( J fLim f ) -> x e. U. J )
5 4 ssriv 
 |-  ( J fLim f ) C_ U. J
6 fdm 
 |-  ( F : X --> Y -> dom F = X )
7 6 adantl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> dom F = X )
8 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
9 8 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> X = U. J )
10 7 9 eqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> dom F = U. J )
11 5 10 sseqtrrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( J fLim f ) C_ dom F )
12 funimass4 
 |-  ( ( Fun F /\ ( J fLim f ) C_ dom F ) -> ( ( F " ( J fLim f ) ) C_ ( ( K fLimf f ) ` F ) <-> A. x e. ( J fLim f ) ( F ` x ) e. ( ( K fLimf f ) ` F ) ) )
13 2 11 12 syl2an2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( F " ( J fLim f ) ) C_ ( ( K fLimf f ) ` F ) <-> A. x e. ( J fLim f ) ( F ` x ) e. ( ( K fLimf f ) ` F ) ) )
14 13 ralbidv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. f e. ( Fil ` X ) ( F " ( J fLim f ) ) C_ ( ( K fLimf f ) ` F ) <-> A. f e. ( Fil ` X ) A. x e. ( J fLim f ) ( F ` x ) e. ( ( K fLimf f ) ` F ) ) )
15 14 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. f e. ( Fil ` X ) ( F " ( J fLim f ) ) C_ ( ( K fLimf f ) ` F ) ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) A. x e. ( J fLim f ) ( F ` x ) e. ( ( K fLimf f ) ` F ) ) ) )
16 1 15 bitr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( F " ( J fLim f ) ) C_ ( ( K fLimf f ) ` F ) ) ) )