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

Theorem heicant 31933
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.) (Proof shortened by AV, 27-Sep-2020.)
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 4425 . . . . . . . . . . 11  |-  ( d  =  y  ->  (
( ( f `  x ) D ( f `  w ) )  <  d  <->  ( (
f `  x ) D ( f `  w ) )  < 
y ) )
21imbi2d 318 . . . . . . . . . 10  |-  ( d  =  y  ->  (
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  d )  <-> 
( ( x C w )  <  z  ->  ( ( f `  x ) D ( f `  w ) )  <  y ) ) )
322ralbidv 2870 . . . . . . . . 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 2940 . . . . . . . 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 3056 . . . . . . 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 2955 . . . . . . . 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 2819 . . . . . . 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 199 . . . . . 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 11329 . . . . . . . . 9  |-  ( d  e.  RR+  ->  ( d  /  2 )  e.  RR+ )
10 breq2 4425 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( d  / 
2 )  ->  (
( ( f `  x ) D ( f `  w ) )  <  y  <->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) )
1110imbi2d 318 . . . . . . . . . . . . . . 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 2865 . . . . . . . . . . . . . 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 2940 . . . . . . . . . . . . 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 2865 . . . . . . . . . . . 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 3181 . . . . . . . . . . 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 735 . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  C  e.  ( *Met `  X ) )
2019anim1i 571 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  ->  ( C  e.  ( *Met `  X )  /\  x  e.  X ) )
21 rphalfcl 11329 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  ( z  /  2 )  e.  RR+ )
2221rpxrd 11344 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( z  /  2 )  e. 
RR* )
23 eqid 2423 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( MetOpen `  C )  =  (
MetOpen `  C )
2423blopn 21507 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( z  /  2
)  e.  RR* )  ->  ( x ( ball `  C ) ( z  /  2 ) )  e.  ( MetOpen `  C
) )
25243expa 1206 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  e.  ( *Met `  X
)  /\  x  e.  X )  /\  (
z  /  2 )  e.  RR* )  ->  (
x ( ball `  C
) ( z  / 
2 ) )  e.  ( MetOpen `  C )
)
2620, 22, 25syl2an 480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  ( x
( ball `  C )
( z  /  2
) )  e.  (
MetOpen `  C ) )
2726adantr 467 . . . . . . . . . . . . . . . . . . . 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 11346 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  0  < 
( z  /  2
) )
2922, 28jca 535 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  e.  RR*  /\  0  <  ( z  /  2
) ) )
30 xblcntr 21418 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( ( z  / 
2 )  e.  RR*  /\  0  <  ( z  /  2 ) ) )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
31303expa 1206 . . . . . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
3332adantr 467 . . . . . . . . . . . . . . . . . . . 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 4883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  X  /\  ( z  /  2
)  e.  RR+ )  -> 
<. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3521, 34sylan2 477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  X  /\  z  e.  RR+ )  ->  <. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3635ad4ant23 1236 . . . . . . . . . . . . . . . . . . . . 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+ ) )
37 rpcn 11312 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  e.  RR+  ->  z  e.  CC )
38372halvesd 10860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  +  ( z  / 
2 ) )  =  z )
3938breq2d 4433 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  RR+  ->  ( ( x C c )  <  ( ( z  /  2 )  +  ( z  /  2
) )  <->  ( x C c )  < 
z ) )
4039imbi1d 319 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
4140ralbidv 2865 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
42 oveq2 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
x C c )  =  ( x C w ) )
4342breq1d 4431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  w  ->  (
( x C c )  <  z  <->  ( x C w )  < 
z ) )
44 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  w  ->  (
f `  c )  =  ( f `  w ) )
4544oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
( f `  x
) D ( f `
 c ) )  =  ( ( f `
 x ) D ( f `  w
) ) )
4645breq1d 4431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  w  ->  (
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 )  <->  ( (
f `  x ) D ( f `  w ) )  < 
( d  /  2
) ) )
4743, 46imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
4847cbvralv 3056 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
4941, 48syl6bb 265 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
5049biimpar 488 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
5150adantll 719 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
52 vex 3085 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  x  e. 
_V
53 ovex 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  /  2 )  e. 
_V
5452, 53op1std 6815 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 1st `  p
)  =  x )
5552, 53op2ndd 6816 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 2nd `  p
)  =  ( z  /  2 ) )
5654, 55oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  =  ( x ( ball `  C ) ( z  /  2 ) ) )
5756eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( x (
ball `  C )
( z  /  2
) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) ) )
5857biantrurd 511 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
5954oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) C c )  =  ( x C c ) )
6055, 55oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 2nd `  p )  +  ( 2nd `  p ) )  =  ( ( z  /  2 )  +  ( z  / 
2 ) ) )
6159, 60breq12d 4434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( 1st `  p ) C c )  < 
( ( 2nd `  p
)  +  ( 2nd `  p ) )  <->  ( x C c )  < 
( ( z  / 
2 )  +  ( z  /  2 ) ) ) )
6254fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( f `  ( 1st `  p ) )  =  ( f `
 x ) )
6362oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( f `
 ( 1st `  p
) ) D ( f `  c ) )  =  ( ( f `  x ) D ( f `  c ) ) )
6463breq1d 4431 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( f `  ( 1st `  p ) ) D ( f `  c
) )  <  (
d  /  2 )  <-> 
( ( f `  x ) D ( f `  c ) )  <  ( d  /  2 ) ) )
6561, 64imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
6665ralbidv 2865 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
6758, 66bitr3d 259 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
6867rspcev 3183 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
6936, 51, 68syl2anc 666 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
70 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  (
x  e.  b  <->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) ) )
71 eqeq1 2427 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
7271anbi1d 710 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
7372rexbidv 2940 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
7470, 73anbi12d 716 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
7574rspcev 3183 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
7627, 33, 69, 75syl12anc 1263 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
7776ex 436 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
7877rexlimdva 2918 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
7978ralimdva 2834 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
8079imp 431 . . . . . . . . . . . . . . 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 ) ) ) ) )
8123mopnuni 21448 . . . . . . . . . . . . . . . . . 18  |-  ( C  e.  ( *Met `  X )  ->  X  =  U. ( MetOpen `  C
) )
8218, 81syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  =  U. ( MetOpen
`  C ) )
8382raleqdv 3032 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
8483ad3antrrr 735 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
8580, 84mpbid 214 . . . . . . . . . . . . . 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 ) ) ) ) )
86 eqid 2423 . . . . . . . . . . . . . . 15  |-  U. ( MetOpen
`  C )  = 
U. ( MetOpen `  C
)
87 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 1st `  p )  =  ( 1st `  (
g `  b )
) )
88 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 2nd `  p )  =  ( 2nd `  (
g `  b )
) )
8987, 88oveq12d 6321 . . . . . . . . . . . . . . . . 17  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) )
9089eqeq2d 2437 . . . . . . . . . . . . . . . 16  |-  ( p  =  ( g `  b )  ->  (
b  =  ( ( 1st `  p ) ( ball `  C
) ( 2nd `  p
) )  <->  b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) ) )
9187oveq1d 6318 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) C c )  =  ( ( 1st `  ( g `  b
) ) C c ) )
9288, 88oveq12d 6321 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 2nd `  p
)  +  ( 2nd `  p ) )  =  ( ( 2nd `  (
g `  b )
)  +  ( 2nd `  ( g `  b
) ) ) )
9391, 92breq12d 4434 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  <->  ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
9487fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  =  ( g `  b )  ->  (
f `  ( 1st `  p ) )  =  ( f `  ( 1st `  ( g `  b ) ) ) )
9594oveq1d 6318 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( f `  ( 1st `  p ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) ) )
9695breq1d 4431 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  (
( ( f `  ( 1st `  p ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  c
) )  <  (
d  /  2 ) ) )
9793, 96imbi12d 322 . . . . . . . . . . . . . . . . 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 ) ) ) )
9897ralbidv 2865 . . . . . . . . . . . . . . . 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 ) ) ) )
9990, 98anbi12d 716 . . . . . . . . . . . . . . 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 ) ) ) ) )
10086, 99cmpcovf 20398 . . . . . . . . . . . . . 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 ) ) ) ) ) )
10117, 85, 100syl2anc 666 . . . . . . . . . . . . 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 ) ) ) ) ) )
102101ex 436 . . . . . . . . . . . 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 ) ) ) ) ) ) )
103 elinel2 3653 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ~P ( MetOpen
`  C )  i^i 
Fin )  ->  s  e.  Fin )
104 simpll 759 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  ph )
105104anim1i 571 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  ( ph  /\  s  e.  Fin )
)
106 frn 5750 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  g  C_  ( X  X.  RR+ ) )
107 rnss 5080 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  C_  ( X  X.  RR+ )  ->  ran  ran  g  C_  ran  ( X  X.  RR+ ) )
108106, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  ran  ( X  X.  RR+ ) )
109 rnxpss 5286 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  ( X  X.  RR+ )  C_  RR+
110108, 109syl6ss 3477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR+ )
111110adantl 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR+ )
112 simplr 761 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
s  e.  Fin )
113 ffun 5746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( g : s --> ( X  X.  RR+ )  ->  Fun  g )
114 vex 3085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  g  e. 
_V
115114fundmen 7648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Fun  g  ->  dom  g  ~~  g )
116115ensymd 7625 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Fun  g  ->  g  ~~  dom  g )
117113, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  dom  g )
118 fdm 5748 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  dom  g  =  s )
119117, 118breqtrd 4446 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  s )
120 enfii 7793 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  Fin  /\  g  ~~  s )  -> 
g  e.  Fin )
121119, 120sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  Fin  /\  g : s --> ( X  X.  RR+ ) )  -> 
g  e.  Fin )
122 rnfi 7861 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  e.  Fin  ->  ran  g  e.  Fin )
123 rnfi 7861 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ran  g  e.  Fin  ->  ran 
ran  g  e.  Fin )
124121, 122, 1233syl 18 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  Fin  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  ran  g  e.  Fin )
125112, 124sylan 474 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  e.  Fin )
126118adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =  s
)
127 eqtr 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  ->  X  =  U. s
)
12882, 127sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =  U. s
)
129 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  X  =/=  (/) )
130129adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =/=  (/) )
131128, 130eqnetrrd 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  U. s  =/=  (/) )
132 unieq 4225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  =  (/)  ->  U. s  =  U. (/) )
133 uni0 4244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  U. (/)  =  (/)
134132, 133syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  =  (/)  ->  U. s  =  (/) )
135134necon3i 2665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( U. s  =/=  (/)  ->  s  =/=  (/) )
136131, 135syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  -> 
s  =/=  (/) )
137136adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> 
s  =/=  (/) )
138126, 137eqnetrd 2718 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =/=  (/) )
139 dm0rn0 5068 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  g  =  (/)  <->  ran  g  =  (/) )
140139necon3bii 2693 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  g  =/=  (/)  <->  ran  g  =/=  (/) )
141138, 140sylib 200 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  g  =/=  (/) )
142 relxp 4959 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  Rel  ( X  X.  RR+ )
143 relss 4939 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ran  g  C_  ( X  X.  RR+ )  ->  ( Rel  ( X  X.  RR+ )  ->  Rel  ran  g ) )
144106, 142, 143mpisyl 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  Rel  ran  g )
145 relrn0 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Rel 
ran  g  ->  ( ran  g  =  (/)  <->  ran  ran  g  =  (/) ) )
146145necon3bid 2683 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Rel 
ran  g  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
147144, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
148147adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> 
( ran  g  =/=  (/)  <->  ran 
ran  g  =/=  (/) ) )
149141, 148mpbid 214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  ran  g  =/=  (/) )
150149adantllr 724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  =/=  (/) )
151 rpssre 11314 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR+  C_  RR
152111, 151syl6ss 3477 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR )
153 ltso 9716 . . . . . . . . . . . . . . . . . . . . . . 23  |-  <  Or  RR
154 fiinfcl 8021 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (  <  Or  RR  /\  ( ran  ran  g  e.  Fin  /\  ran  ran  g  =/=  (/)  /\  ran  ran  g  C_  RR ) )  -> inf ( ran  ran  g ,  RR ,  <  )  e.  ran  ran  g )
155153, 154mpan 675 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ran  ran  g  e.  Fin  /\  ran  ran  g  =/=  (/)  /\  ran  ran  g  C_  RR )  -> inf ( ran  ran  g ,  RR ,  <  )  e. 
ran  ran  g )
156125, 150, 152, 155syl3anc 1265 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  -> inf ( ran 
ran  g ,  RR ,  <  )  e.  ran  ran  g )
157111, 156sseldd 3466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  -> inf ( ran 
ran  g ,  RR ,  <  )  e.  RR+ )
158105, 157sylanl1 655 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> inf ( ran  ran  g ,  RR ,  <  )  e.  RR+ )
159158adantr 467 . . . . . . . . . . . . . . . . . 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 ) ) ) )  -> inf ( ran  ran  g ,  RR ,  <  )  e.  RR+ )
16082ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  X  =  U. ( MetOpen `  C )
)
161160anim1i 571 . . . . . . . . . . . . . . . . . . . . . 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 ) )
162161ad2antrr 731 . . . . . . . . . . . . . . . . . . . . 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
) )
163 simpl 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  X  /\  w  e.  X )  ->  x  e.  X )
164127eleq2d 2493 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
( x  e.  X  <->  x  e.  U. s ) )
165 eluni2 4221 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  U. s  <->  E. b  e.  s  x  e.  b )
166164, 165syl6bb 265 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
( x  e.  X  <->  E. b  e.  s  x  e.  b ) )
167166biimpa 487 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( X  =  U. ( MetOpen `  C )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  x  e.  X )  ->  E. b  e.  s  x  e.  b )
168162, 163, 167syl2an 480 . . . . . . . . . . . . . . . . . . . 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 )
169 nfv 1752 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ b ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )
170 nfra1 2807 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
171169, 170nfan 1985 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
172 nfv 1752 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ b ( x  e.  X  /\  w  e.  X
)
173171, 172nfan 1985 . . . . . . . . . . . . . . . . . . . . 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
) )
174 nfv 1752 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ b ( ( x C w )  < inf ( ran  ran  g ,  RR ,  <  )  ->  (
( f `  x
) D ( f `
 w ) )  <  d )
175 rspa 2793 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
176 oveq2 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  x  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C x ) )
177176breq1d 4431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  x  ->  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  <->  ( ( 1st `  ( g `  b
) ) C x )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
178 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  x  ->  (
f `  c )  =  ( f `  x ) )
179178oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  x  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) ) )
180179breq1d 4431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  x  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  x
) )  <  (
d  /  2 ) ) )
181177, 180imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 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 ) ) ) )
182181rspcva 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )  ->  (
( ( 1st `  (
g `  b )
) C x )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  ->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  x
) )  <  (
d  /  2 ) ) )
183 oveq2 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  w  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C w ) )
184183breq1d 4431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  w  ->  (
( ( 1st `  (
g `  b )
) C c )  <  ( ( 2nd `  ( g `  b
) )  +  ( 2nd `  ( g `
 b ) ) )  <->  ( ( 1st `  ( g `  b
) ) C w )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
18544oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( c  =  w  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 w ) ) )
186185breq1d 4431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( c  =  w  ->  (
( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) )  <  ( d  / 
2 )  <->  ( (
f `  ( 1st `  ( g `  b
) ) ) D ( f `  w
) )  <  (
d  /  2 ) ) )
187184, 186imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 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 ) ) ) )
188187rspcva 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 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 ) ) )
189182, 188anim12i 569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 ) ) ) )
190189anandirs 839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )  ->  (
( 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 ) ) ) )
191 prth 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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
) ) ) )
192190, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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
) ) ) )
193192adantrl 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )  -> 
( ( ( ( 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
) ) ) )
194193ad4ant23 1236 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
195 simpll 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  ->  (
( ph  /\  f : X --> Y )  /\  d  e.  RR+ ) )
196195anim1i 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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+ ) ) )
197196anim1i 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
198110, 151syl6ss 3477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR )
199198adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ran  ran  g  C_  RR )
200 0re 9645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  RR
201 rpge0 11316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  e.  RR+  ->  0  <_ 
y )
202201rgen 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  A. y  e.  RR+  0  <_  y
203 ssralv 3526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ran 
ran  g  C_  RR+  ->  ( A. y  e.  RR+  0  <_  y  ->  A. y  e.  ran  ran  g 0  <_  y ) )
204110, 202, 203mpisyl 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g : s --> ( X  X.  RR+ )  ->  A. y  e.  ran  ran  g 0  <_  y )
205 breq1 4424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
206205ralbidv 2865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  0  ->  ( A. y  e.  ran  ran  g  x  <_  y  <->  A. y  e.  ran  ran  g 0  <_  y
) )
207206rspcev 3183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 0  e.  RR  /\  A. y  e.  ran  ran  g 0  <_  y
)  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
208200, 204, 207sylancr 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
209208adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
210144adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  Rel  ran  g
)
211 ffn 5744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g : s --> ( X  X.  RR+ )  ->  g  Fn  s )
212 fnfvelrn 6032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g  Fn  s  /\  b  e.  s )  ->  ( g `  b
)  e.  ran  g
)
213211, 212sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ran  g )
214 2ndrn 6853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( Rel  ran  g  /\  ( g `  b
)  e.  ran  g
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
215210, 213, 214syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
216 infrelb 10598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  -> inf ( ran 
ran  g ,  RR ,  <  )  <_  ( 2nd `  ( g `  b ) ) )
217199, 209, 215, 216syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  -> inf ( ran  ran  g ,  RR ,  <  )  <_  ( 2nd `  ( g `  b
) ) )
218217adantll 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  -> inf ( ran 
ran  g ,  RR ,  <  )  <_  ( 2nd `  ( g `  b ) ) )
219218ad2ant2r 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)  -> inf ( ran  ran  g ,  RR ,  <  )  <_  ( 2nd `  ( g `  b
) ) )
22018ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  C  e.  ( *Met `  X ) )
221 xmetcl 21338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  w  e.  X
)  ->  ( x C w )  e. 
RR* )
2222213expb 1207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( C  e.  ( *Met `  X )  /\  ( x  e.  X  /\  w  e.  X ) )  -> 
( x C w )  e.  RR* )
223220, 222sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  ( x C w )  e. 
RR* )
224223adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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* )
225 simplr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  g :
s --> ( X  X.  RR+ ) )
226 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( b  e.  s  /\  x  e.  b )  ->  b  e.  s )
227 ne0i 3768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 2nd `  ( g `
 b ) )  e.  ran  ran  g  ->  ran  ran  g  =/=  (/) )
228215, 227syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ran  ran  g  =/=  (/) )
229 infrecl 10592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ran  ran  g  C_  RR  /\  ran  ran  g  =/=  (/)  /\  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )  -> inf ( ran 
ran  g ,  RR ,  <  )  e.  RR )
230199, 228, 209, 229syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  -> inf ( ran  ran  g ,  RR ,  <  )  e.  RR )
231230rexrd 9692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  -> inf ( ran  ran  g ,  RR ,  <  )  e.  RR* )
232225, 226, 231syl2an 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)  -> inf ( ran  ran  g ,  RR ,  <  )  e.  RR* )
233 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  g : s --> ( X  X.  RR+ ) )
234233ffvelrnda 6035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  (
g `  b )  e.  ( X  X.  RR+ ) )
235 xp2nd 6836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g `  b )  e.  ( X  X.  RR+ )  ->  ( 2nd `  ( g `  b
) )  e.  RR+ )
236234, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e.  RR+ )
237236rpxrd 11344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e. 
RR* )
238237ad2ant2r 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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* )
239 xrltletr 11456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( x C w )  e.  RR*  /\ inf ( ran  ran  g ,  RR ,  <  )  e.  RR*  /\  ( 2nd `  (
g `  b )
)  e.  RR* )  ->  ( ( ( x C w )  < inf ( ran  ran  g ,  RR ,  <  )  /\ inf ( ran  ran  g ,  RR ,  <  )  <_ 
( 2nd `  (
g `  b )
) )  ->  (
x C w )  <  ( 2nd `  (
g `  b )
) ) )
240224, 232, 238, 239syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  < inf ( ran  ran  g ,  RR ,  <  )  /\ inf ( ran  ran  g ,  RR ,  <  )  <_  ( 2nd `  ( g `  b
) ) )  -> 
( x C w )  <  ( 2nd `  ( g `  b
) ) ) )
241219, 240mpan2d 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  < inf ( ran  ran  g ,  RR ,  <  )  ->  ( x C w )  < 
( 2nd `  (
g `  b )
) ) )
242241adantlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  < inf ( ran  ran  g ,  RR ,  <  )  ->  (
x C w )  <  ( 2nd `  (
g `  b )
) ) )
24318ad6antr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
244 simpllr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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+ ) )
245 ffvelrn 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ( X  X.  RR+ )
)
246 xp1st 6835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g `  b )  e.  ( X  X.  RR+ )  ->  ( 1st `  ( g `  b
) )  e.  X
)
247245, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 1st `  ( g `  b
) )  e.  X
)
248244, 226, 247syl2an 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
249 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x  e.  X  /\  w  e.  X )  ->  w  e.  X )
250249ad3antlr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
251 xmetcl 21338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( C  e.  ( *Met `  X )  /\  ( 1st `  (
g `  b )
)  e.  X  /\  w  e.  X )  ->  ( ( 1st `  (
g `  b )
) C w )  e.  RR* )
252243, 248, 250, 251syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( 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 )
) C w )  e.  RR* )
253252adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( ( ( 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 )  <  ( 2nd `  (
g `  b )
) )  ->  (
( 1st `  (
g `  b )
) C w )  e.  RR* )
254245, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 2nd `  ( g `  b
) )  e.  RR+ )
255225, 254sylan 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ( ( (
ph  /\  f : X
--> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e.  RR+ )
256255ad2ant2r 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( ( ( ( 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
) )