Metamath Proof Explorer

Theorem metcn

Description: Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of Munkres p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D . (Contributed by NM, 15-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses metcn.2 
|- J = ( MetOpen ` C )
metcn.4 
|- K = ( MetOpen ` D )
Assertion metcn 
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )

Proof

Step Hyp Ref Expression
1 metcn.2 
 |-  J = ( MetOpen ` C )
2 metcn.4 
 |-  K = ( MetOpen ` D )
3 1 mopntopon 
 |-  ( C e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
4 2 mopntopon 
 |-  ( D e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) )
5 cncnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
6 3 4 5 syl2an 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
7 simplr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F : X --> Y ) /\ x e. X ) -> F : X --> Y )
8 1 2 metcnp 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )
9 8 ad4ant124 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F : X --> Y ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )
10 7 9 mpbirand 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F : X --> Y ) /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) )
11 10 ralbidva 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ F : X --> Y ) -> ( A. x e. X F e. ( ( J CnP K ) ` x ) <-> A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) )
12 11 pm5.32da 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) <-> ( F : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )
13 6 12 bitrd 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )