Metamath Proof Explorer

Theorem heicant

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)

Ref Expression
Hypotheses 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 heicant 
|- ( ph -> ( ( metUnif ` C ) uCn ( metUnif ` D ) ) = ( ( MetOpen ` C ) Cn ( MetOpen ` D ) ) )

Proof

Step Hyp Ref Expression
1 heicant.c 
 |-  ( ph -> C e. ( *Met ` X ) )
2 heicant.d 
 |-  ( ph -> D e. ( *Met ` Y ) )
3 heicant.j 
 |-  ( ph -> ( MetOpen ` C ) e. Comp )
4 heicant.x 
 |-  ( ph -> X =/= (/) )
5 heicant.y 
 |-  ( ph -> Y =/= (/) )
6 breq2 
 |-  ( d = y -> ( ( ( f ` x ) D ( f ` w ) ) < d <-> ( ( f ` x ) D ( f ` w ) ) < y ) )
7 6 imbi2d 
 |-  ( d = y -> ( ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) <-> ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) )
8 7 2ralbidv 
 |-  ( 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 ) ) )
9 8 rexbidv 
 |-  ( 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 ) ) )
10 9 cbvralvw 
 |-  ( 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 ) )
11 r19.12 
 |-  ( 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 ) )
12 11 ralimi 
 |-  ( 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 ) )
13 10 12 sylbi 
 |-  ( 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 ) )
14 rphalfcl 
 |-  ( d e. RR+ -> ( d / 2 ) e. RR+ )
15 breq2 
 |-  ( y = ( d / 2 ) -> ( ( ( f ` x ) D ( f ` w ) ) < y <-> ( ( f ` x ) D ( f ` w ) ) < ( d / 2 ) ) )
16 15 imbi2d 
 |-  ( y = ( d / 2 ) -> ( ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) <-> ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < ( d / 2 ) ) ) )
17 16 ralbidv 
 |-  ( 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 ) ) ) )
18 17 rexbidv 
 |-  ( 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 ) ) ) )
19 18 ralbidv 
 |-  ( 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 ) ) ) )
20 19 rspcva 
 |-  ( ( ( 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 ) ) )
21 3 ad3antrrr 
 |-  ( ( ( ( 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 )
22 1 ad2antrr 
 |-  ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) -> C e. ( *Met ` X ) )
23 22 anim1i 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ x e. X ) -> ( C e. ( *Met ` X ) /\ x e. X ) )
24 rphalfcl 
 |-  ( z e. RR+ -> ( z / 2 ) e. RR+ )
25 24 rpxrd 
 |-  ( z e. RR+ -> ( z / 2 ) e. RR* )
26 eqid 
 |-  ( MetOpen ` C ) = ( MetOpen ` C )
27 26 blopn 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ ( z / 2 ) e. RR* ) -> ( x ( ball ` C ) ( z / 2 ) ) e. ( MetOpen ` C ) )
28 27 3expa 
 |-  ( ( ( C e. ( *Met ` X ) /\ x e. X ) /\ ( z / 2 ) e. RR* ) -> ( x ( ball ` C ) ( z / 2 ) ) e. ( MetOpen ` C ) )
29 23 25 28 syl2an 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ x e. X ) /\ z e. RR+ ) -> ( x ( ball ` C ) ( z / 2 ) ) e. ( MetOpen ` C ) )
30 29 adantr 
 |-  ( ( ( ( ( ( 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 ) )
31 24 rpgt0d 
 |-  ( z e. RR+ -> 0 < ( z / 2 ) )
32 25 31 jca 
 |-  ( z e. RR+ -> ( ( z / 2 ) e. RR* /\ 0 < ( z / 2 ) ) )
33 xblcntr 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ ( ( z / 2 ) e. RR* /\ 0 < ( z / 2 ) ) ) -> x e. ( x ( ball ` C ) ( z / 2 ) ) )
34 33 3expa 
 |-  ( ( ( C e. ( *Met ` X ) /\ x e. X ) /\ ( ( z / 2 ) e. RR* /\ 0 < ( z / 2 ) ) ) -> x e. ( x ( ball ` C ) ( z / 2 ) ) )
35 23 32 34 syl2an 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ x e. X ) /\ z e. RR+ ) -> x e. ( x ( ball ` C ) ( z / 2 ) ) )
36 35 adantr 
 |-  ( ( ( ( ( ( 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 ) ) )
37 opelxpi 
 |-  ( ( x e. X /\ ( z / 2 ) e. RR+ ) -> <. x , ( z / 2 ) >. e. ( X X. RR+ ) )
38 24 37 sylan2 
 |-  ( ( x e. X /\ z e. RR+ ) -> <. x , ( z / 2 ) >. e. ( X X. RR+ ) )
39 38 ad4ant23 
 |-  ( ( ( ( ( ( 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+ ) )
40 rpcn 
 |-  ( z e. RR+ -> z e. CC )
41 40 2halvesd 
 |-  ( z e. RR+ -> ( ( z / 2 ) + ( z / 2 ) ) = z )
42 41 breq2d 
 |-  ( z e. RR+ -> ( ( x C c ) < ( ( z / 2 ) + ( z / 2 ) ) <-> ( x C c ) < z ) )
43 42 imbi1d 
 |-  ( 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 ) ) ) )
44 43 ralbidv 
 |-  ( 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 ) ) ) )
45 oveq2 
 |-  ( c = w -> ( x C c ) = ( x C w ) )
46 45 breq1d 
 |-  ( c = w -> ( ( x C c ) < z <-> ( x C w ) < z ) )
47 fveq2 
 |-  ( c = w -> ( f ` c ) = ( f ` w ) )
48 47 oveq2d 
 |-  ( c = w -> ( ( f ` x ) D ( f ` c ) ) = ( ( f ` x ) D ( f ` w ) ) )
49 48 breq1d 
 |-  ( c = w -> ( ( ( f ` x ) D ( f ` c ) ) < ( d / 2 ) <-> ( ( f ` x ) D ( f ` w ) ) < ( d / 2 ) ) )
50 46 49 imbi12d 
 |-  ( c = w -> ( ( ( x C c ) < z -> ( ( f ` x ) D ( f ` c ) ) < ( d / 2 ) ) <-> ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < ( d / 2 ) ) ) )
51 50 cbvralvw 
 |-  ( 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 ) ) )
52 44 51 bitrdi 
 |-  ( 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 ) ) ) )
53 52 biimpar 
 |-  ( ( 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 ) ) )
