Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heicant Structured version   Unicode version

Theorem heicant 31421
Description: Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.)
Hypotheses
Ref Expression
heicant.c  |-  ( ph  ->  C  e.  ( *Met `  X ) )
heicant.d  |-  ( ph  ->  D  e.  ( *Met `  Y ) )
heicant.j  |-  ( ph  ->  ( MetOpen `  C )  e.  Comp )
heicant.x  |-  ( ph  ->  X  =/=  (/) )
heicant.y  |-  ( ph  ->  Y  =/=  (/) )
Assertion
Ref Expression
heicant  |-  ( ph  ->  ( (metUnif `  C
) Cnu (metUnif `  D )
)  =  ( (
MetOpen `  C )  Cn  ( MetOpen `  D )
) )

Proof of Theorem heicant
Dummy variables  b 
c  d  f  g  p  s  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 4399 . . . . . . . . . . 11  |-  ( d  =  y  ->  (
( ( f `  x ) D ( f `  w ) )  <  d  <->  ( (
f `  x ) D ( f `  w ) )  < 
y ) )
21imbi2d 314 . . . . . . . . . 10  |-  ( d  =  y  ->  (
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  d )  <-> 
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y ) ) )
322ralbidv 2848 . . . . . . . . 9  |-  ( d  =  y  ->  ( A. x  e.  X  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  d )  <->  A. x  e.  X  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y ) ) )
43rexbidv 2918 . . . . . . . 8  |-  ( d  =  y  ->  ( E. z  e.  RR+  A. x  e.  X  A. w  e.  X  ( (
x C w )  <  z  ->  (
( f `  x
) D ( f `
 w ) )  <  d )  <->  E. z  e.  RR+  A. x  e.  X  A. w  e.  X  ( ( x C w )  < 
z  ->  ( (
f `  x ) D ( f `  w ) )  < 
y ) ) )
54cbvralv 3034 . . . . . . 7  |-  ( A. d  e.  RR+  E. z  e.  RR+  A. x  e.  X  A. w  e.  X  ( ( x C w )  < 
z  ->  ( (
f `  x ) D ( f `  w ) )  < 
d )  <->  A. y  e.  RR+  E. z  e.  RR+  A. x  e.  X  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y ) )
6 r19.12 2933 . . . . . . . 8  |-  ( E. z  e.  RR+  A. x  e.  X  A. w  e.  X  ( (
x C w )  <  z  ->  (
( f `  x
) D ( f `
 w ) )  <  y )  ->  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( (
x C w )  <  z  ->  (
( f `  x
) D ( f `
 w ) )  <  y ) )
76ralimi 2797 . . . . . . 7  |-  ( A. y  e.  RR+  E. z  e.  RR+  A. x  e.  X  A. w  e.  X  ( ( x C w )  < 
z  ->  ( (
f `  x ) D ( f `  w ) )  < 
y )  ->  A. y  e.  RR+  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y ) )
85, 7sylbi 195 . . . . . 6  |-  ( A. d  e.  RR+  E. z  e.  RR+  A. x  e.  X  A. w  e.  X  ( ( x C w )  < 
z  ->  ( (
f `  x ) D ( f `  w ) )  < 
d )  ->  A. y  e.  RR+  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y ) )
9 rphalfcl 11290 . . . . . . . . 9  |-  ( d  e.  RR+  ->  ( d  /  2 )  e.  RR+ )
10 breq2 4399 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( d  / 
2 )  ->  (
( ( f `  x ) D ( f `  w ) )  <  y  <->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) )
1110imbi2d 314 . . . . . . . . . . . . . . 15  |-  ( y  =  ( d  / 
2 )  ->  (
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y )  <-> 
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) ) )
1211ralbidv 2843 . . . . . . . . . . . . . 14  |-  ( y  =  ( d  / 
2 )  ->  ( A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y )  <->  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) ) )
1312rexbidv 2918 . . . . . . . . . . . . 13  |-  ( y  =  ( d  / 
2 )  ->  ( E. z  e.  RR+  A. w  e.  X  ( (
x C w )  <  z  ->  (
( f `  x
) D ( f `
 w ) )  <  y )  <->  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  < 
z  ->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) ) )
1413ralbidv 2843 . . . . . . . . . . . 12  |-  ( y  =  ( d  / 
2 )  ->  ( A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( (
x C w )  <  z  ->  (
( f `  x
) D ( f `
 w ) )  <  y )  <->  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  < 
z  ->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) ) )
1514rspcva 3158 . . . . . . . . . . 11  |-  ( ( ( d  /  2
)  e.  RR+  /\  A. y  e.  RR+  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  < 
z  ->  ( (
f `  x ) D ( f `  w ) )  < 
y ) )  ->  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( (
x C w )  <  z  ->  (
( f `  x
) D ( f `
 w ) )  <  ( d  / 
2 ) ) )
16 heicant.j . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( MetOpen `  C )  e.  Comp )
1716ad3antrrr 728 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  ( MetOpen `  C )  e.  Comp )
18 heicant.c . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  C  e.  ( *Met `  X ) )
1918ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  C  e.  ( *Met `  X ) )
2019anim1i 566 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  ->  ( C  e.  ( *Met `  X )  /\  x  e.  X ) )
21 rphalfcl 11290 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  ( z  /  2 )  e.  RR+ )
2221rpxrd 11305 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( z  /  2 )  e. 
RR* )
23 eqid 2402 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( MetOpen `  C )  =  (
MetOpen `  C )
2423blopn 21295 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( z  /  2
)  e.  RR* )  ->  ( x ( ball `  C ) ( z  /  2 ) )  e.  ( MetOpen `  C
) )
25243expa 1197 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  e.  ( *Met `  X
)  /\  x  e.  X )  /\  (
z  /  2 )  e.  RR* )  ->  (
x ( ball `  C
) ( z  / 
2 ) )  e.  ( MetOpen `  C )
)
2620, 22, 25syl2an 475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  ( x
( ball `  C )
( z  /  2
) )  e.  (
MetOpen `  C ) )
2726adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  x  e.  X )  /\  z  e.  RR+ )  /\  A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  ( x
( ball `  C )
( z  /  2
) )  e.  (
MetOpen `  C ) )
2821rpgt0d 11307 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  0  < 
( z  /  2
) )
2922, 28jca 530 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  e.  RR*  /\  0  <  ( z  /  2
) ) )
30 xblcntr 21206 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( ( z  / 
2 )  e.  RR*  /\  0  <  ( z  /  2 ) ) )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
31303expa 1197 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  e.  ( *Met `  X
)  /\  x  e.  X )  /\  (
( z  /  2
)  e.  RR*  /\  0  <  ( z  /  2
) ) )  ->  x  e.  ( x
( ball `  C )
( z  /  2
) ) )
3220, 29, 31syl2an 475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
3332adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  x  e.  X )  /\  z  e.  RR+ )  /\  A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
34 opelxpi 4855 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  X  /\  ( z  /  2
)  e.  RR+ )  -> 
<. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3521, 34sylan2 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  X  /\  z  e.  RR+ )  ->  <. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3635adantll 712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  <. x ,  ( z  /  2
) >.  e.  ( X  X.  RR+ ) )
3736adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  x  e.  X )  /\  z  e.  RR+ )  /\  A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  <. x ,  ( z  /  2
) >.  e.  ( X  X.  RR+ ) )
38 rpcn 11273 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  e.  RR+  ->  z  e.  CC )
39382halvesd 10825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  +  ( z  / 
2 ) )  =  z )
4039breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  RR+  ->  ( ( x C c )  <  ( ( z  /  2 )  +  ( z  /  2
) )  <->  ( x C c )  < 
z ) )
4140imbi1d 315 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  RR+  ->  ( ( ( x C c )  <  ( ( z  /  2 )  +  ( z  / 
2 ) )  -> 
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) )  <-> 
( ( x C c )  <  z  ->  ( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) ) ) )
4241ralbidv 2843 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  RR+  ->  ( A. c  e.  X  (
( x C c )  <  ( ( z  /  2 )  +  ( z  / 
2 ) )  -> 
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) )  <->  A. c  e.  X  ( ( x C c )  <  z  ->  ( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) ) ) )
43 oveq2 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
x C c )  =  ( x C w ) )
4443breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  w  ->  (
( x C c )  <  z  <->  ( x C w )  < 
z ) )
45 fveq2 5849 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  w  ->  (
f `  c )  =  ( f `  w ) )
4645oveq2d 6294 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
( f `  x
) D ( f `
 c ) )  =  ( ( f `
 x ) D ( f `  w
) ) )
4746breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  w  ->  (
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 )  <->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) )
4844, 47imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  w  ->  (
( ( x C c )  <  z  ->  ( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) )  <-> 
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) ) )
4948cbvralv 3034 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. c  e.  X  (
( x C c )  <  z  -> 
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) )  <->  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )
5042, 49syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  ( A. c  e.  X  (
( x C c )  <  ( ( z  /  2 )  +  ( z  / 
2 ) )  -> 
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) )  <->  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) ) )
5150biimpar 483 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( z  e.  RR+  /\  A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  A. c  e.  X  ( (
x C c )  <  ( ( z  /  2 )  +  ( z  /  2
) )  ->  (
( f `  x
) D ( f `
 c ) )  <  ( d  / 
2 ) ) )
5251adantll 712 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  x  e.  X )  /\  z  e.  RR+ )  /\  A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  A. c  e.  X  ( (
x C c )  <  ( ( z  /  2 )  +  ( z  /  2
) )  ->  (
( f `  x
) D ( f `
 c ) )  <  ( d  / 
2 ) ) )
53 vex 3062 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  x  e. 
_V
54 ovex 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  /  2 )  e. 
_V
5553, 54op1std 6794 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 1st `  p
)  =  x )
5653, 54op2ndd 6795 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 2nd `  p
)  =  ( z  /  2 ) )
5755, 56oveq12d 6296 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  =  ( x ( ball `  C ) ( z  /  2 ) ) )
5857eqcomd 2410 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( x (
ball `  C )
( z  /  2
) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) ) )
5958biantrurd 506 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( A. c  e.  X  ( (
( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) )  <->  ( ( x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
6055oveq1d 6293 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) C c )  =  ( x C c ) )
6156, 56oveq12d 6296 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 2nd `  p )  +  ( 2nd `  p ) )  =  ( ( z  /  2 )  +  ( z  / 
2 ) ) )
6260, 61breq12d 4408 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( 1st `  p ) C c )  < 
( ( 2nd `  p
)  +  ( 2nd `  p ) )  <->  ( x C c )  < 
( ( z  / 
2 )  +  ( z  /  2 ) ) ) )
6355fveq2d 5853 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( f `  ( 1st `  p ) )  =  ( f `
 x ) )
6463oveq1d 6293 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( f `
 ( 1st `  p
) ) D ( f `  c ) )  =  ( ( f `  x ) D ( f `  c ) ) )
6564breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 )  <-> 
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) ) )
6662, 65imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) )  <->  ( ( x C c )  < 
( ( z  / 
2 )  +  ( z  /  2 ) )  ->  ( (
f `  x ) D ( f `  c ) )  < 
( d  /  2
) ) ) )
6766ralbidv 2843 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( A. c  e.  X  ( (
( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) )  <->  A. c  e.  X  ( ( x C c )  <  (
( z  /  2
)  +  ( z  /  2 ) )  ->  ( ( f `
 x ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )
6859, 67bitr3d 255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  <->  A. c  e.  X  ( (
x C c )  <  ( ( z  /  2 )  +  ( z  /  2
) )  ->  (
( f `  x
) D ( f `
 c ) )  <  ( d  / 
2 ) ) ) )
6968rspcev 3160 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
<. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ )  /\  A. c  e.  X  ( ( x C c )  < 
( ( z  / 
2 )  +  ( z  /  2 ) )  ->  ( (
f `  x ) D ( f `  c ) )  < 
( d  /  2
) ) )  ->  E. p  e.  ( X  X.  RR+ ) ( ( x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )
7037, 52, 69syl2anc 659 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  x  e.  X )  /\  z  e.  RR+ )  /\  A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  E. p  e.  ( X  X.  RR+ ) ( ( x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )
71 eleq2 2475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  (
x  e.  b  <->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) ) )
72 eqeq1 2406 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  (
b  =  ( ( 1st `  p ) ( ball `  C
) ( 2nd `  p
) )  <->  ( x
( ball `  C )
( z  /  2
) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) ) ) )
7372anbi1d 703 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  (
( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  <->  ( (
x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
7473rexbidv 2918 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  ( E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  /\  A. c  e.  X  ( ( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  <->  E. p  e.  ( X  X.  RR+ ) ( ( x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
7571, 74anbi12d 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  (
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  <->  ( x  e.  ( x ( ball `  C ) ( z  /  2 ) )  /\  E. p  e.  ( X  X.  RR+ ) ( ( x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
7675rspcev 3160 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( x ( ball `  C ) ( z  /  2 ) )  e.  ( MetOpen `  C
)  /\  ( x  e.  ( x ( ball `  C ) ( z  /  2 ) )  /\  E. p  e.  ( X  X.  RR+ ) ( ( x ( ball `  C
) ( z  / 
2 ) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )  ->  E. b  e.  (
MetOpen `  C ) ( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  /\  A. c  e.  X  ( ( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
7727, 33, 70, 76syl12anc 1228 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  x  e.  X )  /\  z  e.  RR+ )  /\  A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  E. b  e.  ( MetOpen `  C )
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
7877ex 432 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  ( A. w  e.  X  (
( x C w )  <  z  -> 
( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) )  ->  E. b  e.  (
MetOpen `  C ) ( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  /\  A. c  e.  X  ( ( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
7978rexlimdva 2896 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  ->  ( E. z  e.  RR+  A. w  e.  X  ( (
x C w )  <  z  ->  (
( f `  x
) D ( f `
 w ) )  <  ( d  / 
2 ) )  ->  E. b  e.  ( MetOpen
`  C ) ( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  /\  A. c  e.  X  ( ( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
8079ralimdva 2812 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  -> 
( A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) )  ->  A. x  e.  X  E. b  e.  ( MetOpen
`  C ) ( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  /\  A. c  e.  X  ( ( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
8180imp 427 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  A. x  e.  X  E. b  e.  ( MetOpen `  C )
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
8223mopnuni 21236 . . . . . . . . . . . . . . . . . 18  |-  ( C  e.  ( *Met `  X )  ->  X  =  U. ( MetOpen `  C
) )
8318, 82syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  =  U. ( MetOpen
`  C ) )
8483raleqdv 3010 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A. x  e.  X  E. b  e.  ( MetOpen `  C )
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  <->  A. x  e.  U. ( MetOpen `  C
) E. b  e.  ( MetOpen `  C )
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
8584ad3antrrr 728 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  ( A. x  e.  X  E. b  e.  ( MetOpen `  C ) ( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  /\  A. c  e.  X  ( ( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  <->  A. x  e.  U. ( MetOpen `  C
) E. b  e.  ( MetOpen `  C )
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
8681, 85mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  A. x  e.  U. ( MetOpen `  C
) E. b  e.  ( MetOpen `  C )
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
87 eqid 2402 . . . . . . . . . . . . . . 15  |-  U. ( MetOpen
`  C )  = 
U. ( MetOpen `  C
)
88 fveq2 5849 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 1st `  p )  =  ( 1st `  (
g `  b )
) )
89 fveq2 5849 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 2nd `  p )  =  ( 2nd `  (
g `  b )
) )
9088, 89oveq12d 6296 . . . . . . . . . . . . . . . . 17  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) )
9190eqeq2d 2416 . . . . . . . . . . . . . . . 16  |-  ( p  =  ( g `  b )  ->  (
b  =  ( ( 1st `  p ) ( ball `  C
) ( 2nd `  p
) )  <->  b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) ) )
9288oveq1d 6293 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) C c )  =  ( ( 1st `  ( g `  b
) ) C c ) )
9389, 89oveq12d 6296 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 2nd `  p
)  +  ( 2nd `  p ) )  =  ( ( 2nd `  (
g `  b )
)  +  ( 2nd `  ( g `  b
) ) ) )
9492, 93breq12d 4408 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  <->  ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
9588fveq2d 5853 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  =  ( g `  b )  ->  (
f `  ( 1st `  p ) )  =  ( f `  ( 1st `  ( g `  b ) ) ) )
9695oveq1d 6293 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( f `  ( 1st `  p ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) ) )
9796breq1d 4405 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  (
( ( f `  ( 1st `  p ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )
9894, 97imbi12d 318 . . . . . . . . . . . . . . . . 17  |-  ( p  =  ( g `  b )  ->  (
( ( ( 1st `  p ) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p
) )  ->  (
( f `  ( 1st `  p ) ) D ( f `  c ) )  < 
( d  /  2
) )  <->  ( (
( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )
9998ralbidv 2843 . . . . . . . . . . . . . . . 16  |-  ( p  =  ( g `  b )  ->  ( A. c  e.  X  ( ( ( 1st `  p ) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p
) )  ->  (
( f `  ( 1st `  p ) ) D ( f `  c ) )  < 
( d  /  2
) )  <->  A. c  e.  X  ( (
( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )
10091, 99anbi12d 709 . . . . . . . . . . . . . . 15  |-  ( p  =  ( g `  b )  ->  (
( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  <->  ( b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) )  /\  A. c  e.  X  ( ( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )
10187, 100cmpcovf 20184 . . . . . . . . . . . . . 14  |-  ( ( ( MetOpen `  C )  e.  Comp  /\  A. x  e.  U. ( MetOpen `  C
) E. b  e.  ( MetOpen `  C )
( x  e.  b  /\  E. p  e.  ( X  X.  RR+ ) ( b  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  /\  A. c  e.  X  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  ->  ( (
f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) )  ->  E. s  e.  ( ~P ( MetOpen `  C
)  i^i  Fin )
( U. ( MetOpen `  C )  =  U. s  /\  E. g ( g : s --> ( X  X.  RR+ )  /\  A. b  e.  s  ( b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
10217, 86, 101syl2anc 659 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) ) )  ->  E. s  e.  ( ~P ( MetOpen `  C )  i^i  Fin ) ( U. ( MetOpen
`  C )  = 
U. s  /\  E. g ( g : s --> ( X  X.  RR+ )  /\  A. b  e.  s  ( b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) )  /\  A. c  e.  X  ( ( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) )
103102ex 432 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  -> 
( A. x  e.  X  E. z  e.  RR+  A. w  e.  X  ( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  ( d  /  2 ) )  ->  E. s  e.  ( ~P ( MetOpen `  C
)  i^i  Fin )
( U. ( MetOpen `  C )  =  U. s  /\  E. g ( g : s --> ( X  X.  RR+ )  /\  A. b  e.  s  ( b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) ) ) ) )
104 inss2 3660 . . . . . . . . . . . . . . 15  |-  ( ~P ( MetOpen `  C )  i^i  Fin )  C_  Fin
105104sseli 3438 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ~P ( MetOpen
`  C )  i^i 
Fin )  ->  s  e.  Fin )
106 simpll 752 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  ph )
107106anim1i 566 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  ( ph  /\  s  e.  Fin )
)
108 frn 5720 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  g  C_  ( X  X.  RR+ ) )
109 rnss 5052 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  C_  ( X  X.  RR+ )  ->  ran  ran  g  C_  ran  ( X  X.  RR+ ) )
110108, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  ran  ( X  X.  RR+ ) )
111 rnxpss 5257 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  ( X  X.  RR+ )  C_  RR+
112110, 111syl6ss 3454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR+ )
113112adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR+ )
114 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
s  e.  Fin )
115 ffun 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( g : s --> ( X  X.  RR+ )  ->  Fun  g )
116 vex 3062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  g  e. 
_V
117116fundmen 7627 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Fun  g  ->  dom  g  ~~  g )
118117ensymd 7604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Fun  g  ->  g  ~~  dom  g )
119115, 118syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  dom  g )
120 fdm 5718 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  dom  g  =  s )
121119, 120breqtrd 4419 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  s )
122 enfii 7772 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  Fin  /\  g  ~~  s )  -> 
g  e.  Fin )
123121, 122sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  Fin  /\  g : s --> ( X  X.  RR+ ) )  -> 
g  e.  Fin )
124 rnfi 7839 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  e.  Fin  ->  ran  g  e.  Fin )
125 rnfi 7839 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  e.  Fin  ->  ran 
ran  g  e.  Fin )
126123, 124, 1253syl 18 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  Fin  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  ran  g  e.  Fin )
127114, 126sylan 469 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  e.  Fin )
128120adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =  s
)
129 eqtr 2428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  ->  X  =  U. s
)
13083, 129sylan 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =  U. s
)
131 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  X  =/=  (/) )
132131adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =/=  (/) )
133130, 132eqnetrrd 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  U. s  =/=  (/) )
134 unieq 4199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  =  (/)  ->  U. s  =  U. (/) )
135 uni0 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  U. (/)  =  (/)
136134, 135syl6eq 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  =  (/)  ->  U. s  =  (/) )
137136necon3i 2643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( U. s  =/=  (/)  ->  s  =/=  (/) )
138133, 137syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  -> 
s  =/=  (/) )
139138adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> 
s  =/=  (/) )
140128, 139eqnetrd 2696 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =/=  (/) )
141 dm0rn0 5040 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  g  =  (/)  <->  ran  g  =  (/) )
142141necon3bii 2671 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  g  =/=  (/)  <->  ran  g  =/=  (/) )
143140, 142sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  g  =/=  (/) )
144 relxp 4931 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  Rel  ( X  X.  RR+ )
145 relss 4911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ran  g  C_  ( X  X.  RR+ )  ->  ( Rel  ( X  X.  RR+ )  ->  Rel  ran  g ) )
146108, 144, 145mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  Rel  ran  g )
147 relrn0 5081 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Rel 
ran  g  ->  ( ran  g  =  (/)  <->  ran  ran  g  =  (/) ) )
148147necon3bid 2661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Rel 
ran  g  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
149146, 148syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
150149adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> 
( ran  g  =/=  (/)  <->  ran 
ran  g  =/=  (/) ) )
151143, 150mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  ran  g  =/=  (/) )
152151adantllr 717 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  =/=  (/) )
153 rpssre 11275 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR+  C_  RR
154113, 153syl6ss 3454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR )
155 gtso 9697 . . . . . . . . . . . . . . . . . . . . . . 23  |-  `'  <  Or  RR
156 fisupcl 7961 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( `'  <  Or  RR  /\  ( ran  ran  g  e.  Fin  /\  ran  ran  g  =/=  (/)  /\  ran  ran  g  C_  RR ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  ran  ran  g )
157155, 156mpan 668 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ran  ran  g  e.  Fin  /\  ran  ran  g  =/=  (/)  /\  ran  ran  g  C_  RR )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  ran  ran  g
)
158127, 152, 154, 157syl3anc 1230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  ran  ran  g
)
159113, 158sseldd 3443 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR+ )
160107, 159sylanl1 648 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR+ )
161160adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  /\  A. b  e.  s  (
b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR+ )
16283ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  X  =  U. ( MetOpen `  C )
)
163162anim1i 566 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  ->  ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s ) )
164163ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  /\  A. b  e.  s  (
b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  -> 
( X  =  U. ( MetOpen `  C )  /\  U. ( MetOpen `  C
)  =  U. s
) )
165 simpl 455 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  X  /\  w  e.  X )  ->  x  e.  X )
166129eleq2d 2472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
( x  e.  X  <->  x  e.  U. s ) )
167 eluni2 4195 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  U. s  <->  E. b  e.  s  x  e.  b )
168166, 167syl6bb 261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
( x  e.  X  <->  E. b  e.  s  x  e.  b ) )
169168biimpa 482 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( X  =  U. ( MetOpen `  C )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  x  e.  X )  ->  E. b  e.  s  x  e.  b )
170164, 165, 169syl2an 475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  /\  A. b  e.  s  ( b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  /\  ( x  e.  X  /\  w  e.  X
) )  ->  E. b  e.  s  x  e.  b )
171 nfv 1728 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ b ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )
172 nfra1 2785 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ b A. b  e.  s  ( b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )
173171, 172nfan 1956 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ b ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  /\  A. b  e.  s  ( b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )
174 nfv 1728 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ b ( x  e.  X  /\  w  e.  X
)
175173, 174nfan 1956 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ b ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  /\  A. b  e.  s  ( b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  /\  ( x  e.  X  /\  w  e.  X
) )
176 nfv 1728 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ b ( ( x C w )  <  sup ( ran  ran  g ,  RR ,  `'  <  )  ->  ( ( f `
 x ) D ( f `  w
) )  <  d
)
177 rspa 2771 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A. b  e.  s  ( b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  /\  b  e.  s )  ->  (
b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )
178 oveq2 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  x  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C x ) )
179178breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  x  ->  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  <->  ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
180 fveq2 5849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  =  x  ->  (
f `  c )  =  ( f `  x ) )
181180oveq2d 6294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  x  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) ) )
182181breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  x  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  x
) )  <  (
d  /  2 ) ) )
183179, 182imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  x  ->  (
( ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  < 
( d  /  2
) )  <->  ( (
( 1st `  (
g `  b )
) C x )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  x
) )  <  (
d  /  2 ) ) ) )
184183rspcva 3158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  X  /\  A. c  e.  X  ( ( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  ->  (
( ( 1st `  (
g `  b )
) C x )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  x
) )  <  (
d  /  2 ) ) )
185 oveq2 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  w  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C w ) )
186185breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  w  ->  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  <->  ( ( 1st `  ( g `  b
) ) C w )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
18745oveq2d 6294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  w  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 w ) ) )
188187breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  w  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) )
189186, 188imbi12d 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  w  ->  (
( ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  < 
( d  /  2
) )  <->  ( (
( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) ) )
190189rspcva 3158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( w  e.  X  /\  A. c  e.  X  ( ( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  ->  (
( ( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) )
191184, 190anim12i 564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( x  e.  X  /\  A. c  e.  X  ( ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  < 
( d  /  2
) ) )  /\  ( w  e.  X  /\  A. c  e.  X  ( ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  < 
( d  /  2
) ) ) )  ->  ( ( ( ( 1st `  (
g `  b )
) C x )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  x
) )  <  (
d  /  2 ) )  /\  ( ( ( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) ) )
192191anandirs 832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  X  /\  w  e.  X
)  /\  A. c  e.  X  ( (
( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  ->  (
( ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  x ) )  < 
( d  /  2
) )  /\  (
( ( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) ) )
193 prth 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  x ) )  < 
( d  /  2
) )  /\  (
( ( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) )  ->  (
( ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  /\  (
( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) ) )  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) )  <  ( d  / 
2 )  /\  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  w ) )  < 
( d  /  2
) ) ) )
194192, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  X  /\  w  e.  X
)  /\  A. c  e.  X  ( (
( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )  ->  (
( ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  /\  (
( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) ) )  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) )  <  ( d  / 
2 )  /\  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  w ) )  < 
( d  /  2
) ) ) )
195194adantrl 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  X  /\  w  e.  X
)  /\  ( b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) )  /\  A. c  e.  X  ( ( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  -> 
( ( ( ( 1st `  ( g `
 b ) ) C x )  < 
( ( 2nd `  (
g `  b )
)  +  ( 2nd `  ( g `  b
) ) )  /\  ( ( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) ) )  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) )  <  ( d  / 
2 )  /\  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  w ) )  < 
( d  /  2
) ) ) )
196195adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( x  e.  X  /\  w  e.  X )  /\  (
b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  /\  ( b  e.  s  /\  x  e.  b ) )  ->  (
( ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  /\  (
( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) ) )  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) )  <  ( d  / 
2 )  /\  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  w ) )  < 
( d  /  2
) ) ) )
197196adantlll 716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  (
b  =  ( ( 1st `  ( g `
 b ) ) ( ball `  C
) ( 2nd `  (
g `  b )
) )  /\  A. c  e.  X  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) ) )  /\  ( b  e.  s  /\  x  e.  b ) )  ->  (
( ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) )  /\  (
( 1st `  (
g `  b )
) C w )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) ) )  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) )  <  ( d  / 
2 )  /\  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  w ) )  < 
( d  /  2
) ) ) )
198 simpll 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  ->  (
( ph  /\  f : X --> Y )  /\  d  e.  RR+ ) )
199198anim1i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> 
( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) ) )
200199anim1i 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  ( (
( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
) )
201112, 153syl6ss 3454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR )
202201adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ran  ran  g  C_  RR )
203 0re 9626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  RR
204 rpge0 11277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  e.  RR+  ->  0  <_ 
y )
205204rgen 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  A. y  e.  RR+  0  <_  y
206 ssralv 3503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ran 
ran  g  C_  RR+  ->  ( A. y  e.  RR+  0  <_  y  ->  A. y  e.  ran  ran  g 0  <_  y ) )
207112, 205, 206mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g : s --> ( X  X.  RR+ )  ->  A. y  e.  ran  ran  g 0  <_  y )
208 breq1 4398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
209208ralbidv 2843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  0  ->  ( A. y  e.  ran  ran  g  x  <_  y  <->  A. y  e.  ran  ran  g 0  <_  y
) )
210209rspcev 3160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 0  e.  RR  /\  A. y  e.  ran  ran  g 0  <_  y
)  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
211203, 207, 210sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
212211adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
213146adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  Rel  ran  g
)
214 ffn 5714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g : s --> ( X  X.  RR+ )  ->  g  Fn  s )
215 fnfvelrn 6006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g  Fn  s  /\  b  e.  s )  ->  ( g `  b
)  e.  ran  g
)
216214, 215sylan 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ran  g )
217 2ndrn 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( Rel  ran  g  /\  ( g `  b
)  e.  ran  g
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
218213, 216, 217syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
219 infmrlb 10564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ran  ran  g  C_  RR  /\  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y  /\  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  <_  ( 2nd `  (
g `  b )
) )
220202, 212, 218, 219syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  <_ 
( 2nd `  (
g `  b )
) )
221220adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  <_  ( 2nd `  (
g `  b )
) )
222221ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  (
b  e.  s  /\  x  e.  b )
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  <_ 
( 2nd `  (
g `  b )
) )
22318ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  C  e.  ( *Met `  X ) )
224 xmetcl 21126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  w  e.  X
)  ->  ( x C w )  e. 
RR* )
2252243expb 1198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( C  e.  ( *Met `  X )  /\  ( x  e.  X  /\  w  e.  X ) )  -> 
( x C w )  e.  RR* )
226223, 225sylan 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  ( x C w )  e. 
RR* )
227226adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  (
b  e.  s  /\  x  e.  b )
)  ->  ( x C w )  e. 
RR* )
228 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  g :
s --> ( X  X.  RR+ ) )
229 simpl 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( b  e.  s  /\  x  e.  b )  ->  b  e.  s )
230 ne0i 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 2nd `  ( g `
 b ) )  e.  ran  ran  g  ->  ran  ran  g  =/=  (/) )
231218, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ran  ran  g  =/=  (/) )
232 infmrcl 10562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ran  ran  g  C_  RR  /\  ran  ran  g  =/=  (/)  /\  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR )
233202, 231, 212, 232syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR )
234233rexrd 9673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e. 
RR* )
235228, 229, 234syl2an 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  (
b  e.  s  /\  x  e.  b )
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e. 
RR* )
236 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  g : s --> ( X  X.  RR+ ) )
237236ffvelrnda 6009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  (
g `  b )  e.  ( X  X.  RR+ ) )
238 xp2nd 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g `  b )  e.  ( X  X.  RR+ )  ->  ( 2nd `  ( g `  b
) )  e.  RR+ )
239237, 238syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e.  RR+ )
240239rpxrd 11305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e. 
RR* )
241240ad2ant2r 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  (
b  e.  s  /\  x  e.  b )
)  ->  ( 2nd `  ( g `  b
) )  e.  RR* )
242 xrltletr 11413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( x C w )  e.  RR*  /\  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR*  /\  ( 2nd `  ( g `  b ) )  e. 
RR* )  ->  (
( ( x C w )  <  sup ( ran  ran  g ,  RR ,  `'  <  )  /\  sup ( ran 
ran  g ,  RR ,  `'  <  )  <_ 
( 2nd `  (
g `  b )
) )  ->  (
x C w )  <  ( 2nd `  (
g `  b )
) ) )
243227, 235, 241, 242syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  (
b  e.  s  /\  x  e.  b )
)  ->  ( (
( x C w )  <  sup ( ran  ran  g ,  RR ,  `'  <  )  /\  sup ( ran  ran  g ,  RR ,  `'  <  )  <_  ( 2nd `  (
g `  b )
) )  ->  (
x C w )  <  ( 2nd `  (
g `  b )
) ) )
244222, 243mpan2d 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  (
b  e.  s  /\  x  e.  b )
)  ->  ( (
x C w )  <  sup ( ran  ran  g ,  RR ,  `'  <  )  ->  (
x C w )  <  ( 2nd `  (
g `  b )
) ) )
245244adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) ) )  /\  ( b  e.  s  /\  x  e.  b ) )  -> 
( ( x C w )  <  sup ( ran  ran  g ,  RR ,  `'  <  )  ->  ( x C w )  <  ( 2nd `  ( g `  b ) ) ) )
24618ad6antr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) ) )  /\  ( b  e.  s  /\  x  e.  b ) )  ->  C  e.  ( *Met `  X ) )
247 simpllr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) ) )  ->  g : s --> ( X  X.  RR+ ) )
248 ffvelrn 6007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ( X  X.  RR+ )
)
249 xp1st 6814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g `  b )  e.  ( X  X.  RR+ )  ->  ( 1st `  ( g `  b
) )  e.  X
)
250248, 249syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 1st `  ( g `  b
) )  e.  X
)
251247, 229, 250syl2an 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) ) )  /\  ( b  e.  s  /\  x  e.  b ) )  -> 
( 1st `  (
g `  b )
)  e.  X )
252 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x  e.  X  /\  w  e.  X )  ->  w  e.  X )
253252ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  =  ( ( 1st `  ( g `  b
) ) ( ball `  C ) ( 2nd `  ( g `  b
) ) ) )  /\  ( b  e.  s  /\  x  e.  b ) )  ->  w  e.  X )
254 xmetcl 21126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( C  e.  ( *Met `  X )  /\  ( 1st `  (
g `  b )
)  e.  X  /\  w  e.  X )  ->  ( ( 1st `  (
g `  b )
) C w )  e.  RR* )
255246, 251, 253, 254syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g