Metamath Proof Explorer

Theorem cnpfcf

Description: A function F is continuous at point A iff F respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnpfcf 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnpf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` A ) ) -> F : X --> Y )
2 1 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( ( J CnP K ) ` A ) ) -> F : X --> Y )
3 2 3adantl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F e. ( ( J CnP K ) ` A ) ) -> F : X --> Y )
4 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
5 cnpfcfi 
 |-  ( ( K e. Top /\ A e. ( J fClus f ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) )
6 5 3com23 
 |-  ( ( K e. Top /\ F e. ( ( J CnP K ) ` A ) /\ A e. ( J fClus f ) ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) )
7 6 3expia 
 |-  ( ( K e. Top /\ F e. ( ( J CnP K ) ` A ) ) -> ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) )
8 4 7 sylan 
 |-  ( ( K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) )
9 8 ralrimivw 
 |-  ( ( K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` A ) ) -> A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) )
10 9 3ad2antl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F e. ( ( J CnP K ) ` A ) ) -> A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) )
11 3 10 jca 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) ) )
12 11 ex 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) -> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) ) ) )
13 simplrl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> g e. ( Fil ` X ) )
14 filfbas 
 |-  ( g e. ( Fil ` X ) -> g e. ( fBas ` X ) )
15 13 14 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> g e. ( fBas ` X ) )
16 simprl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> h e. ( Fil ` Y ) )
17 simpllr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> F : X --> Y )
18 simprr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> ( ( Y FilMap F ) ` g ) C_ h )
19 15 16 17 18 fmfnfm 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> E. f e. ( Fil ` X ) ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) )
20 r19.29 
 |-  ( ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) /\ E. f e. ( Fil ` X ) ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) -> E. f e. ( Fil ` X ) ( ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) )
21 flimfcls 
 |-  ( J fLim f ) C_ ( J fClus f )
22 simpll1 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> J e. ( TopOn ` X ) )
23 22 ad2antrr 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> J e. ( TopOn ` X ) )
24 simprl 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> f e. ( Fil ` X ) )
25 simprrl 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> g C_ f )
26 flimss2 
 |-  ( ( J e. ( TopOn ` X ) /\ f e. ( Fil ` X ) /\ g C_ f ) -> ( J fLim g ) C_ ( J fLim f ) )
27 23 24 25 26 syl3anc 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> ( J fLim g ) C_ ( J fLim f ) )
28 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> A e. ( J fLim g ) )
29 28 ad2antrr 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> A e. ( J fLim g ) )
30 27 29 sseldd 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> A e. ( J fLim f ) )
31 21 30 sselid 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> A e. ( J fClus f ) )
32 simpll2 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> K e. ( TopOn ` Y ) )
33 32 ad2antrr 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> K e. ( TopOn ` Y ) )
34 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> F : X --> Y )
35 34 ad2antrr 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> F : X --> Y )
36 fcfval 
 |-  ( ( K e. ( TopOn ` Y ) /\ f e. ( Fil ` X ) /\ F : X --> Y ) -> ( ( K fClusf f ) ` F ) = ( K fClus ( ( Y FilMap F ) ` f ) ) )
37 33 24 35 36 syl3anc 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> ( ( K fClusf f ) ` F ) = ( K fClus ( ( Y FilMap F ) ` f ) ) )
38 simprrr 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> h = ( ( Y FilMap F ) ` f ) )
39 38 oveq2d 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> ( K fClus h ) = ( K fClus ( ( Y FilMap F ) ` f ) ) )
40 37 39 eqtr4d 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> ( ( K fClusf f ) ` F ) = ( K fClus h ) )
41 40 eleq2d 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> ( ( F ` A ) e. ( ( K fClusf f ) ` F ) <-> ( F ` A ) e. ( K fClus h ) ) )
42 41 biimpd 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> ( ( F ` A ) e. ( ( K fClusf f ) ` F ) -> ( F ` A ) e. ( K fClus h ) ) )
43 31 42 embantd 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ ( f e. ( Fil ` X ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) ) -> ( ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( F ` A ) e. ( K fClus h ) ) )
44 43 expr 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ f e. ( Fil ` X ) ) -> ( ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) -> ( ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( F ` A ) e. ( K fClus h ) ) ) )
45 44 impcomd 
 |-  ( ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) /\ f e. ( Fil ` X ) ) -> ( ( ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) -> ( F ` A ) e. ( K fClus h ) ) )
