Metamath Proof Explorer

Theorem cnfcf

Description: Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnfcf 
|- ( ( 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 fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 cncnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
2 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. X ) -> F : X --> Y )
3 cnpfcf 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) ) )
4 3 ad4ant124 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) ) )
5 2 4 mpbirand 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> A. f e. ( Fil ` X ) ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
6 5 ralbidva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. X F e. ( ( J CnP K ) ` x ) <-> A. x e. X A. f e. ( Fil ` X ) ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
7 ralcom 
 |-  ( A. x e. X A. f e. ( Fil ` X ) ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) <-> A. f e. ( Fil ` X ) A. x e. X ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) )
8 eqid 
 |-  U. J = U. J
9 8 fclselbas 
 |-  ( x e. ( J fClus f ) -> x e. U. J )
10 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
11 10 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> X = U. J )
12 11 eleq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( x e. X <-> x e. U. J ) )
13 9 12 syl5ibr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( x e. ( J fClus f ) -> x e. X ) )
14 13 pm4.71rd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( x e. ( J fClus f ) <-> ( x e. X /\ x e. ( J fClus f ) ) ) )
15 14 imbi1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) <-> ( ( x e. X /\ x e. ( J fClus f ) ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
16 impexp 
 |-  ( ( ( x e. X /\ x e. ( J fClus f ) ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) <-> ( x e. X -> ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
17 15 16 bitrdi 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) <-> ( x e. X -> ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) ) )
18 17 ralbidv2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. ( J fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) <-> A. x e. X ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
19 18 ralbidv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. f e. ( Fil ` X ) A. x e. ( J fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) <-> A. f e. ( Fil ` X ) A. x e. X ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
20 7 19 bitr4id 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. X A. f e. ( Fil ` X ) ( x e. ( J fClus f ) -> ( F ` x ) e. ( ( K fClusf f ) ` F ) ) <-> A. f e. ( Fil ` X ) A. x e. ( J fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) ) )
21 6 20 bitrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( A. x e. X F e. ( ( J CnP K ) ` x ) <-> A. f e. ( Fil ` X ) A. x e. ( J fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) ) )
22 21 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) A. x e. ( J fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )
23 1 22 bitrd 
 |-  ( ( 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 fClus f ) ( F ` x ) e. ( ( K fClusf f ) ` F ) ) ) )