Metamath Proof Explorer


Theorem metcnpi

Description: Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp . (Contributed by NM, 17-Dec-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypotheses metcn.2 J = MetOpen C
metcn.4 K = MetOpen D
Assertion metcnpi C ∞Met X D ∞Met Y F J CnP K P A + x + y X P C y < x F P D F y < A

Proof

Step Hyp Ref Expression
1 metcn.2 J = MetOpen C
2 metcn.4 K = MetOpen D
3 simpr C ∞Met X D ∞Met Y F J CnP K P F J CnP K P
4 simpll C ∞Met X D ∞Met Y F J CnP K P C ∞Met X
5 simplr C ∞Met X D ∞Met Y F J CnP K P D ∞Met Y
6 eqid J = J
7 6 cnprcl F J CnP K P P J
8 7 adantl C ∞Met X D ∞Met Y F J CnP K P P J
9 1 mopnuni C ∞Met X X = J
10 9 ad2antrr C ∞Met X D ∞Met Y F J CnP K P X = J
11 8 10 eleqtrrd C ∞Met X D ∞Met Y F J CnP K P P X
12 1 2 metcnp C ∞Met X D ∞Met Y P X F J CnP K P F : X Y z + x + y X P C y < x F P D F y < z
13 4 5 11 12 syl3anc C ∞Met X D ∞Met Y F J CnP K P F J CnP K P F : X Y z + x + y X P C y < x F P D F y < z
14 3 13 mpbid C ∞Met X D ∞Met Y F J CnP K P F : X Y z + x + y X P C y < x F P D F y < z
15 breq2 z = A F P D F y < z F P D F y < A
16 15 imbi2d z = A P C y < x F P D F y < z P C y < x F P D F y < A
17 16 rexralbidv z = A x + y X P C y < x F P D F y < z x + y X P C y < x F P D F y < A
18 17 rspccv z + x + y X P C y < x F P D F y < z A + x + y X P C y < x F P D F y < A
19 14 18 simpl2im C ∞Met X D ∞Met Y F J CnP K P A + x + y X P C y < x F P D F y < A
20 19 impr C ∞Met X D ∞Met Y F J CnP K P A + x + y X P C y < x F P D F y < A