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

Metamath Proof Explorer

Theorem metcnp3

Description: Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of Gleason p. 240. (Contributed by NM, 17-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 1 mopntopon ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 3 3ad2ant1 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 2 mopnval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
6 5 3ad2ant2 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
7 2 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
8 7 3ad2ant2 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
9 simp3 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
10 4 6 8 9 tgcnp ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
11 simpll2 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
12 simplr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝐹 : 𝑋 ⟶ 𝑌 )
13 simpll3 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑃 ∈ 𝑋 )
14 12 13 ffvelcdmd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
15 simpr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
16 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) )
17 11 14 15 16 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) )
18 rpxr ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ* )
19 18 adantl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ* )
20 blelrn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ∧ 𝑦 ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∈ ran ( ball ‘ 𝐷 ) )
21 11 14 19 20 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∈ ran ( ball ‘ 𝐷 ) )
22 eleq2 ⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
23 sseq2 ⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
24 23 anbi2d ⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
25 24 rexbidv ⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
26 22 25 imbi12d ⊢ ( 𝑢 = ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ( ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) )
27 26 rspcv ⊢ ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∈ ran ( ball ‘ 𝐷 ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) )
28 21 27 syl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) ) )
29 17 28 mpid ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
30 simpl1 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
31 30 ad2antrr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
32 simplrr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → 𝑣 ∈ 𝐽 )
33 simpr ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → 𝑃 ∈ 𝑣 )
34 1 mopni2 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ∧ 𝑃 ∈ 𝑣 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 )
35 31 32 33 34 syl3anc ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 )
36 sstr2 ⊢ ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( 𝐹 “ 𝑣 ) → ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
37 imass2 ⊢ ( ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( 𝐹 “ 𝑣 ) )
38 36 37 syl11 ⊢ ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
39 38 reximdv ⊢ ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ∃ 𝑧 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ⊆ 𝑣 → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
40 35 39 syl5com ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) → ( ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
41 40 expimpd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
42 41 expr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑣 ∈ 𝐽 → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
43 42 rexlimdv ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
44 29 43 syld ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
45 44 ralrimdva ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
46 simpl2 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
47 blss ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 )
48 47 3expib ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) )
49 46 48 syl ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) )
50 r19.29r ⊢ ( ( ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑦 ∈ ℝ+ ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
51 30 ad3antrrr ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
52 13 ad2antrr ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑃 ∈ 𝑋 )
53 rpxr ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ* )
54 53 ad2antrl ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑧 ∈ ℝ* )
55 1 blopn ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∈ 𝐽 )
56 51 52 54 55 syl3anc ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∈ 𝐽 )
57 simprl ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑧 ∈ ℝ+ )
58 blcntr ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ+ ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) )
59 51 52 57 58 syl3anc ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) )
60 sstr ⊢ ( ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 )
61 60 ad2ant2l ⊢ ( ( ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ∧ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 )
62 61 ancoms ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 )
63 eleq2 ⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( 𝑃 ∈ 𝑣 ↔ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) )
64 imaeq2 ⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( 𝐹 “ 𝑣 ) = ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) )
65 64 sseq1d ⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ↔ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) )
66 63 65 anbi12d ⊢ ( 𝑣 = ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) → ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) ) )
67 66 rspcev ⊢ ( ( ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) )
68 56 59 62 67 syl12anc ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) )
69 68 expr ⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
70 69 rexlimdva ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ) → ( ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
71 70 expimpd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
72 71 rexlimdva ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∃ 𝑦 ∈ ℝ+ ( ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
73 50 72 syl5 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) )
74 73 expd ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∃ 𝑦 ∈ ℝ+ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝑢 → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) )
75 49 74 syld ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) )
76 75 com23 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) )
77 76 exp4a ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ( 𝑢 ∈ ran ( ball ‘ 𝐷 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
78 77 ralrimdv ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) → ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) )
79 45 78 impbid ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) )
80 79 pm5.32da ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ ran ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑢 → ∃ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 “ 𝑣 ) ⊆ 𝑢 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )
81 10 80 bitrd ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝐹 “ ( 𝑃 ( ball ‘ 𝐶 ) 𝑧 ) ) ⊆ ( ( 𝐹 ‘ 𝑃 ) ( ball ‘ 𝐷 ) 𝑦 ) ) ) )