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 e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. 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 e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> F e. ( ( J CnP K ) ` P ) )
4 simpll
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> C e. ( *Met ` X ) )
5 simplr
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> D e. ( *Met ` Y ) )
6 eqid
 |-  U. J = U. J
7 6 cnprcl
 |-  ( F e. ( ( J CnP K ) ` P ) -> P e. U. J )
8 7 adantl
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> P e. U. J )
9 1 mopnuni
 |-  ( C e. ( *Met ` X ) -> X = U. J )
10 9 ad2antrr
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> X = U. J )
11 8 10 eleqtrrd
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> P e. X )
12 1 2 metcnp
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. z e. RR+ E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < z ) ) ) )
13 4 5 11 12 syl3anc
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. z e. RR+ E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < z ) ) ) )
14 3 13 mpbid
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> ( F : X --> Y /\ A. z e. RR+ E. x e. RR+ A. y e. 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 -> ( E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < z ) <-> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) ) )
18 17 rspccv
 |-  ( A. z e. RR+ E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < z ) -> ( A e. RR+ -> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) ) )
19 14 18 simpl2im
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> ( A e. RR+ -> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) ) )
20 19 impr
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) )