This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑓 ) ‘ 𝐹 ) ) ) ) )