Metamath Proof Explorer

Theorem tgioo

Description: The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypotheses remet.1 
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
tgioo.2 
|- J = ( MetOpen ` D )
Assertion tgioo 
|- ( topGen ` ran (,) ) = J

Proof

Step Hyp Ref Expression
1 remet.1 
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
2 tgioo.2 
 |-  J = ( MetOpen ` D )
3 1 rexmet 
 |-  D e. ( *Met ` RR )
4 2 mopnval 
 |-  ( D e. ( *Met ` RR ) -> J = ( topGen ` ran ( ball ` D ) ) )
5 3 4 ax-mp 
 |-  J = ( topGen ` ran ( ball ` D ) )
6 1 blssioo 
 |-  ran ( ball ` D ) C_ ran (,)
7 elssuni 
 |-  ( v e. ran (,) -> v C_ U. ran (,) )
8 unirnioo 
 |-  RR = U. ran (,)
9 7 8 sseqtrrdi 
 |-  ( v e. ran (,) -> v C_ RR )
10 retopbas 
 |-  ran (,) e. TopBases
11 10 a1i 
 |-  ( ( v e. ran (,) /\ x e. v ) -> ran (,) e. TopBases )
12 simpl 
 |-  ( ( v e. ran (,) /\ x e. v ) -> v e. ran (,) )
13 9 sselda 
 |-  ( ( v e. ran (,) /\ x e. v ) -> x e. RR )
14 1re 
 |-  1 e. RR
15 1 bl2ioo 
 |-  ( ( x e. RR /\ 1 e. RR ) -> ( x ( ball ` D ) 1 ) = ( ( x - 1 ) (,) ( x + 1 ) ) )
16 14 15 mpan2 
 |-  ( x e. RR -> ( x ( ball ` D ) 1 ) = ( ( x - 1 ) (,) ( x + 1 ) ) )
17 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
18 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
19 17 18 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
20 peano2rem 
 |-  ( x e. RR -> ( x - 1 ) e. RR )
21 20 rexrd 
 |-  ( x e. RR -> ( x - 1 ) e. RR* )
22 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
23 22 rexrd 
 |-  ( x e. RR -> ( x + 1 ) e. RR* )
24 fnovrn 
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ ( x - 1 ) e. RR* /\ ( x + 1 ) e. RR* ) -> ( ( x - 1 ) (,) ( x + 1 ) ) e. ran (,) )
25 19 21 23 24 mp3an2i 
 |-  ( x e. RR -> ( ( x - 1 ) (,) ( x + 1 ) ) e. ran (,) )
26 16 25 eqeltrd 
 |-  ( x e. RR -> ( x ( ball ` D ) 1 ) e. ran (,) )
27 13 26 syl 
 |-  ( ( v e. ran (,) /\ x e. v ) -> ( x ( ball ` D ) 1 ) e. ran (,) )
28 simpr 
 |-  ( ( v e. ran (,) /\ x e. v ) -> x e. v )
29 1rp 
 |-  1 e. RR+
30 blcntr 
 |-  ( ( D e. ( *Met ` RR ) /\ x e. RR /\ 1 e. RR+ ) -> x e. ( x ( ball ` D ) 1 ) )
31 3 29 30 mp3an13 
 |-  ( x e. RR -> x e. ( x ( ball ` D ) 1 ) )
32 13 31 syl 
 |-  ( ( v e. ran (,) /\ x e. v ) -> x e. ( x ( ball ` D ) 1 ) )
33 28 32 elind 
 |-  ( ( v e. ran (,) /\ x e. v ) -> x e. ( v i^i ( x ( ball ` D ) 1 ) ) )
34 basis2 
 |-  ( ( ( ran (,) e. TopBases /\ v e. ran (,) ) /\ ( ( x ( ball ` D ) 1 ) e. ran (,) /\ x e. ( v i^i ( x ( ball ` D ) 1 ) ) ) ) -> E. z e. ran (,) ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) )
35 11 12 27 33 34 syl22anc 
 |-  ( ( v e. ran (,) /\ x e. v ) -> E. z e. ran (,) ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) )
36 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( z e. ran (,) <-> E. a e. RR* E. b e. RR* z = ( a (,) b ) ) )
37 19 36 ax-mp 
 |-  ( z e. ran (,) <-> E. a e. RR* E. b e. RR* z = ( a (,) b ) )
38 eleq2 
 |-  ( z = ( a (,) b ) -> ( x e. z <-> x e. ( a (,) b ) ) )
39 sseq1 
 |-  ( z = ( a (,) b ) -> ( z C_ ( v i^i ( x ( ball ` D ) 1 ) ) <-> ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) )
40 38 39 anbi12d 
 |-  ( z = ( a (,) b ) -> ( ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) <-> ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) ) )
