Metamath Proof Explorer

Theorem metcnpi3

Description: Epsilon-delta property of a metric space function continuous at P . A variation of metcnpi2 with non-strict ordering. (Contributed by NM, 16-Dec-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypotheses metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion metcnpi3 ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) ≤ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 metcn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metcn.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 1 2 metcnpi2 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) )
4 rphalfcl ⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 / 2 ) ∈ ℝ+ )
5 4 ad2antrl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) ) ) → ( 𝑧 / 2 ) ∈ ℝ+ )
6 simplll ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
7 simprr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
8 simplrl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) )
9 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
10 9 cnprcl ⊢ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → 𝑃 ∈ ∪ 𝐽 )
11 8 10 syl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝑃 ∈ ∪ 𝐽 )
12 1 mopnuni ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
13 6 12 syl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 = ∪ 𝐽 )
14 11 13 eleqtrrd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝑃 ∈ 𝑋 )
15 xmetcl ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑦 𝐶 𝑃 ) ∈ ℝ* )
16 6 7 14 15 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 𝐶 𝑃 ) ∈ ℝ* )
17 4 ad2antrl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 / 2 ) ∈ ℝ+ )
18 17 rpxrd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 / 2 ) ∈ ℝ* )
19 rpxr ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ* )
20 19 ad2antrl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝑧 ∈ ℝ* )
21 rphalflt ⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 / 2 ) < 𝑧 )
22 21 ad2antrl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑧 / 2 ) < 𝑧 )
23 xrlelttr ⊢ ( ( ( 𝑦 𝐶 𝑃 ) ∈ ℝ* ∧ ( 𝑧 / 2 ) ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) ∧ ( 𝑧 / 2 ) < 𝑧 ) → ( 𝑦 𝐶 𝑃 ) < 𝑧 ) )
24 23 expcomd ⊢ ( ( ( 𝑦 𝐶 𝑃 ) ∈ ℝ* ∧ ( 𝑧 / 2 ) ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑧 / 2 ) < 𝑧 → ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( 𝑦 𝐶 𝑃 ) < 𝑧 ) ) )
25 24 imp ⊢ ( ( ( ( 𝑦 𝐶 𝑃 ) ∈ ℝ* ∧ ( 𝑧 / 2 ) ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( 𝑧 / 2 ) < 𝑧 ) → ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( 𝑦 𝐶 𝑃 ) < 𝑧 ) )
26 16 18 20 22 25 syl31anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( 𝑦 𝐶 𝑃 ) < 𝑧 ) )
27 simpllr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
28 1 mopntopon ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
29 6 28 syl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
30 2 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
31 27 30 syl ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
32 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
33 29 31 8 32 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
34 33 7 ffvelcdmd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 )
35 33 14 ffvelcdmd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 )
36 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ∈ ℝ* )
37 27 34 35 36 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ∈ ℝ* )
38 simplrr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐴 ∈ ℝ+ )
39 38 rpxrd ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → 𝐴 ∈ ℝ* )
40 xrltle ⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) )
41 37 39 40 syl2anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) )
42 26 41 imim12d ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝑦 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) → ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) ) )
43 42 anassrs ⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑦 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) → ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) ) )
44 43 ralimdva ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) → ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) ) )
45 44 impr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) ) ) → ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) )
46 breq2 ⊢ ( 𝑥 = ( 𝑧 / 2 ) → ( ( 𝑦 𝐶 𝑃 ) ≤ 𝑥 ↔ ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) ) )
47 46 rspceaimv ⊢ ( ( ( 𝑧 / 2 ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) ≤ ( 𝑧 / 2 ) → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) ≤ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) )
48 5 45 47 syl2anc ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) < 𝑧 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) < 𝐴 ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) ≤ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) )
49 3 48 rexlimddv ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐶 𝑃 ) ≤ 𝑥 → ( ( 𝐹 ‘ 𝑦 ) 𝐷 ( 𝐹 ‘ 𝑃 ) ) ≤ 𝐴 ) )