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 𝐾 ) β€˜ 𝑃 ) ∧ 𝐴 ∈ ℝ+ ) ) β†’ βˆƒ π‘₯ ∈ ℝ+ βˆ€ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐢 𝑃 ) ≀ π‘₯ β†’ ( ( 𝐹 β€˜ 𝑦 ) 𝐷 ( 𝐹 β€˜ 𝑃 ) ) ≀ 𝐴 ) )