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

Theorem heicant 28351
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 4293 . . . . . . . . . . 11  |-  ( d  =  y  ->  (
( ( f `  x ) D ( f `  w ) )  <  d  <->  ( (
f `  x ) D ( f `  w ) )  < 
y ) )
21imbi2d 316 . . . . . . . . . 10  |-  ( d  =  y  ->  (
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  d )  <-> 
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y ) ) )
322ralbidv 2755 . . . . . . . . 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 2734 . . . . . . . 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 2945 . . . . . . 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 2828 . . . . . . . 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 2789 . . . . . . 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 11011 . . . . . . . . 9  |-  ( d  e.  RR+  ->  ( d  /  2 )  e.  RR+ )
10 breq2 4293 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( d  / 
2 )  ->  (
( ( f `  x ) D ( f `  w ) )  <  y  <->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) )
1110imbi2d 316 . . . . . . . . . . . . . . 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 2733 . . . . . . . . . . . . . 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 2734 . . . . . . . . . . . . 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 2733 . . . . . . . . . . . 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 3068 . . . . . . . . . . 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 724 . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  C  e.  ( *Met `  X ) )
2019anim1i 565 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  ->  ( C  e.  ( *Met `  X )  /\  x  e.  X ) )
21 rphalfcl 11011 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  ( z  /  2 )  e.  RR+ )
2221rpxrd 11024 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( z  /  2 )  e. 
RR* )
23 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( MetOpen `  C )  =  (
MetOpen `  C )
2423blopn 20034 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( z  /  2
)  e.  RR* )  ->  ( x ( ball `  C ) ( z  /  2 ) )  e.  ( MetOpen `  C
) )
25243expa 1182 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  e.  ( *Met `  X
)  /\  x  e.  X )  /\  (
z  /  2 )  e.  RR* )  ->  (
x ( ball `  C
) ( z  / 
2 ) )  e.  ( MetOpen `  C )
)
2620, 22, 25syl2an 474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  ( x
( ball `  C )
( z  /  2
) )  e.  (
MetOpen `  C ) )
2726adantr 462 . . . . . . . . . . . . . . . . . . . 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 11026 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  0  < 
( z  /  2
) )
2922, 28jca 529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  e.  RR*  /\  0  <  ( z  /  2
) ) )
30 xblcntr 19945 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( ( z  / 
2 )  e.  RR*  /\  0  <  ( z  /  2 ) ) )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
31303expa 1182 . . . . . . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
3332adantr 462 . . . . . . . . . . . . . . . . . . . 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 4867 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  X  /\  ( z  /  2
)  e.  RR+ )  -> 
<. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3521, 34sylan2 471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  X  /\  z  e.  RR+ )  ->  <. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3635adantll 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  <. x ,  ( z  /  2
) >.  e.  ( X  X.  RR+ ) )
3736adantr 462 . . . . . . . . . . . . . . . . . . . . 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 10995 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  e.  RR+  ->  z  e.  CC )
39382halvesd 10566 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  +  ( z  / 
2 ) )  =  z )
4039breq2d 4301 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  RR+  ->  ( ( x C c )  <  ( ( z  /  2 )  +  ( z  /  2
) )  <->  ( x C c )  < 
z ) )
4140imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . . . 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 2733 . . . . . . . . . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
x C c )  =  ( x C w ) )
4443breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  w  ->  (
( x C c )  <  z  <->  ( x C w )  < 
z ) )
45 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  w  ->  (
f `  c )  =  ( f `  w ) )
4645oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
( f `  x
) D ( f `
 c ) )  =  ( ( f `
 x ) D ( f `  w
) ) )
4746breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  w  ->  (
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 )  <->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) )
4844, 47imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . 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 2945 . . . . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . 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 2973 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  x  e. 
_V
54 ovex 6115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  /  2 )  e. 
_V
5553, 54op1std 6586 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 1st `  p
)  =  x )
5653, 54op2ndd 6587 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 2nd `  p
)  =  ( z  /  2 ) )
5755, 56oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  =  ( x ( ball `  C ) ( z  /  2 ) ) )
5857eqcomd 2446 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( x (
ball `  C )
( z  /  2
) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) ) )
5958biantrurd 505 . . . . . . . . . . . . . . . . . . . . . . 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 6105 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) C c )  =  ( x C c ) )
6156, 56oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 2nd `  p )  +  ( 2nd `  p ) )  =  ( ( z  /  2 )  +  ( z  / 
2 ) ) )
6260, 61breq12d 4302 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( 1st `  p ) C c )  < 
( ( 2nd `  p
)  +  ( 2nd `  p ) )  <->  ( x C c )  < 
( ( z  / 
2 )  +  ( z  /  2 ) ) ) )
6355fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( f `  ( 1st `  p ) )  =  ( f `
 x ) )
6463oveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( f `
 ( 1st `  p
) ) D ( f `  c ) )  =  ( ( f `  x ) D ( f `  c ) ) )
6564breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 )  <-> 
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) ) )
6662, 65imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . 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 2733 . . . . . . . . . . . . . . . . . . . . . . 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 3070 . . . . . . . . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . . . . . . . . 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 2502 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  (
x  e.  b  <->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) ) )
72 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . . . . . . . . . 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 2734 . . . . . . . . . . . . . . . . . . . . . 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 705 . . . . . . . . . . . . . . . . . . . . 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 3070 . . . . . . . . . . . . . . . . . . . 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 1211 . . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . . . . 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 2792 . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . 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 19975 . . . . . . . . . . . . . . . . . 18  |-  ( C  e.  ( *Met `  X )  ->  X  =  U. ( MetOpen `  C
) )
8318, 82syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  =  U. ( MetOpen
`  C ) )
8483raleqdv 2921 . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . 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 2441 . . . . . . . . . . . . . . 15  |-  U. ( MetOpen
`  C )  = 
U. ( MetOpen `  C
)
88 fveq2 5688 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 1st `  p )  =  ( 1st `  (
g `  b )
) )
89 fveq2 5688 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 2nd `  p )  =  ( 2nd `  (
g `  b )
) )
9088, 89oveq12d 6108 . . . . . . . . . . . . . . . . 17  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) )
9190eqeq2d 2452 . . . . . . . . . . . . . . . 16  |-  ( p  =  ( g `  b )  ->  (
b  =  ( ( 1st `  p ) ( ball `  C
) ( 2nd `  p
) )  <->  b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) ) )
9288oveq1d 6105 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) C c )  =  ( ( 1st `  ( g `  b
) ) C c ) )
9389, 89oveq12d 6108 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 2nd `  p
)  +  ( 2nd `  p ) )  =  ( ( 2nd `  (
g `  b )
)  +  ( 2nd `  ( g `  b
) ) ) )
9492, 93breq12d 4302 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  <->  ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
9588fveq2d 5692 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  =  ( g `  b )  ->  (
f `  ( 1st `  p ) )  =  ( f `  ( 1st `  ( g `  b ) ) ) )
9695oveq1d 6105 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( f `  ( 1st `  p ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) ) )
9796breq1d 4299 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  (
( ( f `  ( 1st `  p ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )
9894, 97imbi12d 320 . . . . . . . . . . . . . . . . 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 2733 . . . . . . . . . . . . . . . 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 705 . . . . . . . . . . . . . . 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 18953 . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . 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 434 . . . . . . . . . . . 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 3568 . . . . . . . . . . . . . . 15  |-  ( ~P ( MetOpen `  C )  i^i  Fin )  C_  Fin
105104sseli 3349 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ~P ( MetOpen
`  C )  i^i 
Fin )  ->  s  e.  Fin )
106 simpll 748 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  ph )
107106anim1i 565 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  ( ph  /\  s  e.  Fin )
)
108 frn 5562 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  g  C_  ( X  X.  RR+ ) )
109 rnss 5064 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  C_  ( X  X.  RR+ )  ->  ran  ran  g  C_  ran  ( X  X.  RR+ ) )
110108, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  ran  ( X  X.  RR+ ) )
111 rnxpss 5267 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  ( X  X.  RR+ )  C_  RR+
112110, 111syl6ss 3365 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR+ )
113112adantl 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR+ )
114 simplr 749 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
s  e.  Fin )
115 ffun 5558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( g : s --> ( X  X.  RR+ )  ->  Fun  g )
116 vex 2973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  g  e. 
_V
117116fundmen 7379 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Fun  g  ->  dom  g  ~~  g )
118117ensymd 7356 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Fun  g  ->  g  ~~  dom  g )
119115, 118syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  dom  g )
120 fdm 5560 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  dom  g  =  s )
121119, 120breqtrd 4313 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  s )
122 enfii 7526 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  Fin  /\  g  ~~  s )  -> 
g  e.  Fin )
123121, 122sylan2 471 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  Fin  /\  g : s --> ( X  X.  RR+ ) )  -> 
g  e.  Fin )
124 rnfi 7592 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  e.  Fin  ->  ran  g  e.  Fin )
125 rnfi 7592 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  e.  Fin  ->  ran 
ran  g  e.  Fin )
126123, 124, 1253syl 20 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  Fin  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  ran  g  e.  Fin )
127114, 126sylan 468 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  e.  Fin )
128120adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =  s
)
129 eqtr 2458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  ->  X  =  U. s
)
13083, 129sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =  U. s
)
131 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  X  =/=  (/) )
132131adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =/=  (/) )
133130, 132eqnetrrd 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  U. s  =/=  (/) )
134 unieq 4096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  =  (/)  ->  U. s  =  U. (/) )
135 uni0 4115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  U. (/)  =  (/)
136134, 135syl6eq 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  =  (/)  ->  U. s  =  (/) )
137136necon3i 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( U. s  =/=  (/)  ->  s  =/=  (/) )
138133, 137syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  -> 
s  =/=  (/) )
139138adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> 
s  =/=  (/) )
140128, 139eqnetrd 2624 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =/=  (/) )
141 dm0rn0 5052 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  g  =  (/)  <->  ran  g  =  (/) )
142141necon3bii 2638 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  g  =/=  (/)  <->  ran  g  =/=  (/) )
143140, 142sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  g  =/=  (/) )
144 relxp 4943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  Rel  ( X  X.  RR+ )
145 relss 4923 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ran  g  C_  ( X  X.  RR+ )  ->  ( Rel  ( X  X.  RR+ )  ->  Rel  ran  g ) )
146108, 144, 145mpisyl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  Rel  ran  g )
147 relrn0 5093 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Rel 
ran  g  ->  ( ran  g  =  (/)  <->  ran  ran  g  =  (/) ) )
148147necon3bid 2641 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Rel 
ran  g  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
149146, 148syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
150149adantl 463 . . . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  =/=  (/) )
153 rpssre 10997 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR+  C_  RR
154113, 153syl6ss 3365 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR )
155 ltso 9451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  <  Or  RR
156 cnvso 5373 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (  < 
Or  RR  <->  `'  <  Or  RR )
157155, 156mpbi 208 . . . . . . . . . . . . . . . . . . . . . . 23  |-  `'  <  Or  RR
158 fisupcl 7713 . . . . . . . . . . . . . . . . . . . . . . 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 )
159157, 158mpan 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ran  ran  g  e.  Fin  /\  ran  ran  g  =/=  (/)  /\  ran  ran  g  C_  RR )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  ran  ran  g
)
160127, 152, 154, 159syl3anc 1213 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  ran  ran  g
)
161113, 160sseldd 3354 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR+ )
162107, 161sylanl1 645 . . . . . . . . . . . . . . . . . . 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+ )
163162adantr 462 . . . . . . . . . . . . . . . . . 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+ )
16483ad3antrrr 724 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  X  =  U. ( MetOpen `  C )
)
165164anim1i 565 . . . . . . . . . . . . . . . . . . . . . 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 ) )
166165ad2antrr 720 . . . . . . . . . . . . . . . . . . . . 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
) )
167 simpl 454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  X  /\  w  e.  X )  ->  x  e.  X )
168129eleq2d 2508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
( x  e.  X  <->  x  e.  U. s ) )
169 eluni2 4092 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  U. s  <->  E. b  e.  s  x  e.  b )
170168, 169syl6bb 261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
( x  e.  X  <->  E. b  e.  s  x  e.  b ) )
171170biimpa 481 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( X  =  U. ( MetOpen `  C )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  x  e.  X )  ->  E. b  e.  s  x  e.  b )
172166, 167, 171syl2an 474 . . . . . . . . . . . . . . . . . . . 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 )
173 nfv 1678 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ b ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )
174 nfra1 2764 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
175173, 174nfan 1865 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
176 nfv 1678 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ b ( x  e.  X  /\  w  e.  X
)
177175, 176nfan 1865 . . . . . . . . . . . . . . . . . . . . 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
) )
178 nfv 1678 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ b ( ( x C w )  <  sup ( ran  ran  g ,  RR ,  `'  <  )  ->  ( ( f `
 x ) D ( f `  w
) )  <  d
)
179 rsp 2774 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) ) ) )
180179imp 429 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
181 oveq2 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  x  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C x ) )
182181breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
183 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  =  x  ->  (
f `  c )  =  ( f `  x ) )
184183oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  x  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) ) )
185184breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  x  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  x
) )  <  (
d  /  2 ) ) )
186182, 185imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
187186rspcva 3068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
188 oveq2 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  w  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C w ) )
189188breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
19045oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  w  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 w ) ) )
191190breq1d 4299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  w  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) )
192189, 191imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
193192rspcva 3068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
194187, 193anim12i 563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
195194anandirs 822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
196 prth 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
197195, 196syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
198197adantrl 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
199198adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
200199adantlll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
201 simpll 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  ->  (
( ph  /\  f : X --> Y )  /\  d  e.  RR+ ) )
202201anim1i 565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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+ ) ) )
203202anim1i 565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
204112, 153syl6ss 3365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR )
205204adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ran  ran  g  C_  RR )
206 0re 9382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  RR
207 rpge0 10999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  e.  RR+  ->  0  <_ 
y )
208207rgen 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  A. y  e.  RR+  0  <_  y
209 ssralv 3413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ran 
ran  g  C_  RR+  ->  ( A. y  e.  RR+  0  <_  y  ->  A. y  e.  ran  ran  g 0  <_  y ) )
210112, 208, 209mpisyl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g : s --> ( X  X.  RR+ )  ->  A. y  e.  ran  ran  g 0  <_  y )
211 breq1 4292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
212211ralbidv 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  0  ->  ( A. y  e.  ran  ran  g  x  <_  y  <->  A. y  e.  ran  ran  g 0  <_  y
) )
213212rspcev 3070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 0  e.  RR  /\  A. y  e.  ran  ran  g 0  <_  y
)  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
214206, 210, 213sylancr 658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
215214adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
216146adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  Rel  ran  g
)
217 ffn 5556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g : s --> ( X  X.  RR+ )  ->  g  Fn  s )
218 fnfvelrn 5837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g  Fn  s  /\  b  e.  s )  ->  ( g `  b
)  e.  ran  g
)
219217, 218sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ran  g )
220 2ndrn 6621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( Rel  ran  g  /\  ( g `  b
)  e.  ran  g
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
221216, 219, 220syl2anc 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
222 infmrlb 10307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
223205, 215, 221, 222syl3anc 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  <_ 
( 2nd `  (
g `  b )
) )
224223adantll 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  <_  ( 2nd `  (
g `  b )
) )
225224ad2ant2r 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
22618ad3antrrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  C  e.  ( *Met `  X ) )
227 xmetcl 19865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  w  e.  X
)  ->  ( x C w )  e. 
RR* )
2282273expb 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( C  e.  ( *Met `  X )  /\  ( x  e.  X  /\  w  e.  X ) )  -> 
( x C w )  e.  RR* )
229226, 228sylan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  ( x C w )  e. 
RR* )
230229adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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* )
231 simplr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  g :
s --> ( X  X.  RR+ ) )
232 simpl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( b  e.  s  /\  x  e.  b )  ->  b  e.  s )
233 ne0i 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 2nd `  ( g `
 b ) )  e.  ran  ran  g  ->  ran  ran  g  =/=  (/) )
234221, 233syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ran  ran  g  =/=  (/) )
235 infmrcl 10305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
236205, 234, 215, 235syl3anc 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR )
237236rexrd 9429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e. 
RR* )
238231, 232, 237syl2an 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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* )
239 simpr 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  g : s --> ( X  X.  RR+ ) )
240239ffvelrnda 5840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  (
g `  b )  e.  ( X  X.  RR+ ) )
241 xp2nd 6606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g `  b )  e.  ( X  X.  RR+ )  ->  ( 2nd `  ( g `  b
) )  e.  RR+ )
242240, 241syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e.  RR+ )
243242rpxrd 11024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e. 
RR* )
244243ad2ant2r 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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* )
245 xrltletr 11127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
246230, 238, 244, 245syl3anc 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
247225, 246mpan2d 669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
248247adantlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
24918ad6antr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
250 simpllr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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+ ) )
251 ffvelrn 5838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ( X  X.  RR+ )
)
252 xp1st 6605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g `  b )  e.  ( X  X.  RR+ )  ->  ( 1st `  ( g `  b
) )  e.  X
)
253251, 252syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 1st `  ( g `  b
) )  e.  X
)
254250, 232, 253syl2an 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  =  ( ( 1st `  ( g