41 inss2 
 |-  ( v i^i ( x ( ball ` D ) 1 ) ) C_ ( x ( ball ` D ) 1 )
42 sstr 
 |-  ( ( ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) /\ ( v i^i ( x ( ball ` D ) 1 ) ) C_ ( x ( ball ` D ) 1 ) ) -> ( a (,) b ) C_ ( x ( ball ` D ) 1 ) )
43 41 42 mpan2 
 |-  ( ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) -> ( a (,) b ) C_ ( x ( ball ` D ) 1 ) )
44 43 adantl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( a (,) b ) C_ ( x ( ball ` D ) 1 ) )
45 elioore 
 |-  ( x e. ( a (,) b ) -> x e. RR )
46 45 adantr 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> x e. RR )
47 46 16 syl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( x ( ball ` D ) 1 ) = ( ( x - 1 ) (,) ( x + 1 ) ) )
48 44 47 sseqtrd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( a (,) b ) C_ ( ( x - 1 ) (,) ( x + 1 ) ) )
49 dfss 
 |-  ( ( a (,) b ) C_ ( ( x - 1 ) (,) ( x + 1 ) ) <-> ( a (,) b ) = ( ( a (,) b ) i^i ( ( x - 1 ) (,) ( x + 1 ) ) ) )
50 48 49 sylib 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( a (,) b ) = ( ( a (,) b ) i^i ( ( x - 1 ) (,) ( x + 1 ) ) ) )
51 eliooxr 
 |-  ( x e. ( a (,) b ) -> ( a e. RR* /\ b e. RR* ) )
52 21 23 jca 
 |-  ( x e. RR -> ( ( x - 1 ) e. RR* /\ ( x + 1 ) e. RR* ) )
53 45 52 syl 
 |-  ( x e. ( a (,) b ) -> ( ( x - 1 ) e. RR* /\ ( x + 1 ) e. RR* ) )
54 iooin 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( x - 1 ) e. RR* /\ ( x + 1 ) e. RR* ) ) -> ( ( a (,) b ) i^i ( ( x - 1 ) (,) ( x + 1 ) ) ) = ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) )
55 51 53 54 syl2anc 
 |-  ( x e. ( a (,) b ) -> ( ( a (,) b ) i^i ( ( x - 1 ) (,) ( x + 1 ) ) ) = ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) )
56 55 adantr 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( ( a (,) b ) i^i ( ( x - 1 ) (,) ( x + 1 ) ) ) = ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) )
57 50 56 eqtrd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( a (,) b ) = ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) )
58 mnfxr 
 |-  -oo e. RR*
59 58 a1i 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> -oo e. RR* )
60 46 21 syl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( x - 1 ) e. RR* )
61 51 adantr 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( a e. RR* /\ b e. RR* ) )
62 61 simpld 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> a e. RR* )
63 60 62 ifcld 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR* )
64 61 simprd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> b e. RR* )
65 46 22 syl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( x + 1 ) e. RR )
66 65 rexrd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( x + 1 ) e. RR* )
67 64 66 ifcld 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR* )
68 45 20 syl 
 |-  ( x e. ( a (,) b ) -> ( x - 1 ) e. RR )
69 68 adantr 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( x - 1 ) e. RR )
70 69 mnfltd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> -oo < ( x - 1 ) )
71 xrmax2 
 |-  ( ( a e. RR* /\ ( x - 1 ) e. RR* ) -> ( x - 1 ) <_ if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) )
72 62 60 71 syl2anc 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( x - 1 ) <_ if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) )
73 59 60 63 70 72 xrltletrd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> -oo < if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) )
74 simpl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> x e. ( a (,) b ) )
75 74 57 eleqtrd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> x e. ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) )
76 eliooxr 
 |-  ( x e. ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) -> ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR* /\ if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR* ) )
77 ne0i 
 |-  ( x e. ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) -> ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) =/= (/) )
78 ioon0 
 |-  ( ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR* /\ if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR* ) -> ( ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) =/= (/) <-> if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) < if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) )
79 77 78 syl5ib 
 |-  ( ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR* /\ if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR* ) -> ( x e. ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) -> if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) < if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) )
80 76 79 mpcom 
 |-  ( x e. ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) -> if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) < if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) )
81 75 80 syl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) < if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) )
82 xrre2 
 |-  ( ( ( -oo e. RR* /\ if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR* /\ if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR* ) /\ ( -oo < if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) /\ if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) < if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) ) -> if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR )
83 59 63 67 73 81 82 syl32anc 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR )
84 mnfle 
 |-  ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR* -> -oo <_ if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) )
85 63 84 syl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> -oo <_ if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) )
86 59 63 67 85 81 xrlelttrd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> -oo < if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) )
87 xrmin2 
 |-  ( ( b e. RR* /\ ( x + 1 ) e. RR* ) -> if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) <_ ( x + 1 ) )
88 64 66 87 syl2anc 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) <_ ( x + 1 ) )
89 xrre 
 |-  ( ( ( if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR* /\ ( x + 1 ) e. RR ) /\ ( -oo < if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) /\ if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) <_ ( x + 1 ) ) ) -> if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR )
90 67 65 86 88 89 syl22anc 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR )
91 1 ioo2blex 
 |-  ( ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) e. RR /\ if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) e. RR ) -> ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) e. ran ( ball ` D ) )
92 83 90 91 syl2anc 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( if ( a <_ ( x - 1 ) , ( x - 1 ) , a ) (,) if ( b <_ ( x + 1 ) , b , ( x + 1 ) ) ) e. ran ( ball ` D ) )
93 57 92 eqeltrd 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( a (,) b ) e. ran ( ball ` D ) )
94 inss1 
 |-  ( v i^i ( x ( ball ` D ) 1 ) ) C_ v
95 sstr 
 |-  ( ( ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) /\ ( v i^i ( x ( ball ` D ) 1 ) ) C_ v ) -> ( a (,) b ) C_ v )
96 94 95 mpan2 
 |-  ( ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) -> ( a (,) b ) C_ v )
97 96 adantl 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( a (,) b ) C_ v )
98 sseq1 
 |-  ( z = ( a (,) b ) -> ( z C_ v <-> ( a (,) b ) C_ v ) )
99 38 98 anbi12d 
 |-  ( z = ( a (,) b ) -> ( ( x e. z /\ z C_ v ) <-> ( x e. ( a (,) b ) /\ ( a (,) b ) C_ v ) ) )
100 99 rspcev 
 |-  ( ( ( a (,) b ) e. ran ( ball ` D ) /\ ( x e. ( a (,) b ) /\ ( a (,) b ) C_ v ) ) -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ v ) )
101 93 74 97 100 syl12anc 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ v ) )
102 blssex 
 |-  ( ( D e. ( *Met ` RR ) /\ x e. RR ) -> ( E. z e. ran ( ball ` D ) ( x e. z /\ z C_ v ) <-> E. y e. RR+ ( x ( ball ` D ) y ) C_ v ) )
103 3 46 102 sylancr 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> ( E. z e. ran ( ball ` D ) ( x e. z /\ z C_ v ) <-> E. y e. RR+ ( x ( ball ` D ) y ) C_ v ) )
104 101 103 mpbid 
 |-  ( ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v )
105 40 104 syl6bi 
 |-  ( z = ( a (,) b ) -> ( ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v ) )
106 105 a1i 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( z = ( a (,) b ) -> ( ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v ) ) )
107 106 rexlimivv 
 |-  ( E. a e. RR* E. b e. RR* z = ( a (,) b ) -> ( ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v ) )
108 107 imp 
 |-  ( ( E. a e. RR* E. b e. RR* z = ( a (,) b ) /\ ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v )
109 37 108 sylanb 
 |-  ( ( z e. ran (,) /\ ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v )
110 109 rexlimiva 
 |-  ( E. z e. ran (,) ( x e. z /\ z C_ ( v i^i ( x ( ball ` D ) 1 ) ) ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v )
111 35 110 syl 
 |-  ( ( v e. ran (,) /\ x e. v ) -> E. y e. RR+ ( x ( ball ` D ) y ) C_ v )
112 111 ralrimiva 
 |-  ( v e. ran (,) -> A. x e. v E. y e. RR+ ( x ( ball ` D ) y ) C_ v )
113 2 elmopn2 
 |-  ( D e. ( *Met ` RR ) -> ( v e. J <-> ( v C_ RR /\ A. x e. v E. y e. RR+ ( x ( ball ` D ) y ) C_ v ) ) )
114 3 113 ax-mp 
 |-  ( v e. J <-> ( v C_ RR /\ A. x e. v E. y e. RR+ ( x ( ball ` D ) y ) C_ v ) )
115 9 112 114 sylanbrc 
 |-  ( v e. ran (,) -> v e. J )
116 115 ssriv 
 |-  ran (,) C_ J
117 116 5 sseqtri 
 |-  ran (,) C_ ( topGen ` ran ( ball ` D ) )
118 2basgen 
 |-  ( ( ran ( ball ` D ) C_ ran (,) /\ ran (,) C_ ( topGen ` ran ( ball ` D ) ) ) -> ( topGen ` ran ( ball ` D ) ) = ( topGen ` ran (,) ) )
119 6 117 118 mp2an 
 |-  ( topGen ` ran ( ball ` D ) ) = ( topGen ` ran (,) )
120 5 119 eqtr2i 
 |-  ( topGen ` ran (,) ) = J