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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cnpf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋𝑌 )
2 1 3expa ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋𝑌 )
3 2 3adantl3 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋𝑌 )
4 cnpflfi ( ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) )
5 4 expcom ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) )
6 5 ralrimivw ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) )
7 6 adantl ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) )
8 3 7 jca ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) )
9 8 ex ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) → ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) ) )
10 simpl1 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
11 simpl3 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → 𝐴𝑋 )
12 neiflim ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴𝑋 ) → 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
13 10 11 12 syl2anc ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
14 11 snssd ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → { 𝐴 } ⊆ 𝑋 )
15 11 snn0d ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → { 𝐴 } ≠ ∅ )
16 neifil ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ∧ { 𝐴 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
17 10 14 15 16 syl3anc ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
18 oveq2 ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝐽 fLim 𝑓 ) = ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
19 18 eleq2d ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ↔ 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
20 oveq2 ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝐾 fLimf 𝑓 ) = ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
21 20 fveq1d ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) )
22 21 eleq2d ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ↔ ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) )
23 19 22 imbi12d ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ↔ ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
24 23 rspcv ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
25 17 24 syl ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
26 13 25 mpid ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) )
27 26 imdistanda ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) → ( ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) → ( 𝐹 : 𝑋𝑌 ∧ ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
28 eqid ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } )
29 28 cnpflf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
30 27 29 sylibrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) → ( ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) )
31 9 30 impbid ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) ) )