Metamath Proof Explorer

Theorem metcnp

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . (Contributed by NM, 11-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion metcnp ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 1 2 metcnp3 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
4 ffun ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → Fun 𝐹 )
5 4 ad2antlr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → Fun 𝐹 )
6 simpll1 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
7 simpll3 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑃 ∈ 𝑋 )
8 rpxr ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ* )
9 8 ad2antll ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑧 ∈ ℝ* )
10 blssm ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑋 )
11 6 7 9 10 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑋 )
12 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
13 12 ad2antlr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → dom 𝐹 = 𝑋 )
14 11 13 sseqtrrd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ dom 𝐹 )
15 funimass4 ⊢ ( ( Fun 𝐹 ∧ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑤 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
16 5 14 15 syl2anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑤 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
17 elbl ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ* ) → ( 𝑤 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑤 ) < 𝑧 ) ) )
18 6 7 9 17 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( 𝑤 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ↔ ( 𝑤 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑤 ) < 𝑧 ) ) )
19 18 imbi1d ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( 𝑤 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ↔ ( ( 𝑤 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑤 ) < 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
20 impexp ⊢ ( ( ( 𝑤 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑤 ) < 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑋 → ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
21 simpl2 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
22 21 ad2antrr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
23 simplrl ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝑦 ∈ ℝ+ )
24 23 rpxrd ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝑦 ∈ ℝ* )
25 simpllr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
26 7 adantr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
27 25 26 ffvelcdmd ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
28 simplr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
29 28 ffvelcdmda ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑌 )
30 elbl2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑦 ∈ ℝ* ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) )
31 22 24 27 29 30 syl22anc ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) )
32 31 imbi2d ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ↔ ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) )
33 32 pm5.74da ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( 𝑤 ∈ 𝑋 → ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ↔ ( 𝑤 ∈ 𝑋 → ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) )
34 20 33 bitrid ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( ( 𝑤 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑤 ) < 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑋 → ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) )
35 19 34 bitrd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( 𝑤 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑋 → ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) )
36 35 ralbidv2 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ∀ 𝑤 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ( 𝐹 ‘ 𝑤 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) )
37 16 36 bitrd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) )
38 37 anassrs ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) )
39 38 rexbidva ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) )
40 39 ralbidva ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) )
41 40 pm5.32da ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) )
42 3 41 bitrd ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑃 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹 ‘ 𝑃 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑦 ) ) ) )