ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  metcnp3 Unicode version

Theorem metcnp3 14151
Description: Two ways to express that  F is continuous at  P for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
Hypotheses
Ref Expression
metcn.2  |-  J  =  ( MetOpen `  C )
metcn.4  |-  K  =  ( MetOpen `  D )
Assertion
Ref Expression
metcnp3  |-  ( ( 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+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y ) ) ) )
Distinct variable groups:    y, z, F   
y, J, z    y, K, z    y, X, z   
y, Y, z    y, C, z    y, D, z   
y, P, z

Proof of Theorem metcnp3
Dummy variables  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 metcn.2 . . . . 5  |-  J  =  ( MetOpen `  C )
21mopntopon 14083 . . . 4  |-  ( C  e.  ( *Met `  X )  ->  J  e.  (TopOn `  X )
)
323ad2ant1 1018 . . 3  |-  ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  ->  J  e.  (TopOn `  X )
)
4 metcn.4 . . . . 5  |-  K  =  ( MetOpen `  D )
54mopnval 14082 . . . 4  |-  ( D  e.  ( *Met `  Y )  ->  K  =  ( topGen `  ran  ( ball `  D )
) )
653ad2ant2 1019 . . 3  |-  ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  ->  K  =  ( topGen `  ran  ( ball `  D )
) )
74mopntopon 14083 . . . 4  |-  ( D  e.  ( *Met `  Y )  ->  K  e.  (TopOn `  Y )
)
873ad2ant2 1019 . . 3  |-  ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  ->  K  e.  (TopOn `  Y )
)
9 simp3 999 . . 3  |-  ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  ->  P  e.  X )
103, 6, 8, 9tgcnp 13849 . 2  |-  ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  ->  ( F  e.  ( ( J  CnP  K ) `  P )  <->  ( F : X --> Y  /\  A. u  e.  ran  ( ball `  D ) ( ( F `  P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) ) ) )
11 simpll2 1037 . . . . . . . 8  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  ->  D  e.  ( *Met `  Y ) )
12 simplr 528 . . . . . . . . 9  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  ->  F : X --> Y )
13 simpll3 1038 . . . . . . . . 9  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  ->  P  e.  X )
1412, 13ffvelcdmd 5655 . . . . . . . 8  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( F `  P
)  e.  Y )
15 simpr 110 . . . . . . . 8  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
y  e.  RR+ )
16 blcntr 14056 . . . . . . . 8  |-  ( ( D  e.  ( *Met `  Y )  /\  ( F `  P )  e.  Y  /\  y  e.  RR+ )  ->  ( F `  P
)  e.  ( ( F `  P ) ( ball `  D
) y ) )
1711, 14, 15, 16syl3anc 1238 . . . . . . 7  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( F `  P
)  e.  ( ( F `  P ) ( ball `  D
) y ) )
18 rpxr 9664 . . . . . . . . . 10  |-  ( y  e.  RR+  ->  y  e. 
RR* )
1918adantl 277 . . . . . . . . 9  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
y  e.  RR* )
20 blelrn 14060 . . . . . . . . 9  |-  ( ( D  e.  ( *Met `  Y )  /\  ( F `  P )  e.  Y  /\  y  e.  RR* )  ->  ( ( F `  P ) ( ball `  D ) y )  e.  ran  ( ball `  D ) )
2111, 14, 19, 20syl3anc 1238 . . . . . . . 8  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( ( F `  P ) ( ball `  D ) y )  e.  ran  ( ball `  D ) )
22 eleq2 2241 . . . . . . . . . 10  |-  ( u  =  ( ( F `
 P ) (
ball `  D )
y )  ->  (
( F `  P
)  e.  u  <->  ( F `  P )  e.  ( ( F `  P
) ( ball `  D
) y ) ) )
23 sseq2 3181 . . . . . . . . . . . 12  |-  ( u  =  ( ( F `
 P ) (
ball `  D )
y )  ->  (
( F " v
)  C_  u  <->  ( F " v )  C_  (
( F `  P
) ( ball `  D
) y ) ) )
2423anbi2d 464 . . . . . . . . . . 11  |-  ( u  =  ( ( F `
 P ) (
ball `  D )
y )  ->  (
( P  e.  v  /\  ( F "
v )  C_  u
)  <->  ( P  e.  v  /\  ( F
" v )  C_  ( ( F `  P ) ( ball `  D ) y ) ) ) )
2524rexbidv 2478 . . . . . . . . . 10  |-  ( u  =  ( ( F `
 P ) (
ball `  D )
y )  ->  ( E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )  <->  E. v  e.  J  ( P  e.  v  /\  ( F " v ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) ) )
2622, 25imbi12d 234 . . . . . . . . 9  |-  ( u  =  ( ( F `
 P ) (
ball `  D )
y )  ->  (
( ( F `  P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )
)  <->  ( ( F `
 P )  e.  ( ( F `  P ) ( ball `  D ) y )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  ( ( F `  P )
( ball `  D )
y ) ) ) ) )
2726rspcv 2839 . . . . . . . 8  |-  ( ( ( F `  P
) ( ball `  D
) y )  e. 
ran  ( ball `  D
)  ->  ( A. u  e.  ran  ( ball `  D ) ( ( F `  P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) )  -> 
( ( F `  P )  e.  ( ( F `  P
) ( ball `  D
) y )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  ( ( F `  P )
( ball `  D )
y ) ) ) ) )
2821, 27syl 14 . . . . . . 7  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( A. u  e. 
ran  ( ball `  D
) ( ( F `
 P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) )  -> 
( ( F `  P )  e.  ( ( F `  P
) ( ball `  D
) y )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  ( ( F `  P )
( ball `  D )
y ) ) ) ) )
2917, 28mpid 42 . . . . . 6  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( A. u  e. 
ran  ( ball `  D
) ( ( F `
 P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  ( ( F `  P )
( ball `  D )
y ) ) ) )
30 simpl1 1000 . . . . . . . . . . . 12  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  ->  C  e.  ( *Met `  X ) )
3130ad2antrr 488 . . . . . . . . . . 11  |-  ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  ( y  e.  RR+  /\  v  e.  J ) )  /\  P  e.  v )  ->  C  e.  ( *Met `  X ) )
32 simplrr 536 . . . . . . . . . . 11  |-  ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  ( y  e.  RR+  /\  v  e.  J ) )  /\  P  e.  v )  ->  v  e.  J )
33 simpr 110 . . . . . . . . . . 11  |-  ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  ( y  e.  RR+  /\  v  e.  J ) )  /\  P  e.  v )  ->  P  e.  v )
341mopni2 14123 . . . . . . . . . . 11  |-  ( ( C  e.  ( *Met `  X )  /\  v  e.  J  /\  P  e.  v
)  ->  E. z  e.  RR+  ( P (
ball `  C )
z )  C_  v
)
3531, 32, 33, 34syl3anc 1238 . . . . . . . . . 10  |-  ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  ( y  e.  RR+  /\  v  e.  J ) )  /\  P  e.  v )  ->  E. z  e.  RR+  ( P (
ball `  C )
z )  C_  v
)
36 sstr2 3164 . . . . . . . . . . . 12  |-  ( ( F " ( P ( ball `  C
) z ) ) 
C_  ( F "
v )  ->  (
( F " v
)  C_  ( ( F `  P )
( ball `  D )
y )  ->  ( F " ( P (
ball `  C )
z ) )  C_  ( ( F `  P ) ( ball `  D ) y ) ) )
37 imass2 5006 . . . . . . . . . . . 12  |-  ( ( P ( ball `  C
) z )  C_  v  ->  ( F "
( P ( ball `  C ) z ) )  C_  ( F " v ) )
3836, 37syl11 31 . . . . . . . . . . 11  |-  ( ( F " v ) 
C_  ( ( F `
 P ) (
ball `  D )
y )  ->  (
( P ( ball `  C ) z ) 
C_  v  ->  ( F " ( P (
ball `  C )
z ) )  C_  ( ( F `  P ) ( ball `  D ) y ) ) )
3938reximdv 2578 . . . . . . . . . 10  |-  ( ( F " v ) 
C_  ( ( F `
 P ) (
ball `  D )
y )  ->  ( E. z  e.  RR+  ( P ( ball `  C
) z )  C_  v  ->  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )
4035, 39syl5com 29 . . . . . . . . 9  |-  ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  ( y  e.  RR+  /\  v  e.  J ) )  /\  P  e.  v )  ->  (
( F " v
)  C_  ( ( F `  P )
( ball `  D )
y )  ->  E. z  e.  RR+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y ) ) )
4140expimpd 363 . . . . . . . 8  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  ( y  e.  RR+  /\  v  e.  J ) )  ->  ( ( P  e.  v  /\  ( F " v ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) )  ->  E. z  e.  RR+  ( F " ( P (
ball `  C )
z ) )  C_  ( ( F `  P ) ( ball `  D ) y ) ) )
4241expr 375 . . . . . . 7  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( v  e.  J  ->  ( ( P  e.  v  /\  ( F
" v )  C_  ( ( F `  P ) ( ball `  D ) y ) )  ->  E. z  e.  RR+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y ) ) ) )
4342rexlimdv 2593 . . . . . 6  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( E. v  e.  J  ( P  e.  v  /\  ( F
" v )  C_  ( ( F `  P ) ( ball `  D ) y ) )  ->  E. z  e.  RR+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y ) ) )
4429, 43syld 45 . . . . 5  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( A. u  e. 
ran  ( ball `  D
) ( ( F `
 P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) )  ->  E. z  e.  RR+  ( F " ( P (
ball `  C )
z ) )  C_  ( ( F `  P ) ( ball `  D ) y ) ) )
4544ralrimdva 2557 . . . 4  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( A. u  e. 
ran  ( ball `  D
) ( ( F `
 P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) )  ->  A. y  e.  RR+  E. z  e.  RR+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y ) ) )
