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 snnzg ⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ≠ ∅ )
16 11 15 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → { 𝐴 } ≠ ∅ )
17 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ∧ { 𝐴 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
18 10 14 16 17 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
19 oveq2 ⊢ ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝐽 fLim 𝑓 ) = ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
20 19 eleq2d ⊢ ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) ↔ 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ) )
21 oveq2 ⊢ ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( 𝐾 fLimf 𝑓 ) = ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
22 21 fveq1d ⊢ ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) = ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) )
23 22 eleq2d ⊢ ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) )
24 20 23 imbi12d ⊢ ( 𝑓 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ↔ ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
25 24 rspcv ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
26 18 25 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
27 13 26 mpid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) )
28 27 imdistanda ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
29 eqid ⊢ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } )
30 29 cnpflf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) ‘ 𝐹 ) ) ) )
31 28 30 sylibrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) )
32 9 31 impbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐴 ∈ ( 𝐽 fLim 𝑓 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) ) )