46 45 rexlimdva 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> ( E. f e. ( Fil ` X ) ( ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) /\ ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) -> ( F ` A ) e. ( K fClus h ) ) )
47 20 46 syl5 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> ( ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) /\ E. f e. ( Fil ` X ) ( g C_ f /\ h = ( ( Y FilMap F ) ` f ) ) ) -> ( F ` A ) e. ( K fClus h ) ) )
48 19 47 mpan2d 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ ( h e. ( Fil ` Y ) /\ ( ( Y FilMap F ) ` g ) C_ h ) ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( F ` A ) e. ( K fClus h ) ) )
49 48 expr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ h e. ( Fil ` Y ) ) -> ( ( ( Y FilMap F ) ` g ) C_ h -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( F ` A ) e. ( K fClus h ) ) ) )
50 49 com23 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) /\ h e. ( Fil ` Y ) ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( ( ( Y FilMap F ) ` g ) C_ h -> ( F ` A ) e. ( K fClus h ) ) ) )
51 50 ralrimdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> A. h e. ( Fil ` Y ) ( ( ( Y FilMap F ) ` g ) C_ h -> ( F ` A ) e. ( K fClus h ) ) ) )
52 toponmax 
 |-  ( K e. ( TopOn ` Y ) -> Y e. K )
53 32 52 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> Y e. K )
54 simprl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> g e. ( Fil ` X ) )
55 54 14 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> g e. ( fBas ` X ) )
56 fmfil 
 |-  ( ( Y e. K /\ g e. ( fBas ` X ) /\ F : X --> Y ) -> ( ( Y FilMap F ) ` g ) e. ( Fil ` Y ) )
57 53 55 34 56 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( ( Y FilMap F ) ` g ) e. ( Fil ` Y ) )
58 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
59 32 58 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> Y = U. K )
60 59 fveq2d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( Fil ` Y ) = ( Fil ` U. K ) )
61 57 60 eleqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( ( Y FilMap F ) ` g ) e. ( Fil ` U. K ) )
62 eqid 
 |-  U. K = U. K
63 62 flimfnfcls 
 |-  ( ( ( Y FilMap F ) ` g ) e. ( Fil ` U. K ) -> ( ( F ` A ) e. ( K fLim ( ( Y FilMap F ) ` g ) ) <-> A. h e. ( Fil ` U. K ) ( ( ( Y FilMap F ) ` g ) C_ h -> ( F ` A ) e. ( K fClus h ) ) ) )
64 61 63 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( ( F ` A ) e. ( K fLim ( ( Y FilMap F ) ` g ) ) <-> A. h e. ( Fil ` U. K ) ( ( ( Y FilMap F ) ` g ) C_ h -> ( F ` A ) e. ( K fClus h ) ) ) )
65 flfval 
 |-  ( ( K e. ( TopOn ` Y ) /\ g e. ( Fil ` X ) /\ F : X --> Y ) -> ( ( K fLimf g ) ` F ) = ( K fLim ( ( Y FilMap F ) ` g ) ) )
66 32 54 34 65 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( ( K fLimf g ) ` F ) = ( K fLim ( ( Y FilMap F ) ` g ) ) )
67 66 eleq2d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( ( F ` A ) e. ( ( K fLimf g ) ` F ) <-> ( F ` A ) e. ( K fLim ( ( Y FilMap F ) ` g ) ) ) )
68 60 raleqdv 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( A. h e. ( Fil ` Y ) ( ( ( Y FilMap F ) ` g ) C_ h -> ( F ` A ) e. ( K fClus h ) ) <-> A. h e. ( Fil ` U. K ) ( ( ( Y FilMap F ) ` g ) C_ h -> ( F ` A ) e. ( K fClus h ) ) ) )
69 64 67 68 3bitr4d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( ( F ` A ) e. ( ( K fLimf g ) ` F ) <-> A. h e. ( Fil ` Y ) ( ( ( Y FilMap F ) ` g ) C_ h -> ( F ` A ) e. ( K fClus h ) ) ) )
70 51 69 sylibrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ ( g e. ( Fil ` X ) /\ A e. ( J fLim g ) ) ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( F ` A ) e. ( ( K fLimf g ) ` F ) ) )
71 70 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ g e. ( Fil ` X ) ) -> ( A e. ( J fLim g ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( F ` A ) e. ( ( K fLimf g ) ` F ) ) ) )
72 71 com23 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) /\ g e. ( Fil ` X ) ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> ( A e. ( J fLim g ) -> ( F ` A ) e. ( ( K fLimf g ) ` F ) ) ) )
73 72 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) -> A. g e. ( Fil ` X ) ( A e. ( J fLim g ) -> ( F ` A ) e. ( ( K fLimf g ) ` F ) ) ) )
74 73 imdistanda 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) ) -> ( F : X --> Y /\ A. g e. ( Fil ` X ) ( A e. ( J fLim g ) -> ( F ` A ) e. ( ( K fLimf g ) ` F ) ) ) ) )
75 cnpflf 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> Y /\ A. g e. ( Fil ` X ) ( A e. ( J fLim g ) -> ( F ` A ) e. ( ( K fLimf g ) ` F ) ) ) ) )
76 74 75 sylibrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) ) -> F e. ( ( J CnP K ) ` A ) ) )
77 12 76 impbid 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fClus f ) -> ( F ` A ) e. ( ( K fClusf f ) ` F ) ) ) ) )