Metamath Proof Explorer

Theorem metcnp2

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . The distance arguments are swapped compared to metcnp (and Munkres' metcn ) for compatibility with df-lm . Definition 1.3-3 of Kreyszig p. 20. (Contributed by NM, 4-Jun-2007) (Revised by Mario Carneiro, 13-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 metcn.2 
 |-  J = ( MetOpen ` C )
2 metcn.4 
 |-  K = ( MetOpen ` D )
3 1 2 metcnp 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) )
4 simpl1 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> C e. ( *Met ` X ) )
5 4 ad2antrr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> C e. ( *Met ` X ) )
6 simpl3 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> P e. X )
7 6 ad2antrr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> P e. X )
8 simpr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> w e. X )
9 xmetsym 
 |-  ( ( C e. ( *Met ` X ) /\ P e. X /\ w e. X ) -> ( P C w ) = ( w C P ) )
10 5 7 8 9 syl3anc 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> ( P C w ) = ( w C P ) )
11 10 breq1d 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> ( ( P C w ) < z <-> ( w C P ) < z ) )
12 simpl2 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> D e. ( *Met ` Y ) )
13 12 ad2antrr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> D e. ( *Met ` Y ) )
14 simpllr 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> F : X --> Y )
15 14 7 ffvelrnd 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> ( F ` P ) e. Y )
16 14 8 ffvelrnd 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> ( F ` w ) e. Y )
17 xmetsym 
 |-  ( ( D e. ( *Met ` Y ) /\ ( F ` P ) e. Y /\ ( F ` w ) e. Y ) -> ( ( F ` P ) D ( F ` w ) ) = ( ( F ` w ) D ( F ` P ) ) )
18 13 15 16 17 syl3anc 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> ( ( F ` P ) D ( F ` w ) ) = ( ( F ` w ) D ( F ` P ) ) )
19 18 breq1d 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> ( ( ( F ` P ) D ( F ` w ) ) < y <-> ( ( F ` w ) D ( F ` P ) ) < y ) )
20 11 19 imbi12d 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) /\ w e. X ) -> ( ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) <-> ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) )
21 20 ralbidva 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) <-> A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) )
22 21 anassrs 
 |-  ( ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) /\ z e. RR+ ) -> ( A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) <-> A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) )
23 22 rexbidva 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) /\ y e. RR+ ) -> ( E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) <-> E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) )
24 23 ralbidva 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) /\ F : X --> Y ) -> ( A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) <-> A. y e. RR+ E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) )
25 24 pm5.32da 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) ) )
26 3 25 bitrd 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) ) )