Metamath Proof Explorer

Theorem cnpflf2

Description: F is continuous at point A iff a limit of F when x tends to A is ( FA ) . Proposition 9 of BourbakiTop1 p. TG I.50. (Contributed by FL, 29-May-2011) (Revised by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypothesis cnpflf2.3 ⊢ 𝐿 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } )
Assertion cnpflf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 cnpflf2.3 ⊢ 𝐿 = ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } )
2 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
3 2 3expa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
4 3 3adantl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
5 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐴 ∈ 𝑋 )
7 neiflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) )
8 1 oveq2i ⊢ ( 𝐽 fLim 𝐿 ) = ( 𝐽 fLim ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
9 7 8 eleqtrrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( 𝐽 fLim 𝐿 ) )
10 5 6 9 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐿 ) )
11 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )
12 cnpflfi ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐿 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) )
13 10 11 12 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) )
14 4 13 jca ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ) )
15 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
16 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
17 15 16 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐽 ∈ Top )
18 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐴 ∈ 𝑋 )
19 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
20 15 19 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝑋 = ∪ 𝐽 )
21 18 20 eleqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐴 ∈ ∪ 𝐽 )
22 1 eleq2i ⊢ ( 𝑧 ∈ 𝐿 ↔ 𝑧 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
23 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
24 23 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ∪ 𝐽 ) → ( 𝑧 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ ( 𝑧 ⊆ ∪ 𝐽 ∧ ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ) ) )
25 22 24 syl5bb ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ∪ 𝐽 ) → ( 𝑧 ∈ 𝐿 ↔ ( 𝑧 ⊆ ∪ 𝐽 ∧ ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ) ) )
26 17 21 25 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑧 ∈ 𝐿 ↔ ( 𝑧 ⊆ ∪ 𝐽 ∧ ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ) ) )
27 sstr2 ⊢ ( ( 𝐹 “ 𝑣 ) ⊆ ( 𝐹 “ 𝑧 ) → ( ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) )
28 imass2 ⊢ ( 𝑣 ⊆ 𝑧 → ( 𝐹 “ 𝑣 ) ⊆ ( 𝐹 “ 𝑧 ) )
29 27 28 syl11 ⊢ ( ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ( 𝑣 ⊆ 𝑧 → ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) )
30 29 anim2d ⊢ ( ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ( ( 𝐴 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) → ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
31 30 reximdv ⊢ ( ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ( ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
32 31 com12 ⊢ ( ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) → ( ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
33 32 adantl ⊢ ( ( 𝑧 ⊆ ∪ 𝐽 ∧ ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑧 ) ) → ( ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
34 26 33 syl6bi ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑧 ∈ 𝐿 → ( ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) )
35 34 rexlimdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∃ 𝑧 ∈ 𝐿 ( 𝐹 “ 𝑧 ) ⊆ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
36 35 imim2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑧 ∈ 𝐿 ( 𝐹 “ 𝑧 ) ⊆ 𝑢 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) )
37 36 ralimdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑧 ∈ 𝐿 ( 𝐹 “ 𝑧 ) ⊆ 𝑢 ) → ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) )
38 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
39 37 38 jctild ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑧 ∈ 𝐿 ( 𝐹 “ 𝑧 ) ⊆ 𝑢 ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
40 39 adantld ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑧 ∈ 𝐿 ( 𝐹 “ 𝑧 ) ⊆ 𝑢 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
41 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
42 18 snssd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → { 𝐴 } ⊆ 𝑋 )
43 snnzg ⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ≠ ∅ )
44 18 43 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → { 𝐴 } ≠ ∅ )
45 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ∧ { 𝐴 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
46 15 42 44 45 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∈ ( Fil ‘ 𝑋 ) )
47 1 46 eqeltrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
48 isflf ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑧 ∈ 𝐿 ( 𝐹 “ 𝑧 ) ⊆ 𝑢 ) ) ) )
49 41 47 38 48 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑧 ∈ 𝐿 ( 𝐹 “ 𝑧 ) ⊆ 𝑢 ) ) ) )
50 iscnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
51 50 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝐾 ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝐴 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
52 40 49 51 3imtr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ) )
53 52 impr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) )
54 14 53 impbida ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐴 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ 𝐹 ) ) ) )