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

Theorem heicant 28452
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 4317 . . . . . . . . . . 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 2778 . . . . . . . . 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 2757 . . . . . . . 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 2968 . . . . . . 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 2851 . . . . . . . 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 2812 . . . . . . 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 11036 . . . . . . . . 9  |-  ( d  e.  RR+  ->  ( d  /  2 )  e.  RR+ )
10 breq2 4317 . . . . . . . . . . . . . . . 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 2756 . . . . . . . . . . . . . 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 2757 . . . . . . . . . . . . 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 2756 . . . . . . . . . . . 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 3092 . . . . . . . . . . 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 729 . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  C  e.  ( *Met `  X ) )
2019anim1i 568 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  ->  ( C  e.  ( *Met `  X )  /\  x  e.  X ) )
21 rphalfcl 11036 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  ( z  /  2 )  e.  RR+ )
2221rpxrd 11049 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( z  /  2 )  e. 
RR* )
23 eqid 2443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( MetOpen `  C )  =  (
MetOpen `  C )
2423blopn 20097 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( z  /  2
)  e.  RR* )  ->  ( x ( ball `  C ) ( z  /  2 ) )  e.  ( MetOpen `  C
) )
25243expa 1187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  e.  ( *Met `  X
)  /\  x  e.  X )  /\  (
z  /  2 )  e.  RR* )  ->  (
x ( ball `  C
) ( z  / 
2 ) )  e.  ( MetOpen `  C )
)
2620, 22, 25syl2an 477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  ( x
( ball `  C )
( z  /  2
) )  e.  (
MetOpen `  C ) )
2726adantr 465 . . . . . . . . . . . . . . . . . . . 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 11051 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  RR+  ->  0  < 
( z  /  2
) )
2922, 28jca 532 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  e.  RR*  /\  0  <  ( z  /  2
) ) )
30 xblcntr 20008 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  ( ( z  / 
2 )  e.  RR*  /\  0  <  ( z  /  2 ) ) )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
31303expa 1187 . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) )
3332adantr 465 . . . . . . . . . . . . . . . . . . . 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 4892 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  X  /\  ( z  /  2
)  e.  RR+ )  -> 
<. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3521, 34sylan2 474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  X  /\  z  e.  RR+ )  ->  <. x ,  ( z  /  2 ) >.  e.  ( X  X.  RR+ ) )
3635adantll 713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  x  e.  X
)  /\  z  e.  RR+ )  ->  <. x ,  ( z  /  2
) >.  e.  ( X  X.  RR+ ) )
3736adantr 465 . . . . . . . . . . . . . . . . . . . . 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 11020 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  e.  RR+  ->  z  e.  CC )
39382halvesd 10591 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  e.  RR+  ->  ( ( z  /  2 )  +  ( z  / 
2 ) )  =  z )
4039breq2d 4325 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2756 . . . . . . . . . . . . . . . . . . . . . . . 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 6120 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
x C c )  =  ( x C w ) )
4443breq1d 4323 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  w  ->  (
( x C c )  <  z  <->  ( x C w )  < 
z ) )
45 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  w  ->  (
f `  c )  =  ( f `  w ) )
4645oveq2d 6128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  w  ->  (
( f `  x
) D ( f `
 c ) )  =  ( ( f `
 x ) D ( f `  w
) ) )
4746breq1d 4323 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2968 . . . . . . . . . . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . 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 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  x  e. 
_V
54 ovex 6137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  /  2 )  e. 
_V
5553, 54op1std 6608 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 1st `  p
)  =  x )
5653, 54op2ndd 6609 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( 2nd `  p
)  =  ( z  /  2 ) )
5755, 56oveq12d 6130 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) ( ball `  C ) ( 2nd `  p ) )  =  ( x ( ball `  C ) ( z  /  2 ) ) )
5857eqcomd 2448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( x (
ball `  C )
( z  /  2
) )  =  ( ( 1st `  p
) ( ball `  C
) ( 2nd `  p
) ) )
5958biantrurd 508 . . . . . . . . . . . . . . . . . . . . . . 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 6127 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 1st `  p ) C c )  =  ( x C c ) )
6156, 56oveq12d 6130 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( 2nd `  p )  +  ( 2nd `  p ) )  =  ( ( z  /  2 )  +  ( z  / 
2 ) ) )
6260, 61breq12d 4326 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( ( 1st `  p ) C c )  < 
( ( 2nd `  p
)  +  ( 2nd `  p ) )  <->  ( x C c )  < 
( ( z  / 
2 )  +  ( z  /  2 ) ) ) )
6355fveq2d 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( f `  ( 1st `  p ) )  =  ( f `
 x ) )
6463oveq1d 6127 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  =  <. x ,  ( z  /  2 )
>.  ->  ( ( f `
 ( 1st `  p
) ) D ( f `  c ) )  =  ( ( f `  x ) D ( f `  c ) ) )
6564breq1d 4323 . . . . . . . . . . . . . . . . . . . . . . . . 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 2756 . . . . . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . . 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 2504 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  ( x (
ball `  C )
( z  /  2
) )  ->  (
x  e.  b  <->  x  e.  ( x ( ball `  C ) ( z  /  2 ) ) ) )
72 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . 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 704 . . . . . . . . . . . . . . . . . . . . . . 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 2757 . . . . . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . . . . . . . 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 2862 . . . . . . . . . . . . . . . . 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 2815 . . . . . . . . . . . . . . . 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 20038 . . . . . . . . . . . . . . . . . 18  |-  ( C  e.  ( *Met `  X )  ->  X  =  U. ( MetOpen `  C
) )
8318, 82syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  X  =  U. ( MetOpen
`  C ) )
8483raleqdv 2944 . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . 15  |-  U. ( MetOpen
`  C )  = 
U. ( MetOpen `  C
)
88 fveq2 5712 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 1st `  p )  =  ( 1st `  (
g `  b )
) )
89 fveq2 5712 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  ( 2nd `  p )  =  ( 2nd `  (
g `  b )
) )
9088, 89oveq12d 6130 . . . . . . . . . . . . . . . . 17  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) ( ball `  C
) ( 2nd `  p
) )  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) )
9190eqeq2d 2454 . . . . . . . . . . . . . . . 16  |-  ( p  =  ( g `  b )  ->  (
b  =  ( ( 1st `  p ) ( ball `  C
) ( 2nd `  p
) )  <->  b  =  ( ( 1st `  (
g `  b )
) ( ball `  C
) ( 2nd `  (
g `  b )
) ) ) )
9288oveq1d 6127 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 1st `  p
) C c )  =  ( ( 1st `  ( g `  b
) ) C c ) )
9389, 89oveq12d 6130 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( 2nd `  p
)  +  ( 2nd `  p ) )  =  ( ( 2nd `  (
g `  b )
)  +  ( 2nd `  ( g `  b
) ) ) )
9492, 93breq12d 4326 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( g `  b )  ->  (
( ( 1st `  p
) C c )  <  ( ( 2nd `  p )  +  ( 2nd `  p ) )  <->  ( ( 1st `  ( g `  b
) ) C c )  <  ( ( 2nd `  ( g `
 b ) )  +  ( 2nd `  (
g `  b )
) ) ) )
9588fveq2d 5716 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  =  ( g `  b )  ->  (
f `  ( 1st `  p ) )  =  ( f `  ( 1st `  ( g `  b ) ) ) )
9695oveq1d 6127 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( g `  b )  ->  (
( f `  ( 1st `  p ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 c ) ) )
9796breq1d 4323 . . . . . . . . . . . . . . . . . 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 2756 . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . 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 19016 . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . 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 3592 . . . . . . . . . . . . . . 15  |-  ( ~P ( MetOpen `  C )  i^i  Fin )  C_  Fin
105104sseli 3373 . . . . . . . . . . . . . 14  |-  ( s  e.  ( ~P ( MetOpen
`  C )  i^i 
Fin )  ->  s  e.  Fin )
106 simpll 753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  ->  ph )
107106anim1i 568 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  ( ph  /\  s  e.  Fin )
)
108 frn 5586 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  g  C_  ( X  X.  RR+ ) )
109 rnss 5089 . . . . . . . . . . . . . . . . . . . . . . . 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 5291 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  ( X  X.  RR+ )  C_  RR+
112110, 111syl6ss 3389 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR+ )
113112adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR+ )
114 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
s  e.  Fin )
115 ffun 5582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( g : s --> ( X  X.  RR+ )  ->  Fun  g )
116 vex 2996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  g  e. 
_V
117116fundmen 7404 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Fun  g  ->  dom  g  ~~  g )
118117ensymd 7381 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Fun  g  ->  g  ~~  dom  g )
119115, 118syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  dom  g )
120 fdm 5584 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( g : s --> ( X  X.  RR+ )  ->  dom  g  =  s )
121119, 120breqtrd 4337 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  g  ~~  s )
122 enfii 7551 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  Fin  /\  g  ~~  s )  -> 
g  e.  Fin )
123121, 122sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  Fin  /\  g : s --> ( X  X.  RR+ ) )  -> 
g  e.  Fin )
124 rnfi 7617 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( g  e.  Fin  ->  ran  g  e.  Fin )
125 rnfi 7617 . . . . . . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  e.  Fin )
128120adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =  s
)
129 eqtr 2460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  ->  X  =  U. s
)
13083, 129sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =  U. s
)
131 heicant.x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  X  =/=  (/) )
132131adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  X  =/=  (/) )
133130, 132eqnetrrd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  ->  U. s  =/=  (/) )
134 unieq 4120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( s  =  (/)  ->  U. s  =  U. (/) )
135 uni0 4139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  U. (/)  =  (/)
136134, 135syl6eq 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  =  (/)  ->  U. s  =  (/) )
137136necon3i 2674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( U. s  =/=  (/)  ->  s  =/=  (/) )
138133, 137syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  U. ( MetOpen
`  C )  = 
U. s )  -> 
s  =/=  (/) )
139138adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  -> 
s  =/=  (/) )
140128, 139eqnetrd 2654 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  dom  g  =/=  (/) )
141 dm0rn0 5077 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  g  =  (/)  <->  ran  g  =  (/) )
142141necon3bii 2634 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  g  =/=  (/)  <->  ran  g  =/=  (/) )
143140, 142sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  U. ( MetOpen `  C )  =  U. s )  /\  g : s --> ( X  X.  RR+ ) )  ->  ran  g  =/=  (/) )
144 relxp 4968 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  Rel  ( X  X.  RR+ )
145 relss 4948 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5118 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( Rel 
ran  g  ->  ( ran  g  =  (/)  <->  ran  ran  g  =  (/) ) )
148147necon3bid 2637 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Rel 
ran  g  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
149146, 148syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g : s --> ( X  X.  RR+ )  ->  ( ran  g  =/=  (/)  <->  ran  ran  g  =/=  (/) ) )
150149adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  =/=  (/) )
153 rpssre 11022 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR+  C_  RR
154113, 153syl6ss 3389 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  ran  ran  g  C_  RR )
155 ltso 9476 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  <  Or  RR
156 cnvso 5397 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (  < 
Or  RR  <->  `'  <  Or  RR )
157155, 156mpbi 208 . . . . . . . . . . . . . . . . . . . . . . 23  |-  `'  <  Or  RR
158 fisupcl 7738 . . . . . . . . . . . . . . . . . . . . . . 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 670 . . . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . . . 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 3378 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  s  e.  Fin )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  g :
s --> ( X  X.  RR+ ) )  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR+ )
162107, 161sylanl1 650 . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  ->  X  =  U. ( MetOpen `  C )
)
165164anim1i 568 . . . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  X  /\  w  e.  X )  ->  x  e.  X )
168129eleq2d 2510 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( X  =  U. ( MetOpen
`  C )  /\  U. ( MetOpen `  C )  =  U. s )  -> 
( x  e.  X  <->  x  e.  U. s ) )
169 eluni2 4116 . . . . . . . . . . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( X  =  U. ( MetOpen `  C )  /\  U. ( MetOpen `  C
)  =  U. s
)  /\  x  e.  X )  ->  E. b  e.  s  x  e.  b )
172166, 167, 171syl2an 477 . . . . . . . . . . . . . . . . . . . 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 1673 . . . . . . . . . . . . . . . . . . . . . . 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 2787 . . . . . . . . . . . . . . . . . . . . . . 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 1861 . . . . . . . . . . . . . . . . . . . . . 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 1673 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ b ( x  e.  X  /\  w  e.  X
)
177175, 176nfan 1861 . . . . . . . . . . . . . . . . . . . . 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 1673 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ b ( ( x C w )  <  sup ( ran  ran  g ,  RR ,  `'  <  )  ->  ( ( f `
 x ) D ( f `  w
) )  <  d
)
179 rsp 2797 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  x  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C x ) )
182181breq1d 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( c  =  x  ->  (
f `  c )  =  ( f `  x ) )
184183oveq2d 6128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  x  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 x ) ) )
185184breq1d 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  w  ->  (
( 1st `  (
g `  b )
) C c )  =  ( ( 1st `  ( g `  b
) ) C w ) )
189188breq1d 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  =  w  ->  (
( f `  ( 1st `  ( g `  b ) ) ) D ( f `  c ) )  =  ( ( f `  ( 1st `  ( g `
 b ) ) ) D ( f `
 w ) ) )
191190breq1d 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 717 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  s  e.  Fin )  /\  U. ( MetOpen `  C )  =  U. s )  ->  (
( ph  /\  f : X --> Y )  /\  d  e.  RR+ ) )
202201anim1i 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  ran  ran  g  C_  RR )
205204adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ran  ran  g  C_  RR )
206 0re 9407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  e.  RR
207 rpge0 11024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  e.  RR+  ->  0  <_ 
y )
208207rgen 2802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  A. y  e.  RR+  0  <_  y
209 ssralv 3437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
212211ralbidv 2756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( x  =  0  ->  ( A. y  e.  ran  ran  g  x  <_  y  <->  A. y  e.  ran  ran  g 0  <_  y
) )
213212rspcev 3094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( g : s --> ( X  X.  RR+ )  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
215214adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  E. x  e.  RR  A. y  e. 
ran  ran  g  x  <_ 
y )
216146adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  Rel  ran  g
)
217 ffn 5580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( g : s --> ( X  X.  RR+ )  ->  g  Fn  s )
218 fnfvelrn 5861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g  Fn  s  /\  b  e.  s )  ->  ( g `  b
)  e.  ran  g
)
219217, 218sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ran  g )
220 2ndrn 6643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( Rel  ran  g  /\  ( g `  b
)  e.  ran  g
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
221216, 219, 220syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( 2nd `  ( g `  b
) )  e.  ran  ran  g )
222 infmrlb 10332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  <_ 
( 2nd `  (
g `  b )
) )
224223adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  C  e.  ( *Met `  X ) )
227 xmetcl 19928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( C  e.  ( *Met `  X )  /\  x  e.  X  /\  w  e.  X
)  ->  ( x C w )  e. 
RR* )
2282273expb 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( C  e.  ( *Met `  X )  /\  ( x  e.  X  /\  w  e.  X ) )  -> 
( x C w )  e.  RR* )
229226, 228sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  (
x  e.  X  /\  w  e.  X )
)  ->  g :
s --> ( X  X.  RR+ ) )
232 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( b  e.  s  /\  x  e.  b )  ->  b  e.  s )
233 ne0i 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e.  RR )
237236rexrd 9454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  sup ( ran  ran  g ,  RR ,  `'  <  )  e. 
RR* )
238231, 232, 237syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  ->  g : s --> ( X  X.  RR+ ) )
240239ffvelrnda 5864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  (
g `  b )  e.  ( X  X.  RR+ ) )
241 xp2nd 6628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  b  e.  s )  ->  ( 2nd `  ( g `  b ) )  e. 
RR* )
244243ad2ant2r 746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( g : s --> ( X  X.  RR+ )  /\  b  e.  s
)  ->  ( g `  b )  e.  ( X  X.  RR+ )
)
252 xp1st 6627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( ph  /\  f : X --> Y )  /\  d  e.  RR+ )  /\  g : s --> ( X  X.  RR+ ) )  /\  ( x  e.  X  /\  w  e.  X
) )  /\  b  =  ( ( 1st `  ( g