46 simpl2 1001 . . . . . . . . 9  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  ->  D  e.  ( *Met `  Y ) )
47 blss 14068 . . . . . . . . . 10  |-  ( ( D  e.  ( *Met `  Y )  /\  u  e.  ran  ( ball `  D )  /\  ( F `  P
)  e.  u )  ->  E. y  e.  RR+  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )
48473expib 1206 . . . . . . . . 9  |-  ( D  e.  ( *Met `  Y )  ->  (
( u  e.  ran  ( ball `  D )  /\  ( F `  P
)  e.  u )  ->  E. y  e.  RR+  ( ( F `  P ) ( ball `  D ) y ) 
C_  u ) )
4946, 48syl 14 . . . . . . . 8  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( ( u  e. 
ran  ( ball `  D
)  /\  ( F `  P )  e.  u
)  ->  E. y  e.  RR+  ( ( F `
 P ) (
ball `  D )
y )  C_  u
) )
50 r19.29r 2615 . . . . . . . . . 10  |-  ( ( E. y  e.  RR+  ( ( F `  P ) ( ball `  D ) y ) 
C_  u  /\  A. y  e.  RR+  E. z  e.  RR+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y ) )  ->  E. y  e.  RR+  (
( ( F `  P ) ( ball `  D ) y ) 
C_  u  /\  E. z  e.  RR+  ( F
" ( P (
ball `  C )
z ) )  C_  ( ( F `  P ) ( ball `  D ) y ) ) )
5130ad3antrrr 492 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  C  e.  ( *Met `  X
) )
5213ad2antrr 488 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  P  e.  X
)
53 rpxr 9664 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  RR+  ->  z  e. 
RR* )
5453ad2antrl 490 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  z  e.  RR* )
551blopn 14130 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  ( *Met `  X )  /\  P  e.  X  /\  z  e.  RR* )  ->  ( P ( ball `  C ) z )  e.  J )
5651, 52, 54, 55syl3anc 1238 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  ( P (
ball `  C )
z )  e.  J
)
57 simprl 529 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  z  e.  RR+ )
58 blcntr 14056 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  ( *Met `  X )  /\  P  e.  X  /\  z  e.  RR+ )  ->  P  e.  ( P ( ball `  C
) z ) )
5951, 52, 57, 58syl3anc 1238 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  P  e.  ( P ( ball `  C
) z ) )
60 sstr 3165 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y )  /\  (
( F `  P
) ( ball `  D
) y )  C_  u )  ->  ( F " ( P (
ball `  C )
z ) )  C_  u )
6160ad2ant2l 508 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) )  /\  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u ) )  ->  ( F "
( P ( ball `  C ) z ) )  C_  u )
6261ancoms 268 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  ( F "
( P ( ball `  C ) z ) )  C_  u )
63 eleq2 2241 . . . . . . . . . . . . . . . . 17  |-  ( v  =  ( P (
ball `  C )
z )  ->  ( P  e.  v  <->  P  e.  ( P ( ball `  C
) z ) ) )
64 imaeq2 4968 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  ( P (
ball `  C )
z )  ->  ( F " v )  =  ( F " ( P ( ball `  C
) z ) ) )
6564sseq1d 3186 . . . . . . . . . . . . . . . . 17  |-  ( v  =  ( P (
ball `  C )
z )  ->  (
( F " v
)  C_  u  <->  ( F " ( P ( ball `  C ) z ) )  C_  u )
)
6663, 65anbi12d 473 . . . . . . . . . . . . . . . 16  |-  ( v  =  ( P (
ball `  C )
z )  ->  (
( P  e.  v  /\  ( F "
v )  C_  u
)  <->  ( P  e.  ( P ( ball `  C ) z )  /\  ( F "
( P ( ball `  C ) z ) )  C_  u )
) )
6766rspcev 2843 . . . . . . . . . . . . . . 15  |-  ( ( ( P ( ball `  C ) z )  e.  J  /\  ( P  e.  ( P
( ball `  C )
z )  /\  ( F " ( P (
ball `  C )
z ) )  C_  u ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )
)
6856, 59, 62, 67syl12anc 1236 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  ( z  e.  RR+  /\  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )
)
6968expr 375 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  /\  z  e.  RR+ )  -> 
( ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) )
7069rexlimdva 2594 . . . . . . . . . . . 12  |-  ( ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  /\  ( ( F `  P ) ( ball `  D ) y ) 
C_  u )  -> 
( E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) )
7170expimpd 363 . . . . . . . . . . 11  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y )  /\  P  e.  X )  /\  F : X --> Y )  /\  y  e.  RR+ )  -> 
( ( ( ( F `  P ) ( ball `  D
) y )  C_  u  /\  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )
) )
7271rexlimdva 2594 . . . . . . . . . 10  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( E. y  e.  RR+  ( ( ( F `
 P ) (
ball `  D )
y )  C_  u  /\  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )
) )
7350, 72syl5 32 . . . . . . . . 9  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( ( E. y  e.  RR+  ( ( F `
 P ) (
ball `  D )
y )  C_  u  /\  A. y  e.  RR+  E. z  e.  RR+  ( F " ( P (
ball `  C )
z ) )  C_  ( ( F `  P ) ( ball `  D ) y ) )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) )
7473expd 258 . . . . . . . 8  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( E. y  e.  RR+  ( ( F `  P ) ( ball `  D ) y ) 
C_  u  ->  ( A. y  e.  RR+  E. z  e.  RR+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) ) )
7549, 74syld 45 . . . . . . 7  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( ( u  e. 
ran  ( ball `  D
)  /\  ( F `  P )  e.  u
)  ->  ( A. y  e.  RR+  E. z  e.  RR+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) ) )
7675com23 78 . . . . . 6  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( A. y  e.  RR+  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y )  ->  (
( u  e.  ran  ( ball `  D )  /\  ( F `  P
)  e.  u )  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )
) ) )
7776exp4a 366 . . . . 5  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( A. y  e.  RR+  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y )  ->  (
u  e.  ran  ( ball `  D )  -> 
( ( F `  P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v
)  C_  u )
) ) ) )
7877ralrimdv 2556 . . . 4  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( A. y  e.  RR+  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y )  ->  A. u  e.  ran  ( ball `  D
) ( ( F `
 P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) ) )
7945, 78impbid 129 . . 3  |-  ( ( ( C  e.  ( *Met `  X
)  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  /\  F : X --> Y )  -> 
( A. u  e. 
ran  ( ball `  D
) ( ( F `
 P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) )  <->  A. y  e.  RR+  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) )
8079pm5.32da 452 . 2  |-  ( ( C  e.  ( *Met `  X )  /\  D  e.  ( *Met `  Y
)  /\  P  e.  X )  ->  (
( F : X --> Y  /\  A. u  e. 
ran  ( ball `  D
) ( ( F `
 P )  e.  u  ->  E. v  e.  J  ( P  e.  v  /\  ( F " v )  C_  u ) ) )  <-> 
( F : X --> Y  /\  A. y  e.  RR+  E. z  e.  RR+  ( F " ( P ( ball `  C
) z ) ) 
C_  ( ( F `
 P ) (
ball `  D )
y ) ) ) )
8110, 80bitrd 188 1  |-  ( ( 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+  ( F "
( P ( ball `  C ) z ) )  C_  ( ( F `  P )
( ball `  D )
y ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    /\ w3a 978    = wceq 1353    e. wcel 2148   A.wral 2455   E.wrex 2456    C_ wss 3131   ran crn 4629   "cima 4631   -->wf 5214   ` cfv 5218  (class class class)co 5878   RR*cxr 7994   RR+crp 9656   topGenctg 12709   *Metcxmet 13580   ballcbl 13582   MetOpencmopn 13585  TopOnctopon 13650    CnP ccnp 13826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7905  ax-resscn 7906  ax-1cn 7907  ax-1re 7908  ax-icn 7909  ax-addcl 7910  ax-addrcl 7911  ax-mulcl 7912  ax-mulrcl 7913  ax-addcom 7914  ax-mulcom 7915  ax-addass 7916  ax-mulass 7917  ax-distr 7918  ax-i2m1 7919  ax-0lt1 7920  ax-1rid 7921  ax-0id 7922  ax-rnegex 7923  ax-precex 7924  ax-cnre 7925  ax-pre-ltirr 7926  ax-pre-ltwlin 7927  ax-pre-lttrn 7928  ax-pre-apti 7929  ax-pre-ltadd 7930  ax-pre-mulgt0 7931  ax-pre-mulext 7932  ax-arch 7933  ax-caucvg 7934
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5834  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145  df-recs 6309  df-frec 6395  df-map 6653  df-sup 6986  df-inf 6987  df-pnf 7997  df-mnf 7998  df-xr 7999  df-ltxr 8000  df-le 8001  df-sub 8133  df-neg 8134  df-reap 8535  df-ap 8542  df-div 8633  df-inn 8923  df-2 8981  df-3 8982  df-4 8983  df-n0 9180  df-z 9257  df-uz 9532  df-q 9623  df-rp 9657  df-xneg 9775  df-xadd 9776  df-seqfrec 10449  df-exp 10523  df-cj 10854  df-re 10855  df-im 10856  df-rsqrt 11010  df-abs 11011  df-topgen 12715  df-psmet 13587  df-xmet 13588  df-bl 13590  df-mopn 13591  df-top 13638  df-topon 13651  df-bases 13683  df-cnp 13829
This theorem is referenced by:  metcnp  14152
  Copyright terms: Public domain W3C validator