54 53 adantll 
 |-  ( ( ( ( ( ( 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 ) ) )
55 vex 
 |-  x e. _V
56 ovex 
 |-  ( z / 2 ) e. _V
57 55 56 op1std 
 |-  ( p = <. x , ( z / 2 ) >. -> ( 1st ` p ) = x )
58 55 56 op2ndd 
 |-  ( p = <. x , ( z / 2 ) >. -> ( 2nd ` p ) = ( z / 2 ) )
59 57 58 oveq12d 
 |-  ( p = <. x , ( z / 2 ) >. -> ( ( 1st ` p ) ( ball ` C ) ( 2nd ` p ) ) = ( x ( ball ` C ) ( z / 2 ) ) )
60 59 eqcomd 
 |-  ( p = <. x , ( z / 2 ) >. -> ( x ( ball ` C ) ( z / 2 ) ) = ( ( 1st ` p ) ( ball ` C ) ( 2nd ` p ) ) )
61 60 biantrurd 
 |-  ( 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 ) ) ) ) )
62 57 oveq1d 
 |-  ( p = <. x , ( z / 2 ) >. -> ( ( 1st ` p ) C c ) = ( x C c ) )
63 58 58 oveq12d 
 |-  ( p = <. x , ( z / 2 ) >. -> ( ( 2nd ` p ) + ( 2nd ` p ) ) = ( ( z / 2 ) + ( z / 2 ) ) )
64 62 63 breq12d 
 |-  ( p = <. x , ( z / 2 ) >. -> ( ( ( 1st ` p ) C c ) < ( ( 2nd ` p ) + ( 2nd ` p ) ) <-> ( x C c ) < ( ( z / 2 ) + ( z / 2 ) ) ) )
65 57 fveq2d 
 |-  ( p = <. x , ( z / 2 ) >. -> ( f ` ( 1st ` p ) ) = ( f ` x ) )
66 65 oveq1d 
 |-  ( p = <. x , ( z / 2 ) >. -> ( ( f ` ( 1st ` p ) ) D ( f ` c ) ) = ( ( f ` x ) D ( f ` c ) ) )
67 66 breq1d 
 |-  ( p = <. x , ( z / 2 ) >. -> ( ( ( f ` ( 1st ` p ) ) D ( f ` c ) ) < ( d / 2 ) <-> ( ( f ` x ) D ( f ` c ) ) < ( d / 2 ) ) )
68 64 67 imbi12d 
 |-  ( 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 ) ) ) )
69 68 ralbidv 
 |-  ( 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 ) ) ) )
70 61 69 bitr3d 
 |-  ( 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 ) ) ) )
71 70 rspcev 
 |-  ( ( <. 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 ) ) ) )
72 39 54 71 syl2anc 
 |-  ( ( ( ( ( ( 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 ) ) ) )
73 eleq2 
 |-  ( b = ( x ( ball ` C ) ( z / 2 ) ) -> ( x e. b <-> x e. ( x ( ball ` C ) ( z / 2 ) ) ) )
74 eqeq1 
 |-  ( b = ( x ( ball ` C ) ( z / 2 ) ) -> ( b = ( ( 1st ` p ) ( ball ` C ) ( 2nd ` p ) ) <-> ( x ( ball ` C ) ( z / 2 ) ) = ( ( 1st ` p ) ( ball ` C ) ( 2nd ` p ) ) ) )
75 74 anbi1d 
 |-  ( 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 ) ) ) ) )
76 75 rexbidv 
 |-  ( 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 ) ) ) ) )
77 73 76 anbi12d 
 |-  ( 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 ) ) ) ) ) )
78 77 rspcev 
 |-  ( ( ( 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 ) ) ) ) )
79 30 36 72 78 syl12anc 
 |-  ( ( ( ( ( ( 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 ) ) ) ) )
80 79 rexlimdva2 
 |-  ( ( ( ( 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 ) ) ) ) ) )
81 80 ralimdva 
 |-  ( ( ( 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 ) ) ) ) ) )
82 81 imp 
 |-  ( ( ( ( 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 ) ) ) ) )
83 26 mopnuni 
 |-  ( C e. ( *Met ` X ) -> X = U. ( MetOpen ` C ) )
84 1 83 syl 
 |-  ( ph -> X = U. ( MetOpen ` C ) )
85 84 raleqdv 
 |-  ( 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 ) ) ) ) ) )
86 85 ad3antrrr 
 |-  ( ( ( ( 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 ) ) ) ) ) )
87 82 86 mpbid 
 |-  ( ( ( ( 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 ) ) ) ) )
88 eqid 
 |-  U. ( MetOpen ` C ) = U. ( MetOpen ` C )
89 fveq2 
 |-  ( p = ( g ` b ) -> ( 1st ` p ) = ( 1st ` ( g ` b ) ) )
90 fveq2 
 |-  ( p = ( g ` b ) -> ( 2nd ` p ) = ( 2nd ` ( g ` b ) ) )
91 89 90 oveq12d 
 |-  ( p = ( g ` b ) -> ( ( 1st ` p ) ( ball ` C ) ( 2nd ` p ) ) = ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) )
92 91 eqeq2d 
 |-  ( p = ( g ` b ) -> ( b = ( ( 1st ` p ) ( ball ` C ) ( 2nd ` p ) ) <-> b = ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) ) )
93 89 oveq1d 
 |-  ( p = ( g ` b ) -> ( ( 1st ` p ) C c ) = ( ( 1st ` ( g ` b ) ) C c ) )
94 90 90 oveq12d 
 |-  ( p = ( g ` b ) -> ( ( 2nd ` p ) + ( 2nd ` p ) ) = ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) )
95 93 94 breq12d 
 |-  ( p = ( g ` b ) -> ( ( ( 1st ` p ) C c ) < ( ( 2nd ` p ) + ( 2nd ` p ) ) <-> ( ( 1st ` ( g ` b ) ) C c ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) ) )
96 89 fveq2d 
 |-  ( p = ( g ` b ) -> ( f ` ( 1st ` p ) ) = ( f ` ( 1st ` ( g ` b ) ) ) )
97 96 oveq1d 
 |-  ( p = ( g ` b ) -> ( ( f ` ( 1st ` p ) ) D ( f ` c ) ) = ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` c ) ) )
98 97 breq1d 
 |-  ( p = ( g ` b ) -> ( ( ( f ` ( 1st ` p ) ) D ( f ` c ) ) < ( d / 2 ) <-> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` c ) ) < ( d / 2 ) ) )
99 95 98 imbi12d 
 |-  ( 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 ) ) ) )
100 99 ralbidv 
 |-  ( 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 ) ) ) )
101 92 100 anbi12d 
 |-  ( 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 ) ) ) ) )
102 88 101 cmpcovf 
 |-  ( ( ( 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 ) ) ) ) ) )
103 21 87 102 syl2anc 
 |-  ( ( ( ( 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 103 ex 
 |-  ( ( ( 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 ) ) ) ) ) ) )
105 elinel2 
 |-  ( s e. ( ~P ( MetOpen ` C ) i^i Fin ) -> s e. Fin )
