Metamath Proof Explorer

Theorem cnpflf

Description: Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

Ref Expression
Assertion cnpflf 
|- ( ( 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 fLim f ) -> ( F ` A ) e. ( ( K fLimf 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 cnpflfi 
 |-  ( ( A e. ( J fLim f ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) )
5 4 expcom 
 |-  ( F e. ( ( J CnP K ) ` A ) -> ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) )
6 5 ralrimivw 
 |-  ( F e. ( ( J CnP K ) ` A ) -> A. f e. ( Fil ` X ) ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) )
7 6 adantl 
 |-  ( ( ( 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 fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) )
8 3 7 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 fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) ) )
9 8 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 fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) ) ) )
10 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> J e. ( TopOn ` X ) )
11 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> A e. X )
12 neiflim 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. ( J fLim ( ( nei ` J ) ` { A } ) ) )
13 10 11 12 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> A e. ( J fLim ( ( nei ` J ) ` { A } ) ) )
14 11 snssd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> { A } C_ X )
15 11 snn0d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> { A } =/= (/) )
16 neifil 
 |-  ( ( J e. ( TopOn ` X ) /\ { A } C_ X /\ { A } =/= (/) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
17 10 14 15 16 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
18 oveq2 
 |-  ( f = ( ( nei ` J ) ` { A } ) -> ( J fLim f ) = ( J fLim ( ( nei ` J ) ` { A } ) ) )
19 18 eleq2d 
 |-  ( f = ( ( nei ` J ) ` { A } ) -> ( A e. ( J fLim f ) <-> A e. ( J fLim ( ( nei ` J ) ` { A } ) ) ) )
20 oveq2 
 |-  ( f = ( ( nei ` J ) ` { A } ) -> ( K fLimf f ) = ( K fLimf ( ( nei ` J ) ` { A } ) ) )
21 20 fveq1d 
 |-  ( f = ( ( nei ` J ) ` { A } ) -> ( ( K fLimf f ) ` F ) = ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) )
22 21 eleq2d 
 |-  ( f = ( ( nei ` J ) ` { A } ) -> ( ( F ` A ) e. ( ( K fLimf f ) ` F ) <-> ( F ` A ) e. ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) ) )
23 19 22 imbi12d 
 |-  ( f = ( ( nei ` J ) ` { A } ) -> ( ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) <-> ( A e. ( J fLim ( ( nei ` J ) ` { A } ) ) -> ( F ` A ) e. ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) ) ) )
24 23 rspcv 
 |-  ( ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) -> ( A e. ( J fLim ( ( nei ` J ) ` { A } ) ) -> ( F ` A ) e. ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) ) ) )
25 17 24 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) -> ( A e. ( J fLim ( ( nei ` J ) ` { A } ) ) -> ( F ` A ) e. ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) ) ) )
26 13 25 mpid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) /\ F : X --> Y ) -> ( A. f e. ( Fil ` X ) ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) -> ( F ` A ) e. ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) ) )
27 26 imdistanda 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) ) -> ( F : X --> Y /\ ( F ` A ) e. ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) ) ) )
28 eqid 
 |-  ( ( nei ` J ) ` { A } ) = ( ( nei ` J ) ` { A } )
29 28 cnpflf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> ( F : X --> Y /\ ( F ` A ) e. ( ( K fLimf ( ( nei ` J ) ` { A } ) ) ` F ) ) ) )
30 27 29 sylibrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ A e. X ) -> ( ( F : X --> Y /\ A. f e. ( Fil ` X ) ( A e. ( J fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) ) -> F e. ( ( J CnP K ) ` A ) ) )
31 9 30 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 fLim f ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) ) ) )