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 J = MetOpen C
metcn.4 K = MetOpen D
Assertion metcnpi3 C ∞Met X D ∞Met Y F J CnP K P A + x + y X y C P x F y D F P A

Proof

Step Hyp Ref Expression
1 metcn.2 J = MetOpen C
2 metcn.4 K = MetOpen D
3 1 2 metcnpi2 C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P < z F y D F P < A
4 rphalfcl z + z 2 +
5 4 ad2antrl C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P < z F y D F P < A z 2 +
6 simplll C ∞Met X D ∞Met Y F J CnP K P A + z + y X C ∞Met X
7 simprr C ∞Met X D ∞Met Y F J CnP K P A + z + y X y X
8 simplrl C ∞Met X D ∞Met Y F J CnP K P A + z + y X F J CnP K P
9 eqid J = J
10 9 cnprcl F J CnP K P P J
11 8 10 syl C ∞Met X D ∞Met Y F J CnP K P A + z + y X P J
12 1 mopnuni C ∞Met X X = J
13 6 12 syl C ∞Met X D ∞Met Y F J CnP K P A + z + y X X = J
14 11 13 eleqtrrd C ∞Met X D ∞Met Y F J CnP K P A + z + y X P X
15 xmetcl C ∞Met X y X P X y C P *
16 6 7 14 15 syl3anc C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P *
17 4 ad2antrl C ∞Met X D ∞Met Y F J CnP K P A + z + y X z 2 +
18 17 rpxrd C ∞Met X D ∞Met Y F J CnP K P A + z + y X z 2 *
19 rpxr z + z *
20 19 ad2antrl C ∞Met X D ∞Met Y F J CnP K P A + z + y X z *
21 rphalflt z + z 2 < z
22 21 ad2antrl C ∞Met X D ∞Met Y F J CnP K P A + z + y X z 2 < z
23 xrlelttr y C P * z 2 * z * y C P z 2 z 2 < z y C P < z
24 23 expcomd y C P * z 2 * z * z 2 < z y C P z 2 y C P < z
25 24 imp y C P * z 2 * z * z 2 < z y C P z 2 y C P < z
26 16 18 20 22 25 syl31anc C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P z 2 y C P < z
27 simpllr C ∞Met X D ∞Met Y F J CnP K P A + z + y X D ∞Met Y
28 1 mopntopon C ∞Met X J TopOn X
29 6 28 syl C ∞Met X D ∞Met Y F J CnP K P A + z + y X J TopOn X
30 2 mopntopon D ∞Met Y K TopOn Y
31 27 30 syl C ∞Met X D ∞Met Y F J CnP K P A + z + y X K TopOn Y
32 cnpf2 J TopOn X K TopOn Y F J CnP K P F : X Y
33 29 31 8 32 syl3anc C ∞Met X D ∞Met Y F J CnP K P A + z + y X F : X Y
34 33 7 ffvelrnd C ∞Met X D ∞Met Y F J CnP K P A + z + y X F y Y
35 33 14 ffvelrnd C ∞Met X D ∞Met Y F J CnP K P A + z + y X F P Y
36 xmetcl D ∞Met Y F y Y F P Y F y D F P *
37 27 34 35 36 syl3anc C ∞Met X D ∞Met Y F J CnP K P A + z + y X F y D F P *
38 simplrr C ∞Met X D ∞Met Y F J CnP K P A + z + y X A +
39 38 rpxrd C ∞Met X D ∞Met Y F J CnP K P A + z + y X A *
40 xrltle F y D F P * A * F y D F P < A F y D F P A
41 37 39 40 syl2anc C ∞Met X D ∞Met Y F J CnP K P A + z + y X F y D F P < A F y D F P A
42 26 41 imim12d C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P < z F y D F P < A y C P z 2 F y D F P A
43 42 anassrs C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P < z F y D F P < A y C P z 2 F y D F P A
44 43 ralimdva C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P < z F y D F P < A y X y C P z 2 F y D F P A
45 44 impr C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P < z F y D F P < A y X y C P z 2 F y D F P A
46 breq2 x = z 2 y C P x y C P z 2
47 46 rspceaimv z 2 + y X y C P z 2 F y D F P A x + y X y C P x F y D F P A
48 5 45 47 syl2anc C ∞Met X D ∞Met Y F J CnP K P A + z + y X y C P < z F y D F P < A x + y X y C P x F y D F P A
49 3 48 rexlimddv C ∞Met X D ∞Met Y F J CnP K P A + x + y X y C P x F y D F P A