106 simpll 
 |-  ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) -> ph )
107 106 anim1i 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ s e. Fin ) -> ( ph /\ s e. Fin ) )
108 frn 
 |-  ( g : s --> ( X X. RR+ ) -> ran g C_ ( X X. RR+ ) )
109 rnss 
 |-  ( ran g C_ ( X X. RR+ ) -> ran ran g C_ ran ( X X. RR+ ) )
110 108 109 syl 
 |-  ( g : s --> ( X X. RR+ ) -> ran ran g C_ ran ( X X. RR+ ) )
111 rnxpss 
 |-  ran ( X X. RR+ ) C_ RR+
112 110 111 sstrdi 
 |-  ( g : s --> ( X X. RR+ ) -> ran ran g C_ RR+ )
113 112 adantl 
 |-  ( ( ( ( ph /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> ran ran g C_ RR+ )
114 simplr 
 |-  ( ( ( ph /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) -> s e. Fin )
115 ffun 
 |-  ( g : s --> ( X X. RR+ ) -> Fun g )
116 vex 
 |-  g e. _V
117 116 fundmen 
 |-  ( Fun g -> dom g ~~ g )
118 117 ensymd 
 |-  ( Fun g -> g ~~ dom g )
119 115 118 syl 
 |-  ( g : s --> ( X X. RR+ ) -> g ~~ dom g )
120 fdm 
 |-  ( g : s --> ( X X. RR+ ) -> dom g = s )
121 119 120 breqtrd 
 |-  ( g : s --> ( X X. RR+ ) -> g ~~ s )
122 enfii 
 |-  ( ( s e. Fin /\ g ~~ s ) -> g e. Fin )
123 121 122 sylan2 
 |-  ( ( s e. Fin /\ g : s --> ( X X. RR+ ) ) -> g e. Fin )
124 rnfi 
 |-  ( g e. Fin -> ran g e. Fin )
125 rnfi 
 |-  ( ran g e. Fin -> ran ran g e. Fin )
126 123 124 125 3syl 
 |-  ( ( s e. Fin /\ g : s --> ( X X. RR+ ) ) -> ran ran g e. Fin )
127 114 126 sylan 
 |-  ( ( ( ( ph /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> ran ran g e. Fin )
128 120 adantl 
 |-  ( ( ( ph /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> dom g = s )
129 eqtr 
 |-  ( ( X = U. ( MetOpen ` C ) /\ U. ( MetOpen ` C ) = U. s ) -> X = U. s )
130 84 129 sylan 
 |-  ( ( ph /\ U. ( MetOpen ` C ) = U. s ) -> X = U. s )
131 4 adantr 
 |-  ( ( ph /\ U. ( MetOpen ` C ) = U. s ) -> X =/= (/) )
132 130 131 eqnetrrd 
 |-  ( ( ph /\ U. ( MetOpen ` C ) = U. s ) -> U. s =/= (/) )
133 unieq 
 |-  ( s = (/) -> U. s = U. (/) )
134 uni0 
 |-  U. (/) = (/)
135 133 134 eqtrdi 
 |-  ( s = (/) -> U. s = (/) )
136 135 necon3i 
 |-  ( U. s =/= (/) -> s =/= (/) )
137 132 136 syl 
 |-  ( ( ph /\ U. ( MetOpen ` C ) = U. s ) -> s =/= (/) )
138 137 adantr 
 |-  ( ( ( ph /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> s =/= (/) )
139 128 138 eqnetrd 
 |-  ( ( ( ph /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> dom g =/= (/) )
140 dm0rn0 
 |-  ( dom g = (/) <-> ran g = (/) )
141 140 necon3bii 
 |-  ( dom g =/= (/) <-> ran g =/= (/) )
142 139 141 sylib 
 |-  ( ( ( ph /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> ran g =/= (/) )
143 relxp 
 |-  Rel ( X X. RR+ )
144 relss 
 |-  ( ran g C_ ( X X. RR+ ) -> ( Rel ( X X. RR+ ) -> Rel ran g ) )
145 108 143 144 mpisyl 
 |-  ( g : s --> ( X X. RR+ ) -> Rel ran g )
146 relrn0 
 |-  ( Rel ran g -> ( ran g = (/) <-> ran ran g = (/) ) )
147 146 necon3bid 
 |-  ( Rel ran g -> ( ran g =/= (/) <-> ran ran g =/= (/) ) )
148 145 147 syl 
 |-  ( g : s --> ( X X. RR+ ) -> ( ran g =/= (/) <-> ran ran g =/= (/) ) )
149 148 adantl 
 |-  ( ( ( ph /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> ( ran g =/= (/) <-> ran ran g =/= (/) ) )
150 142 149 mpbid 
 |-  ( ( ( ph /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> ran ran g =/= (/) )
151 150 adantllr 
 |-  ( ( ( ( ph /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> ran ran g =/= (/) )
152 rpssre 
 |-  RR+ C_ RR
153 113 152 sstrdi 
 |-  ( ( ( ( ph /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> ran ran g C_ RR )
154 ltso 
 |-  < Or RR
155 fiinfcl 
 |-  ( ( < Or RR /\ ( ran ran g e. Fin /\ ran ran g =/= (/) /\ ran ran g C_ RR ) ) -> inf ( ran ran g , RR , < ) e. ran ran g )
156 154 155 mpan 
 |-  ( ( ran ran g e. Fin /\ ran ran g =/= (/) /\ ran ran g C_ RR ) -> inf ( ran ran g , RR , < ) e. ran ran g )
157 127 151 153 156 syl3anc 
 |-  ( ( ( ( ph /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> inf ( ran ran g , RR , < ) e. ran ran g )
158 113 157 sseldd 
 |-  ( ( ( ( ph /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) ) -> inf ( ran ran g , RR , < ) e. RR+ )
159 107 158 sylanl1 
 |-  ( ( ( ( ( ( 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+ )
160 159 adantr 
 |-  ( ( ( ( ( ( ( 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+ )
161 84 ad3antrrr 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ s e. Fin ) -> X = U. ( MetOpen ` C ) )
162 161 anim1i 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) -> ( X = U. ( MetOpen ` C ) /\ U. ( MetOpen ` C ) = U. s ) )
163 162 ad2antrr 
 |-  ( ( ( ( ( ( ( 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 ) )
164 simpl 
 |-  ( ( x e. X /\ w e. X ) -> x e. X )
165 129 eleq2d 
 |-  ( ( X = U. ( MetOpen ` C ) /\ U. ( MetOpen ` C ) = U. s ) -> ( x e. X <-> x e. U. s ) )
166 eluni2 
 |-  ( x e. U. s <-> E. b e. s x e. b )
167 165 166 bitrdi 
 |-  ( ( X = U. ( MetOpen ` C ) /\ U. ( MetOpen ` C ) = U. s ) -> ( x e. X <-> E. b e. s x e. b ) )
168 167 biimpa 
 |-  ( ( ( X = U. ( MetOpen ` C ) /\ U. ( MetOpen ` C ) = U. s ) /\ x e. X ) -> E. b e. s x e. b )
169 163 164 168 syl2an 
 |-  ( ( ( ( ( ( ( ( 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 )
170 nfv 
 |-  F/ b ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) /\ g : s --> ( X X. RR+ ) )
171 nfra1 
 |-  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 ) ) )
172 170 171 nfan 
 |-  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 ) ) ) )
173 nfv 
 |-  F/ b ( x e. X /\ w e. X )
174 172 173 nfan 
 |-  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 ) )
175 nfv 
 |-  F/ b ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d )
176 rspa 
 |-  ( ( 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 ) ) ) )
177 oveq2 
 |-  ( c = x -> ( ( 1st ` ( g ` b ) ) C c ) = ( ( 1st ` ( g ` b ) ) C x ) )
178 177 breq1d 
 |-  ( c = x -> ( ( ( 1st ` ( g ` b ) ) C c ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) <-> ( ( 1st ` ( g ` b ) ) C x ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) ) )
179 fveq2 
 |-  ( c = x -> ( f ` c ) = ( f ` x ) )
180 179 oveq2d 
 |-  ( c = x -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` c ) ) = ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) )
181 180 breq1d 
 |-  ( c = x -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` c ) ) < ( d / 2 ) <-> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) ) )
182 178 181 imbi12d 
 |-  ( 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 ) ) ) )
183 182 rspcva 
 |-  ( ( 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 ) ) )
184 oveq2 
 |-  ( c = w -> ( ( 1st ` ( g ` b ) ) C c ) = ( ( 1st ` ( g ` b ) ) C w ) )
185 184 breq1d 
 |-  ( c = w -> ( ( ( 1st ` ( g ` b ) ) C c ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) <-> ( ( 1st ` ( g ` b ) ) C w ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) ) )
186 47 oveq2d 
 |-  ( c = w -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` c ) ) = ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) )
187 186 breq1d 
 |-  ( c = w -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` c ) ) < ( d / 2 ) <-> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) )
188 185 187 imbi12d 
 |-  ( 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 ) ) ) )
189 188 rspcva 
 |-  ( ( 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 ) ) )
190 183 189 anim12i 
 |-  ( ( ( 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 ) ) ) )
191 190 anandirs 
 |-  ( ( ( 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 ) ) ) )
192 anim12 
 |-  ( ( ( ( ( 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 ) ) ) )
193 191 192 syl 
 |-  ( ( ( 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 ) ) ) )
194 193 adantrl 
 |-  ( ( ( 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 ) ) ) )
195 194 ad4ant23 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) ) )
196 simpll 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ s e. Fin ) /\ U. ( MetOpen ` C ) = U. s ) -> ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) )
197 196 anim1i 
 |-  ( ( ( ( ( ( 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+ ) ) )
198 197 anim1i 
 |-  ( ( ( ( ( ( ( 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 ) ) )
199 112 152 sstrdi 
 |-  ( g : s --> ( X X. RR+ ) -> ran ran g C_ RR )
200 199 adantr 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ran ran g C_ RR )
201 0re 
 |-  0 e. RR
202 rpge0 
 |-  ( y e. RR+ -> 0 <_ y )
203 202 rgen 
 |-  A. y e. RR+ 0 <_ y
204 ssralv 
 |-  ( ran ran g C_ RR+ -> ( A. y e. RR+ 0 <_ y -> A. y e. ran ran g 0 <_ y ) )
205 112 203 204 mpisyl 
 |-  ( g : s --> ( X X. RR+ ) -> A. y e. ran ran g 0 <_ y )
206 breq1 
 |-  ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
207 206 ralbidv 
 |-  ( x = 0 -> ( A. y e. ran ran g x <_ y <-> A. y e. ran ran g 0 <_ y ) )
208 207 rspcev 
 |-  ( ( 0 e. RR /\ A. y e. ran ran g 0 <_ y ) -> E. x e. RR A. y e. ran ran g x <_ y )
209 201 205 208 sylancr 
 |-  ( g : s --> ( X X. RR+ ) -> E. x e. RR A. y e. ran ran g x <_ y )
210 209 adantr 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> E. x e. RR A. y e. ran ran g x <_ y )
211 145 adantr 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> Rel ran g )
212 ffn 
 |-  ( g : s --> ( X X. RR+ ) -> g Fn s )
213 fnfvelrn 
 |-  ( ( g Fn s /\ b e. s ) -> ( g ` b ) e. ran g )
214 212 213 sylan 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( g ` b ) e. ran g )
215 2ndrn 
 |-  ( ( Rel ran g /\ ( g ` b ) e. ran g ) -> ( 2nd ` ( g ` b ) ) e. ran ran g )
216 211 214 215 syl2anc 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) e. ran ran g )
217 infrelb 
 |-  ( ( 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 ) ) )
218 200 210 216 217 syl3anc 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> inf ( ran ran g , RR , < ) <_ ( 2nd ` ( g ` b ) ) )
219 218 adantll 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ b e. s ) -> inf ( ran ran g , RR , < ) <_ ( 2nd ` ( g ` b ) ) )
220 219 ad2ant2r 
 |-  ( ( ( ( ( ( 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 ) ) )
221 1 ad3antrrr 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) -> C e. ( *Met ` X ) )
222 xmetcl 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ w e. X ) -> ( x C w ) e. RR* )
223 222 3expb 
 |-  ( ( C e. ( *Met ` X ) /\ ( x e. X /\ w e. X ) ) -> ( x C w ) e. RR* )
224 221 223 sylan 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) -> ( x C w ) e. RR* )
225 224 adantr 
 |-  ( ( ( ( ( ( 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* )
226 simplr 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) -> g : s --> ( X X. RR+ ) )
227 simpl 
 |-  ( ( b e. s /\ x e. b ) -> b e. s )
228 216 ne0d 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ran ran g =/= (/) )
229 infrecl 
 |-  ( ( 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 )
230 200 228 210 229 syl3anc 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> inf ( ran ran g , RR , < ) e. RR )
231 230 rexrd 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> inf ( ran ran g , RR , < ) e. RR* )
232 226 227 231 syl2an 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) -> g : s --> ( X X. RR+ ) )
234 233 ffvelrnda 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ b e. s ) -> ( g ` b ) e. ( X X. RR+ ) )
235 xp2nd 
 |-  ( ( g ` b ) e. ( X X. RR+ ) -> ( 2nd ` ( g ` b ) ) e. RR+ )
236 234 235 syl 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) e. RR+ )
237 236 rpxrd 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) e. RR* )
238 237 ad2ant2r 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( 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 ) ) ) )
240 225 232 238 239 syl3anc 
 |-  ( ( ( ( ( ( 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 ) ) ) )
241 220 240 mpan2d 
 |-  ( ( ( ( ( ( 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 ) ) ) )
242 241 adantlr 
 |-  ( ( ( ( ( ( ( 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 ) ) ) )
243 1 ad6antr 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( g ` b ) e. ( X X. RR+ ) )
246 xp1st 
 |-  ( ( g ` b ) e. ( X X. RR+ ) -> ( 1st ` ( g ` b ) ) e. X )
247 245 246 syl 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( 1st ` ( g ` b ) ) e. X )
248 244 227 247 syl2an 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( x e. X /\ w e. X ) -> w e. X )
250 249 ad3antlr 
 |-  ( ( ( ( ( ( ( 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 
 |-  ( ( C e. ( *Met ` X ) /\ ( 1st ` ( g ` b ) ) e. X /\ w e. X ) -> ( ( 1st ` ( g ` b ) ) C w ) e. RR* )
252 243 248 250 251 syl3anc 
 |-  ( ( ( ( ( ( ( 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* )
253 252 adantr 
 |-  ( ( ( ( ( ( ( ( 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* )
254 245 235 syl 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) e. RR+ )
255 226 254 sylan 
 |-  ( ( ( ( ( ( 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+ )
256 255 ad2ant2r 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( 2nd ` ( g ` b ) ) e. RR+ )
257 256 rpred 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( 2nd ` ( g ` b ) ) e. RR )
258 164 ad3antlr 
 |-  ( ( ( ( ( ( ( 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 e. X )
259 xmetcl 
 |-  ( ( C e. ( *Met ` X ) /\ ( 1st ` ( g ` b ) ) e. X /\ x e. X ) -> ( ( 1st ` ( g ` b ) ) C x ) e. RR* )
260 243 248 258 259 syl3anc 
 |-  ( ( ( ( ( ( ( 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 x ) e. RR* )
261 254 rpxrd 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) e. RR* )
262 244 227 261 syl2an 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( 2nd ` ( g ` b ) ) e. RR* )
263 eleq2 
 |-  ( b = ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) -> ( x e. b <-> x e. ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) ) )
264 1 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> C e. ( *Met ` X ) )
265 226 247 sylan 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( 1st ` ( g ` b ) ) e. X )
266 255 rpxrd 
 |-  ( ( ( ( ( ( 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* )
267 elbl 
 |-  ( ( C e. ( *Met ` X ) /\ ( 1st ` ( g ` b ) ) e. X /\ ( 2nd ` ( g ` b ) ) e. RR* ) -> ( x e. ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) <-> ( x e. X /\ ( ( 1st ` ( g ` b ) ) C x ) < ( 2nd ` ( g ` b ) ) ) ) )
268 264 265 266 267 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( x e. ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) <-> ( x e. X /\ ( ( 1st ` ( g ` b ) ) C x ) < ( 2nd ` ( g ` b ) ) ) ) )
269 263 268 sylan9bbr 
 |-  ( ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) /\ b = ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) ) -> ( x e. b <-> ( x e. X /\ ( ( 1st ` ( g ` b ) ) C x ) < ( 2nd ` ( g ` b ) ) ) ) )
270 269 biimpd 
 |-  ( ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) /\ b = ( ( 1st ` ( g ` b ) ) ( ball ` C ) ( 2nd ` ( g ` b ) ) ) ) -> ( x e. b -> ( x e. X /\ ( ( 1st ` ( g ` b ) ) C x ) < ( 2nd ` ( g ` b ) ) ) ) )
271 270 an32s 
 |-  ( ( ( ( ( ( ( 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 e. X /\ ( ( 1st ` ( g ` b ) ) C x ) < ( 2nd ` ( g ` b ) ) ) ) )
272 271 impr 
 |-  ( ( ( ( ( ( ( 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 e. X /\ ( ( 1st ` ( g ` b ) ) C x ) < ( 2nd ` ( g ` b ) ) ) )
273 272 simprd 
 |-  ( ( ( ( ( ( ( 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 x ) < ( 2nd ` ( g ` b ) ) )
274 260 262 273 xrltled 
 |-  ( ( ( ( ( ( ( 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 x ) <_ ( 2nd ` ( g ` b ) ) )
275 226 ffvelrnda 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( g ` b ) e. ( X X. RR+ ) )
276 275 246 syl 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( 1st ` ( g ` b ) ) e. X )
277 simplrl 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> x e. X )
278 264 276 277 259 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( 1st ` ( g ` b ) ) C x ) e. RR* )
279 xmetge0 
 |-  ( ( C e. ( *Met ` X ) /\ ( 1st ` ( g ` b ) ) e. X /\ x e. X ) -> 0 <_ ( ( 1st ` ( g ` b ) ) C x ) )
280 264 276 277 279 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> 0 <_ ( ( 1st ` ( g ` b ) ) C x ) )
281 xrrege0 
 |-  ( ( ( ( ( 1st ` ( g ` b ) ) C x ) e. RR* /\ ( 2nd ` ( g ` b ) ) e. RR ) /\ ( 0 <_ ( ( 1st ` ( g ` b ) ) C x ) /\ ( ( 1st ` ( g ` b ) ) C x ) <_ ( 2nd ` ( g ` b ) ) ) ) -> ( ( 1st ` ( g ` b ) ) C x ) e. RR )
282 281 an4s 
 |-  ( ( ( ( ( 1st ` ( g ` b ) ) C x ) e. RR* /\ 0 <_ ( ( 1st ` ( g ` b ) ) C x ) ) /\ ( ( 2nd ` ( g ` b ) ) e. RR /\ ( ( 1st ` ( g ` b ) ) C x ) <_ ( 2nd ` ( g ` b ) ) ) ) -> ( ( 1st ` ( g ` b ) ) C x ) e. RR )
283 282 ex 
 |-  ( ( ( ( 1st ` ( g ` b ) ) C x ) e. RR* /\ 0 <_ ( ( 1st ` ( g ` b ) ) C x ) ) -> ( ( ( 2nd ` ( g ` b ) ) e. RR /\ ( ( 1st ` ( g ` b ) ) C x ) <_ ( 2nd ` ( g ` b ) ) ) -> ( ( 1st ` ( g ` b ) ) C x ) e. RR ) )
284 278 280 283 syl2anc 
 |-  ( ( ( ( ( ( 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 /\ ( ( 1st ` ( g ` b ) ) C x ) <_ ( 2nd ` ( g ` b ) ) ) -> ( ( 1st ` ( g ` b ) ) C x ) e. RR ) )
285 284 ad2ant2r 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( ( 2nd ` ( g ` b ) ) e. RR /\ ( ( 1st ` ( g ` b ) ) C x ) <_ ( 2nd ` ( g ` b ) ) ) -> ( ( 1st ` ( g ` b ) ) C x ) e. RR ) )
286 257 274 285 mp2and 
 |-  ( ( ( ( ( ( ( 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 x ) e. RR )
287 286 adantr 
 |-  ( ( ( ( ( ( ( ( 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 x ) e. RR )
288 xrltle 
 |-  ( ( ( x C w ) e. RR* /\ ( 2nd ` ( g ` b ) ) e. RR* ) -> ( ( x C w ) < ( 2nd ` ( g ` b ) ) -> ( x C w ) <_ ( 2nd ` ( g ` b ) ) ) )
289 225 238 288 syl2anc 
 |-  ( ( ( ( ( ( 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 ) < ( 2nd ` ( g ` b ) ) -> ( x C w ) <_ ( 2nd ` ( g ` b ) ) ) )
290 xmetge0 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ w e. X ) -> 0 <_ ( x C w ) )
291 290 3expb 
 |-  ( ( C e. ( *Met ` X ) /\ ( x e. X /\ w e. X ) ) -> 0 <_ ( x C w ) )
292 221 291 sylan 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) -> 0 <_ ( x C w ) )
293 292 adantr 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ ( b e. s /\ x e. b ) ) -> 0 <_ ( x C w ) )
294 236 rpred 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) e. RR )
295 294 ad2ant2r 
 |-  ( ( ( ( ( ( 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 )
296 xrrege0 
 |-  ( ( ( ( x C w ) e. RR* /\ ( 2nd ` ( g ` b ) ) e. RR ) /\ ( 0 <_ ( x C w ) /\ ( x C w ) <_ ( 2nd ` ( g ` b ) ) ) ) -> ( x C w ) e. RR )
297 296 ex 
 |-  ( ( ( x C w ) e. RR* /\ ( 2nd ` ( g ` b ) ) e. RR ) -> ( ( 0 <_ ( x C w ) /\ ( x C w ) <_ ( 2nd ` ( g ` b ) ) ) -> ( x C w ) e. RR ) )
298 225 295 297 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ ( b e. s /\ x e. b ) ) -> ( ( 0 <_ ( x C w ) /\ ( x C w ) <_ ( 2nd ` ( g ` b ) ) ) -> ( x C w ) e. RR ) )
299 293 298 mpand 
 |-  ( ( ( ( ( ( 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 ) <_ ( 2nd ` ( g ` b ) ) -> ( x C w ) e. RR ) )
300 289 299 syld 
 |-  ( ( ( ( ( ( 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 ) < ( 2nd ` ( g ` b ) ) -> ( x C w ) e. RR ) )
301 300 adantlr 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( x C w ) e. RR ) )
302 301 imp 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) -> ( x C w ) e. RR )
303 287 302 readdcld 
 |-  ( ( ( ( ( ( ( ( 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 x ) + ( x C w ) ) e. RR )
304 303 rexrd 
 |-  ( ( ( ( ( ( ( ( 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 x ) + ( x C w ) ) e. RR* )
305 256 256 rpaddcld 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) e. RR+ )
306 305 rpxrd 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) e. RR* )
307 306 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) -> ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) e. RR* )
308 xmettri 
 |-  ( ( C e. ( *Met ` X ) /\ ( ( 1st ` ( g ` b ) ) e. X /\ w e. X /\ x e. X ) ) -> ( ( 1st ` ( g ` b ) ) C w ) <_ ( ( ( 1st ` ( g ` b ) ) C x ) +e ( x C w ) ) )
309 243 248 250 258 308 syl13anc 
 |-  ( ( ( ( ( ( ( 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 ) <_ ( ( ( 1st ` ( g ` b ) ) C x ) +e ( x C w ) ) )
310 309 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) <_ ( ( ( 1st ` ( g ` b ) ) C x ) +e ( x C w ) ) )
311 rexadd 
 |-  ( ( ( ( 1st ` ( g ` b ) ) C x ) e. RR /\ ( x C w ) e. RR ) -> ( ( ( 1st ` ( g ` b ) ) C x ) +e ( x C w ) ) = ( ( ( 1st ` ( g ` b ) ) C x ) + ( x C w ) ) )
312 287 302 311 syl2anc 
 |-  ( ( ( ( ( ( ( ( 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 x ) +e ( x C w ) ) = ( ( ( 1st ` ( g ` b ) ) C x ) + ( x C w ) ) )
313 310 312 breqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) <_ ( ( ( 1st ` ( g ` b ) ) C x ) + ( x C w ) ) )
314 257 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) -> ( 2nd ` ( g ` b ) ) e. RR )
315 273 adantr 
 |-  ( ( ( ( ( ( ( ( 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 x ) < ( 2nd ` ( g ` b ) ) )
316 simpr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) ) -> ( x C w ) < ( 2nd ` ( g ` b ) ) )
317 287 302 314 314 315 316 lt2addd 
 |-  ( ( ( ( ( ( ( ( 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 x ) + ( x C w ) ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) )
318 253 304 307 313 317 xrlelttrd 
 |-  ( ( ( ( ( ( ( ( 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 ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) )
319 318 ex 
 |-  ( ( ( ( ( ( ( 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 ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) ) )
320 254 rpred 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) e. RR )
321 320 254 ltaddrpd 
 |-  ( ( g : s --> ( X X. RR+ ) /\ b e. s ) -> ( 2nd ` ( g ` b ) ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) )
322 244 227 321 syl2an 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( 2nd ` ( g ` b ) ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) )
323 260 262 306 273 322 xrlttrd 
 |-  ( ( ( ( ( ( ( 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 x ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) )
324 319 323 jctild 
 |-  ( ( ( ( ( ( ( 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 x ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) /\ ( ( 1st ` ( g ` b ) ) C w ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) ) ) )
325 242 324 syld 
 |-  ( ( ( ( ( ( ( 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 , < ) -> ( ( ( 1st ` ( g ` b ) ) C x ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) /\ ( ( 1st ` ( g ` b ) ) C w ) < ( ( 2nd ` ( g ` b ) ) + ( 2nd ` ( g ` b ) ) ) ) ) )
326 simpll 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) -> ( ph /\ f : X --> Y ) )
327 ffvelrn 
 |-  ( ( f : X --> Y /\ x e. X ) -> ( f ` x ) e. Y )
328 ffvelrn 
 |-  ( ( f : X --> Y /\ w e. X ) -> ( f ` w ) e. Y )
329 327 328 anim12dan 
 |-  ( ( f : X --> Y /\ ( x e. X /\ w e. X ) ) -> ( ( f ` x ) e. Y /\ ( f ` w ) e. Y ) )
330 xmetcl 
 |-  ( ( D e. ( *Met ` Y ) /\ ( f ` x ) e. Y /\ ( f ` w ) e. Y ) -> ( ( f ` x ) D ( f ` w ) ) e. RR* )
331 330 3expb 
 |-  ( ( D e. ( *Met ` Y ) /\ ( ( f ` x ) e. Y /\ ( f ` w ) e. Y ) ) -> ( ( f ` x ) D ( f ` w ) ) e. RR* )
332 2 329 331 syl2an 
 |-  ( ( ph /\ ( f : X --> Y /\ ( x e. X /\ w e. X ) ) ) -> ( ( f ` x ) D ( f ` w ) ) e. RR* )
333 332 anassrs 
 |-  ( ( ( ph /\ f : X --> Y ) /\ ( x e. X /\ w e. X ) ) -> ( ( f ` x ) D ( f ` w ) ) e. RR* )
334 326 333 sylan 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) -> ( ( f ` x ) D ( f ` w ) ) e. RR* )
335 334 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( f ` x ) D ( f ` w ) ) e. RR* )
336 2 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> D e. ( *Met ` Y ) )
337 simp-5r 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> f : X --> Y )
338 337 276 ffvelrnd 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( f ` ( 1st ` ( g ` b ) ) ) e. Y )
339 simpllr 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) -> f : X --> Y )
340 339 ffvelrnda 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ x e. X ) -> ( f ` x ) e. Y )
341 340 adantrr 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) -> ( f ` x ) e. Y )
342 341 adantr 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( f ` x ) e. Y )
343 xmetcl 
 |-  ( ( D e. ( *Met ` Y ) /\ ( f ` ( 1st ` ( g ` b ) ) ) e. Y /\ ( f ` x ) e. Y ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR* )
344 336 338 342 343 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR* )
345 14 rpxrd 
 |-  ( d e. RR+ -> ( d / 2 ) e. RR* )
346 345 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( d / 2 ) e. RR* )
347 xrltle 
 |-  ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR* /\ ( d / 2 ) e. RR* ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) <_ ( d / 2 ) ) )
348 344 346 347 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) <_ ( d / 2 ) ) )
349 xmetge0 
 |-  ( ( D e. ( *Met ` Y ) /\ ( f ` ( 1st ` ( g ` b ) ) ) e. Y /\ ( f ` x ) e. Y ) -> 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) )
350 336 338 342 349 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) )
351 14 rpred 
 |-  ( d e. RR+ -> ( d / 2 ) e. RR )
352 351 ad4antlr 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( d / 2 ) e. RR )
353 xrrege0 
 |-  ( ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR* /\ ( d / 2 ) e. RR ) /\ ( 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) <_ ( d / 2 ) ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR )
354 353 ex 
 |-  ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR* /\ ( d / 2 ) e. RR ) -> ( ( 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) <_ ( d / 2 ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR ) )
355 344 352 354 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) <_ ( d / 2 ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR ) )
356 350 355 mpand 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) <_ ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR ) )
357 348 356 syld 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR ) )
358 357 ad2ant2r 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR ) )
359 358 imp 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR )
360 339 ffvelrnda 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ w e. X ) -> ( f ` w ) e. Y )
361 360 adantrl 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) -> ( f ` w ) e. Y )
362 361 adantr 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( f ` w ) e. Y )
363 xmetcl 
 |-  ( ( D e. ( *Met ` Y ) /\ ( f ` ( 1st ` ( g ` b ) ) ) e. Y /\ ( f ` w ) e. Y ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR* )
364 336 338 362 363 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR* )
365 xrltle 
 |-  ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR* /\ ( d / 2 ) e. RR* ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) <_ ( d / 2 ) ) )
366 364 346 365 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) <_ ( d / 2 ) ) )
367 xmetge0 
 |-  ( ( D e. ( *Met ` Y ) /\ ( f ` ( 1st ` ( g ` b ) ) ) e. Y /\ ( f ` w ) e. Y ) -> 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) )
368 336 338 362 367 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) )
369 xrrege0 
 |-  ( ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR* /\ ( d / 2 ) e. RR ) /\ ( 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) <_ ( d / 2 ) ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR )
370 369 ex 
 |-  ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR* /\ ( d / 2 ) e. RR ) -> ( ( 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) <_ ( d / 2 ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) )
371 364 352 370 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( 0 <_ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) <_ ( d / 2 ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) )
372 368 371 mpand 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) <_ ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) )
373 366 372 syld 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) )
374 373 ad2ant2r 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) )
375 374 imp 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR )
376 readdcl 
 |-  ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) e. RR )
377 359 375 376 syl2an 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) ) /\ ( ( ( ( ( ( ( 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 ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) e. RR )
378 377 anandis 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) e. RR )
379 378 rexrd 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) e. RR* )
380 rpxr 
 |-  ( d e. RR+ -> d e. RR* )
381 380 ad6antlr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> d e. RR* )
382 xmettri 
 |-  ( ( D e. ( *Met ` Y ) /\ ( ( f ` x ) e. Y /\ ( f ` w ) e. Y /\ ( f ` ( 1st ` ( g ` b ) ) ) e. Y ) ) -> ( ( f ` x ) D ( f ` w ) ) <_ ( ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
383 336 342 362 338 382 syl13anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( f ` x ) D ( f ` w ) ) <_ ( ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
384 383 ad2ant2r 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( f ` x ) D ( f ` w ) ) <_ ( ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
385 384 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( f ` x ) D ( f ` w ) ) <_ ( ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
386 xmetsym 
 |-  ( ( D e. ( *Met ` Y ) /\ ( f ` x ) e. Y /\ ( f ` ( 1st ` ( g ` b ) ) ) e. Y ) -> ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) = ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) )
387 336 342 338 386 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) = ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) )
388 387 ad2ant2r 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) = ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) )
389 388 adantr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) = ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) )
390 389 oveq1d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) = ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
391 rexadd 
 |-  ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) = ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
392 359 375 391 syl2an 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) ) /\ ( ( ( ( ( ( ( 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 ) ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) = ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
393 392 anandis 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) = ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
394 390 393 eqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` x ) D ( f ` ( 1st ` ( g ` b ) ) ) ) +e ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) = ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
395 385 394 breqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( f ` x ) D ( f ` w ) ) <_ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) )
396 lt2add 
 |-  ( ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) /\ ( ( d / 2 ) e. RR /\ ( d / 2 ) e. RR ) ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < ( ( d / 2 ) + ( d / 2 ) ) ) )
397 396 expcom 
 |-  ( ( ( d / 2 ) e. RR /\ ( d / 2 ) e. RR ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < ( ( d / 2 ) + ( d / 2 ) ) ) ) )
398 352 352 397 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) e. RR /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) e. RR ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < ( ( d / 2 ) + ( d / 2 ) ) ) ) )
399 357 373 398 syl2and 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < ( ( d / 2 ) + ( d / 2 ) ) ) ) )
400 399 pm2.43d 
 |-  ( ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ g : s --> ( X X. RR+ ) ) /\ ( x e. X /\ w e. X ) ) /\ b e. s ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < ( ( d / 2 ) + ( d / 2 ) ) ) )
401 400 ad2ant2r 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < ( ( d / 2 ) + ( d / 2 ) ) ) )
402 401 imp 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < ( ( d / 2 ) + ( d / 2 ) ) )
403 rpcn 
 |-  ( d e. RR+ -> d e. CC )
404 403 2halvesd 
 |-  ( d e. RR+ -> ( ( d / 2 ) + ( d / 2 ) ) = d )
405 404 ad6antlr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( d / 2 ) + ( d / 2 ) ) = d )
406 402 405 breqtrd 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) + ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) ) < d )
407 335 379 381 395 406 xrlelttrd 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) ) -> ( ( f ` x ) D ( f ` w ) ) < d )
408 407 ex 
 |-  ( ( ( ( ( ( ( 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 ) ) -> ( ( ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` x ) ) < ( d / 2 ) /\ ( ( f ` ( 1st ` ( g ` b ) ) ) D ( f ` w ) ) < ( d / 2 ) ) -> ( ( f ` x ) D ( f ` w ) ) < d ) )
409 325 408 imim12d 
 |-  ( ( ( ( ( ( ( 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 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 ) ) ) -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
410 198 409 sylanl1 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) ) ) /\ ( 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 ) ) ) -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
411 410 adantlrr 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) ) -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
412 195 411 mpd 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) )
413 412 exp32 
 |-  ( ( ( ( ( ( ( ( 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 -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) ) )
414 176 413 sylan2 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ ( 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 e. s -> ( x e. b -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) ) )
415 414 expr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ 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 e. s -> ( x e. b -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) ) ) )
416 415 pm2.43d 
 |-  ( ( ( ( ( ( ( ( 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 ) ) /\ 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 -> ( x e. b -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) ) )
417 416 an32s 
 |-  ( ( ( ( ( ( ( ( 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 ) ) -> ( b e. s -> ( x e. b -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) ) )
418 174 175 417 rexlimd 
 |-  ( ( ( ( ( ( ( ( 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 -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
419 169 418 mpd 
 |-  ( ( ( ( ( ( ( ( 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 ) ) -> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) )
420 419 ralrimivva 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) -> A. x e. X A. w e. X ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) )
421 breq2 
 |-  ( z = inf ( ran ran g , RR , < ) -> ( ( x C w ) < z <-> ( x C w ) < inf ( ran ran g , RR , < ) ) )
422 421 imbi1d 
 |-  ( z = inf ( ran ran g , RR , < ) -> ( ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) <-> ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
423 422 2ralbidv 
 |-  ( z = inf ( ran ran g , RR , < ) -> ( 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 ) < inf ( ran ran g , RR , < ) -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
424 423 rspcev 
 |-  ( ( inf ( ran ran g , RR , < ) e. RR+ /\ A. x e. X A. w e. X ( ( x C w ) < inf ( ran ran g , RR , < ) -> ( ( 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 ) ) < d ) )
425 160 420 424 syl2anc 
 |-  ( ( ( ( ( ( ( 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 ) ) ) ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) )
426 425 expl 
 |-  ( ( ( ( ( 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 ) ) ) ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
427 426 exlimdv 
 |-  ( ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ s e. 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 ) ) ) ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
428 427 expimpd 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ s e. 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 ) ) ) ) ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
429 105 428 sylan2 
 |-  ( ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) /\ 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 ) ) ) ) ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
430 429 rexlimdva 
 |-  ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) -> ( 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 ) ) ) ) ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
431 104 430 syld 
 |-  ( ( ( 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. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
432 20 431 syl5 
 |-  ( ( ( ph /\ f : X --> Y ) /\ d e. RR+ ) -> ( ( ( 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 ) ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
433 432 exp4b 
 |-  ( ( ph /\ f : X --> Y ) -> ( d e. RR+ -> ( ( 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 ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) ) ) )
434 14 433 mpdi 
 |-  ( ( ph /\ f : X --> Y ) -> ( d 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 ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) ) )
435 434 ralrimiv 
 |-  ( ( ph /\ f : X --> Y ) -> A. d 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 ) -> E. z e. RR+ A. x e. X A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < d ) ) )
436 r19.21v 
 |-  ( A. d 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 ) -> 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 ) -> 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 ) ) )
437 435 436 sylib 
 |-  ( ( ph /\ f : X --> 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 ) -> 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 ) ) )
438 13 437 impbid2 
 |-  ( ( ph /\ f : X --> Y ) -> ( 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 ) ) )
439 ralcom 
 |-  ( 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 A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) )
440 438 439 bitrdi 
 |-  ( ( ph /\ f : X --> Y ) -> ( 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. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) )
441 440 pm5.32da 
 |-  ( ph -> ( ( f : X --> Y /\ 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 ) ) <-> ( f : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) ) )
442 eqid 
 |-  ( metUnif ` C ) = ( metUnif ` C )
443 eqid 
 |-  ( metUnif ` D ) = ( metUnif ` D )
444 xmetpsmet 
 |-  ( C e. ( *Met ` X ) -> C e. ( PsMet ` X ) )
445 1 444 syl 
 |-  ( ph -> C e. ( PsMet ` X ) )
446 xmetpsmet 
 |-  ( D e. ( *Met ` Y ) -> D e. ( PsMet ` Y ) )
447 2 446 syl 
 |-  ( ph -> D e. ( PsMet ` Y ) )
448 442 443 4 5 445 447 metucn 
 |-  ( ph -> ( f e. ( ( metUnif ` C ) uCn ( metUnif ` D ) ) <-> ( f : X --> Y /\ 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 ) ) ) )
449 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
450 26 449 metcn 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( f e. ( ( MetOpen ` C ) Cn ( MetOpen ` D ) ) <-> ( f : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) ) )
451 1 2 450 syl2anc 
 |-  ( ph -> ( f e. ( ( MetOpen ` C ) Cn ( MetOpen ` D ) ) <-> ( f : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( f ` x ) D ( f ` w ) ) < y ) ) ) )
452 441 448 451 3bitr4d 
 |-  ( ph -> ( f e. ( ( metUnif ` C ) uCn ( metUnif ` D ) ) <-> f e. ( ( MetOpen ` C ) Cn ( MetOpen ` D ) ) ) )
453 452 eqrdv 
 |-  ( ph -> ( ( metUnif ` C ) uCn ( metUnif ` D ) ) = ( ( MetOpen ` C ) Cn ( MetOpen ` D ) ) )