Metamath Proof Explorer


Theorem prdsxmslem2

Description: Lemma for prdsxms . The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses prdsxms.y
|- Y = ( S Xs_ R )
prdsxms.s
|- ( ph -> S e. W )
prdsxms.i
|- ( ph -> I e. Fin )
prdsxms.d
|- D = ( dist ` Y )
prdsxms.b
|- B = ( Base ` Y )
prdsxms.r
|- ( ph -> R : I --> *MetSp )
prdsxms.j
|- J = ( TopOpen ` Y )
prdsxms.v
|- V = ( Base ` ( R ` k ) )
prdsxms.e
|- E = ( ( dist ` ( R ` k ) ) |` ( V X. V ) )
prdsxms.k
|- K = ( TopOpen ` ( R ` k ) )
prdsxms.c
|- C = { x | E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) }
Assertion prdsxmslem2
|- ( ph -> J = ( MetOpen ` D ) )

Proof

Step Hyp Ref Expression
1 prdsxms.y
 |-  Y = ( S Xs_ R )
2 prdsxms.s
 |-  ( ph -> S e. W )
3 prdsxms.i
 |-  ( ph -> I e. Fin )
4 prdsxms.d
 |-  D = ( dist ` Y )
5 prdsxms.b
 |-  B = ( Base ` Y )
6 prdsxms.r
 |-  ( ph -> R : I --> *MetSp )
7 prdsxms.j
 |-  J = ( TopOpen ` Y )
8 prdsxms.v
 |-  V = ( Base ` ( R ` k ) )
9 prdsxms.e
 |-  E = ( ( dist ` ( R ` k ) ) |` ( V X. V ) )
10 prdsxms.k
 |-  K = ( TopOpen ` ( R ` k ) )
11 prdsxms.c
 |-  C = { x | E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) }
12 topnfn
 |-  TopOpen Fn _V
13 6 ffnd
 |-  ( ph -> R Fn I )
14 dffn2
 |-  ( R Fn I <-> R : I --> _V )
15 13 14 sylib
 |-  ( ph -> R : I --> _V )
16 fnfco
 |-  ( ( TopOpen Fn _V /\ R : I --> _V ) -> ( TopOpen o. R ) Fn I )
17 12 15 16 sylancr
 |-  ( ph -> ( TopOpen o. R ) Fn I )
18 11 ptval
 |-  ( ( I e. Fin /\ ( TopOpen o. R ) Fn I ) -> ( Xt_ ` ( TopOpen o. R ) ) = ( topGen ` C ) )
19 3 17 18 syl2anc
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( topGen ` C ) )
20 eldifsn
 |-  ( x e. ( ran ( ball ` D ) \ { (/) } ) <-> ( x e. ran ( ball ` D ) /\ x =/= (/) ) )
21 1 2 3 4 5 6 prdsxmslem1
 |-  ( ph -> D e. ( *Met ` B ) )
22 blrn
 |-  ( D e. ( *Met ` B ) -> ( x e. ran ( ball ` D ) <-> E. p e. B E. r e. RR* x = ( p ( ball ` D ) r ) ) )
23 21 22 syl
 |-  ( ph -> ( x e. ran ( ball ` D ) <-> E. p e. B E. r e. RR* x = ( p ( ball ` D ) r ) ) )
24 21 adantr
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> D e. ( *Met ` B ) )
25 simprl
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> p e. B )
26 simprr
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> r e. RR* )
27 xbln0
 |-  ( ( D e. ( *Met ` B ) /\ p e. B /\ r e. RR* ) -> ( ( p ( ball ` D ) r ) =/= (/) <-> 0 < r ) )
28 24 25 26 27 syl3anc
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> ( ( p ( ball ` D ) r ) =/= (/) <-> 0 < r ) )
29 3 3ad2ant1
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> I e. Fin )
30 29 mptexd
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) e. _V )
31 ovex
 |-  ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) e. _V
32 31 rgenw
 |-  A. n e. I ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) e. _V
33 eqid
 |-  ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) )
34 33 fnmpt
 |-  ( A. n e. I ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) e. _V -> ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) Fn I )
35 32 34 mp1i
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) Fn I )
36 6 3ad2ant1
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> R : I --> *MetSp )
37 36 ffvelrnda
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> ( R ` k ) e. *MetSp )
38 8 9 xmsxmet
 |-  ( ( R ` k ) e. *MetSp -> E e. ( *Met ` V ) )
39 37 38 syl
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> E e. ( *Met ` V ) )
40 eqid
 |-  ( S Xs_ ( k e. I |-> ( R ` k ) ) ) = ( S Xs_ ( k e. I |-> ( R ` k ) ) )
41 eqid
 |-  ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) = ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) )
42 2 3ad2ant1
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> S e. W )
43 37 ralrimiva
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> A. k e. I ( R ` k ) e. *MetSp )
44 simp2l
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> p e. B )
45 36 feqmptd
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> R = ( k e. I |-> ( R ` k ) ) )
46 45 oveq2d
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( S Xs_ R ) = ( S Xs_ ( k e. I |-> ( R ` k ) ) ) )
47 1 46 syl5eq
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> Y = ( S Xs_ ( k e. I |-> ( R ` k ) ) ) )
48 47 fveq2d
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( Base ` Y ) = ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) )
49 5 48 syl5eq
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> B = ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) )
50 44 49 eleqtrd
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> p e. ( Base ` ( S Xs_ ( k e. I |-> ( R ` k ) ) ) ) )
51 40 41 42 29 43 8 50 prdsbascl
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> A. k e. I ( p ` k ) e. V )
52 51 r19.21bi
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> ( p ` k ) e. V )
53 simp2r
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> r e. RR* )
54 53 adantr
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> r e. RR* )
55 eqid
 |-  ( MetOpen ` E ) = ( MetOpen ` E )
56 55 blopn
 |-  ( ( E e. ( *Met ` V ) /\ ( p ` k ) e. V /\ r e. RR* ) -> ( ( p ` k ) ( ball ` E ) r ) e. ( MetOpen ` E ) )
57 39 52 54 56 syl3anc
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> ( ( p ` k ) ( ball ` E ) r ) e. ( MetOpen ` E ) )
58 2fveq3
 |-  ( n = k -> ( dist ` ( R ` n ) ) = ( dist ` ( R ` k ) ) )
59 2fveq3
 |-  ( n = k -> ( Base ` ( R ` n ) ) = ( Base ` ( R ` k ) ) )
60 59 8 eqtr4di
 |-  ( n = k -> ( Base ` ( R ` n ) ) = V )
61 60 sqxpeqd
 |-  ( n = k -> ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) = ( V X. V ) )
62 58 61 reseq12d
 |-  ( n = k -> ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) = ( ( dist ` ( R ` k ) ) |` ( V X. V ) ) )
63 62 9 eqtr4di
 |-  ( n = k -> ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) = E )
64 63 fveq2d
 |-  ( n = k -> ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) = ( ball ` E ) )
65 fveq2
 |-  ( n = k -> ( p ` n ) = ( p ` k ) )
66 eqidd
 |-  ( n = k -> r = r )
67 64 65 66 oveq123d
 |-  ( n = k -> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) = ( ( p ` k ) ( ball ` E ) r ) )
68 ovex
 |-  ( ( p ` k ) ( ball ` E ) r ) e. _V
69 67 33 68 fvmpt
 |-  ( k e. I -> ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) = ( ( p ` k ) ( ball ` E ) r ) )
70 69 adantl
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) = ( ( p ` k ) ( ball ` E ) r ) )
71 fvco3
 |-  ( ( R : I --> *MetSp /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) = ( TopOpen ` ( R ` k ) ) )
72 71 10 eqtr4di
 |-  ( ( R : I --> *MetSp /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) = K )
73 36 72 sylan
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) = K )
74 10 8 9 xmstopn
 |-  ( ( R ` k ) e. *MetSp -> K = ( MetOpen ` E ) )
75 37 74 syl
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> K = ( MetOpen ` E ) )
76 73 75 eqtrd
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) = ( MetOpen ` E ) )
77 57 70 76 3eltr4d
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) /\ k e. I ) -> ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) )
78 77 ralrimiva
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> A. k e. I ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) )
79 36 feqmptd
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> R = ( n e. I |-> ( R ` n ) ) )
80 79 oveq2d
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( S Xs_ R ) = ( S Xs_ ( n e. I |-> ( R ` n ) ) ) )
81 1 80 syl5eq
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> Y = ( S Xs_ ( n e. I |-> ( R ` n ) ) ) )
82 81 fveq2d
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( dist ` Y ) = ( dist ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) )
83 4 82 syl5eq
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> D = ( dist ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) )
84 83 fveq2d
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( ball ` D ) = ( ball ` ( dist ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) ) )
85 84 oveqd
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( p ( ball ` D ) r ) = ( p ( ball ` ( dist ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) ) r ) )
86 fveq2
 |-  ( n = k -> ( R ` n ) = ( R ` k ) )
87 86 cbvmptv
 |-  ( n e. I |-> ( R ` n ) ) = ( k e. I |-> ( R ` k ) )
88 87 oveq2i
 |-  ( S Xs_ ( n e. I |-> ( R ` n ) ) ) = ( S Xs_ ( k e. I |-> ( R ` k ) ) )
89 eqid
 |-  ( Base ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) = ( Base ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) )
90 eqid
 |-  ( dist ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) = ( dist ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) )
91 81 fveq2d
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( Base ` Y ) = ( Base ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) )
92 5 91 syl5eq
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> B = ( Base ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) )
93 44 92 eleqtrd
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> p e. ( Base ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) )
94 simp3
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> 0 < r )
95 88 89 8 9 90 42 29 37 39 93 53 94 prdsbl
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( p ( ball ` ( dist ` ( S Xs_ ( n e. I |-> ( R ` n ) ) ) ) ) r ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) )
96 85 95 eqtrd
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> ( p ( ball ` D ) r ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) )
97 fneq1
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> ( g Fn I <-> ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) Fn I ) )
98 fveq1
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> ( g ` k ) = ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) )
99 98 eleq1d
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> ( ( g ` k ) e. ( ( TopOpen o. R ) ` k ) <-> ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) ) )
100 99 ralbidv
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> ( A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) <-> A. k e. I ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) ) )
101 97 100 anbi12d
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) <-> ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) Fn I /\ A. k e. I ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) ) ) )
102 98 69 sylan9eq
 |-  ( ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) /\ k e. I ) -> ( g ` k ) = ( ( p ` k ) ( ball ` E ) r ) )
103 102 ixpeq2dva
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> X_ k e. I ( g ` k ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) )
104 103 eqeq2d
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> ( ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) <-> ( p ( ball ` D ) r ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) ) )
105 101 104 anbi12d
 |-  ( g = ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) -> ( ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) <-> ( ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) Fn I /\ A. k e. I ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) ) ) )
106 105 spcegv
 |-  ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) e. _V -> ( ( ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) Fn I /\ A. k e. I ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) ) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) ) )
107 106 3impib
 |-  ( ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) e. _V /\ ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) Fn I /\ A. k e. I ( ( n e. I |-> ( ( p ` n ) ( ball ` ( ( dist ` ( R ` n ) ) |` ( ( Base ` ( R ` n ) ) X. ( Base ` ( R ` n ) ) ) ) ) r ) ) ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) ) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) )
108 30 35 78 96 107 syl121anc
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) /\ 0 < r ) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) )
109 108 3expia
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> ( 0 < r -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) ) )
110 28 109 sylbid
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> ( ( p ( ball ` D ) r ) =/= (/) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) ) )
111 110 adantr
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) ) /\ x = ( p ( ball ` D ) r ) ) -> ( ( p ( ball ` D ) r ) =/= (/) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) ) )
112 simpr
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) ) /\ x = ( p ( ball ` D ) r ) ) -> x = ( p ( ball ` D ) r ) )
113 112 neeq1d
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) ) /\ x = ( p ( ball ` D ) r ) ) -> ( x =/= (/) <-> ( p ( ball ` D ) r ) =/= (/) ) )
114 df-3an
 |-  ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) <-> ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) )
115 ral0
 |-  A. k e. (/) ( g ` k ) = U. ( ( TopOpen o. R ) ` k )
116 difeq2
 |-  ( z = I -> ( I \ z ) = ( I \ I ) )
117 difid
 |-  ( I \ I ) = (/)
118 116 117 eqtrdi
 |-  ( z = I -> ( I \ z ) = (/) )
119 118 raleqdv
 |-  ( z = I -> ( A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) <-> A. k e. (/) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) )
120 119 rspcev
 |-  ( ( I e. Fin /\ A. k e. (/) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) -> E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) )
121 3 115 120 sylancl
 |-  ( ph -> E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) )
122 121 adantr
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) )
123 122 biantrud
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) <-> ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) ) )
124 114 123 bitr4id
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) <-> ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) ) )
125 eqeq1
 |-  ( x = ( p ( ball ` D ) r ) -> ( x = X_ k e. I ( g ` k ) <-> ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) )
126 124 125 bi2anan9
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) ) /\ x = ( p ( ball ` D ) r ) ) -> ( ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) <-> ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) ) )
127 126 exbidv
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) ) /\ x = ( p ( ball ` D ) r ) ) -> ( E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) <-> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) ) /\ ( p ( ball ` D ) r ) = X_ k e. I ( g ` k ) ) ) )
128 111 113 127 3imtr4d
 |-  ( ( ( ph /\ ( p e. B /\ r e. RR* ) ) /\ x = ( p ( ball ` D ) r ) ) -> ( x =/= (/) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) )
129 128 ex
 |-  ( ( ph /\ ( p e. B /\ r e. RR* ) ) -> ( x = ( p ( ball ` D ) r ) -> ( x =/= (/) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) ) )
130 129 rexlimdvva
 |-  ( ph -> ( E. p e. B E. r e. RR* x = ( p ( ball ` D ) r ) -> ( x =/= (/) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) ) )
131 23 130 sylbid
 |-  ( ph -> ( x e. ran ( ball ` D ) -> ( x =/= (/) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) ) )
132 131 impd
 |-  ( ph -> ( ( x e. ran ( ball ` D ) /\ x =/= (/) ) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) )
133 20 132 syl5bi
 |-  ( ph -> ( x e. ( ran ( ball ` D ) \ { (/) } ) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) )
134 133 alrimiv
 |-  ( ph -> A. x ( x e. ( ran ( ball ` D ) \ { (/) } ) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) )
135 ssab
 |-  ( ( ran ( ball ` D ) \ { (/) } ) C_ { x | E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) } <-> A. x ( x e. ( ran ( ball ` D ) \ { (/) } ) -> E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) ) )
136 134 135 sylibr
 |-  ( ph -> ( ran ( ball ` D ) \ { (/) } ) C_ { x | E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) } )
137 136 11 sseqtrrdi
 |-  ( ph -> ( ran ( ball ` D ) \ { (/) } ) C_ C )
138 ssv
 |-  *MetSp C_ _V
139 fnssres
 |-  ( ( TopOpen Fn _V /\ *MetSp C_ _V ) -> ( TopOpen |` *MetSp ) Fn *MetSp )
140 12 138 139 mp2an
 |-  ( TopOpen |` *MetSp ) Fn *MetSp
141 fvres
 |-  ( x e. *MetSp -> ( ( TopOpen |` *MetSp ) ` x ) = ( TopOpen ` x ) )
142 xmstps
 |-  ( x e. *MetSp -> x e. TopSp )
143 eqid
 |-  ( TopOpen ` x ) = ( TopOpen ` x )
144 143 tpstop
 |-  ( x e. TopSp -> ( TopOpen ` x ) e. Top )
145 142 144 syl
 |-  ( x e. *MetSp -> ( TopOpen ` x ) e. Top )
146 141 145 eqeltrd
 |-  ( x e. *MetSp -> ( ( TopOpen |` *MetSp ) ` x ) e. Top )
147 146 rgen
 |-  A. x e. *MetSp ( ( TopOpen |` *MetSp ) ` x ) e. Top
148 ffnfv
 |-  ( ( TopOpen |` *MetSp ) : *MetSp --> Top <-> ( ( TopOpen |` *MetSp ) Fn *MetSp /\ A. x e. *MetSp ( ( TopOpen |` *MetSp ) ` x ) e. Top ) )
149 140 147 148 mpbir2an
 |-  ( TopOpen |` *MetSp ) : *MetSp --> Top
150 fco2
 |-  ( ( ( TopOpen |` *MetSp ) : *MetSp --> Top /\ R : I --> *MetSp ) -> ( TopOpen o. R ) : I --> Top )
151 149 6 150 sylancr
 |-  ( ph -> ( TopOpen o. R ) : I --> Top )
152 eqid
 |-  X_ n e. I U. ( ( TopOpen o. R ) ` n ) = X_ n e. I U. ( ( TopOpen o. R ) ` n )
153 11 152 ptbasfi
 |-  ( ( I e. Fin /\ ( TopOpen o. R ) : I --> Top ) -> C = ( fi ` ( { X_ n e. I U. ( ( TopOpen o. R ) ` n ) } u. ran ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) ) ) )
154 3 151 153 syl2anc
 |-  ( ph -> C = ( fi ` ( { X_ n e. I U. ( ( TopOpen o. R ) ` n ) } u. ran ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) ) ) )
155 eqid
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
156 155 mopntop
 |-  ( D e. ( *Met ` B ) -> ( MetOpen ` D ) e. Top )
157 21 156 syl
 |-  ( ph -> ( MetOpen ` D ) e. Top )
158 1 5 2 3 13 prdsbas2
 |-  ( ph -> B = X_ k e. I ( Base ` ( R ` k ) ) )
159 6 72 sylan
 |-  ( ( ph /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) = K )
160 6 ffvelrnda
 |-  ( ( ph /\ k e. I ) -> ( R ` k ) e. *MetSp )
161 xmstps
 |-  ( ( R ` k ) e. *MetSp -> ( R ` k ) e. TopSp )
162 160 161 syl
 |-  ( ( ph /\ k e. I ) -> ( R ` k ) e. TopSp )
163 8 10 istps
 |-  ( ( R ` k ) e. TopSp <-> K e. ( TopOn ` V ) )
164 162 163 sylib
 |-  ( ( ph /\ k e. I ) -> K e. ( TopOn ` V ) )
165 159 164 eqeltrd
 |-  ( ( ph /\ k e. I ) -> ( ( TopOpen o. R ) ` k ) e. ( TopOn ` V ) )
166 toponuni
 |-  ( ( ( TopOpen o. R ) ` k ) e. ( TopOn ` V ) -> V = U. ( ( TopOpen o. R ) ` k ) )
167 165 166 syl
 |-  ( ( ph /\ k e. I ) -> V = U. ( ( TopOpen o. R ) ` k ) )
168 8 167 eqtr3id
 |-  ( ( ph /\ k e. I ) -> ( Base ` ( R ` k ) ) = U. ( ( TopOpen o. R ) ` k ) )
169 168 ixpeq2dva
 |-  ( ph -> X_ k e. I ( Base ` ( R ` k ) ) = X_ k e. I U. ( ( TopOpen o. R ) ` k ) )
170 158 169 eqtrd
 |-  ( ph -> B = X_ k e. I U. ( ( TopOpen o. R ) ` k ) )
171 fveq2
 |-  ( k = n -> ( ( TopOpen o. R ) ` k ) = ( ( TopOpen o. R ) ` n ) )
172 171 unieqd
 |-  ( k = n -> U. ( ( TopOpen o. R ) ` k ) = U. ( ( TopOpen o. R ) ` n ) )
173 172 cbvixpv
 |-  X_ k e. I U. ( ( TopOpen o. R ) ` k ) = X_ n e. I U. ( ( TopOpen o. R ) ` n )
174 170 173 eqtrdi
 |-  ( ph -> B = X_ n e. I U. ( ( TopOpen o. R ) ` n ) )
175 155 mopntopon
 |-  ( D e. ( *Met ` B ) -> ( MetOpen ` D ) e. ( TopOn ` B ) )
176 21 175 syl
 |-  ( ph -> ( MetOpen ` D ) e. ( TopOn ` B ) )
177 toponmax
 |-  ( ( MetOpen ` D ) e. ( TopOn ` B ) -> B e. ( MetOpen ` D ) )
178 176 177 syl
 |-  ( ph -> B e. ( MetOpen ` D ) )
179 174 178 eqeltrrd
 |-  ( ph -> X_ n e. I U. ( ( TopOpen o. R ) ` n ) e. ( MetOpen ` D ) )
180 179 snssd
 |-  ( ph -> { X_ n e. I U. ( ( TopOpen o. R ) ` n ) } C_ ( MetOpen ` D ) )
181 174 mpteq1d
 |-  ( ph -> ( w e. B |-> ( w ` k ) ) = ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) )
182 181 ad2antrr
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( w e. B |-> ( w ` k ) ) = ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) )
183 182 cnveqd
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> `' ( w e. B |-> ( w ` k ) ) = `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) )
184 183 imaeq1d
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( `' ( w e. B |-> ( w ` k ) ) " u ) = ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) )
185 fveq1
 |-  ( w = p -> ( w ` k ) = ( p ` k ) )
186 185 eleq1d
 |-  ( w = p -> ( ( w ` k ) e. u <-> ( p ` k ) e. u ) )
187 eqid
 |-  ( w e. B |-> ( w ` k ) ) = ( w e. B |-> ( w ` k ) )
188 187 mptpreima
 |-  ( `' ( w e. B |-> ( w ` k ) ) " u ) = { w e. B | ( w ` k ) e. u }
189 186 188 elrab2
 |-  ( p e. ( `' ( w e. B |-> ( w ` k ) ) " u ) <-> ( p e. B /\ ( p ` k ) e. u ) )
190 160 38 syl
 |-  ( ( ph /\ k e. I ) -> E e. ( *Met ` V ) )
191 190 adantr
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> E e. ( *Met ` V ) )
192 simprl
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> u e. K )
193 160 74 syl
 |-  ( ( ph /\ k e. I ) -> K = ( MetOpen ` E ) )
194 193 adantr
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> K = ( MetOpen ` E ) )
195 192 194 eleqtrd
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> u e. ( MetOpen ` E ) )
196 simprrr
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> ( p ` k ) e. u )
197 55 mopni2
 |-  ( ( E e. ( *Met ` V ) /\ u e. ( MetOpen ` E ) /\ ( p ` k ) e. u ) -> E. r e. RR+ ( ( p ` k ) ( ball ` E ) r ) C_ u )
198 191 195 196 197 syl3anc
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> E. r e. RR+ ( ( p ` k ) ( ball ` E ) r ) C_ u )
199 21 ad3antrrr
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> D e. ( *Met ` B ) )
200 simprrl
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> p e. B )
201 200 adantr
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> p e. B )
202 rpxr
 |-  ( r e. RR+ -> r e. RR* )
203 202 ad2antrl
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> r e. RR* )
204 155 blopn
 |-  ( ( D e. ( *Met ` B ) /\ p e. B /\ r e. RR* ) -> ( p ( ball ` D ) r ) e. ( MetOpen ` D ) )
205 199 201 203 204 syl3anc
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> ( p ( ball ` D ) r ) e. ( MetOpen ` D ) )
206 simprl
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> r e. RR+ )
207 blcntr
 |-  ( ( D e. ( *Met ` B ) /\ p e. B /\ r e. RR+ ) -> p e. ( p ( ball ` D ) r ) )
208 199 201 206 207 syl3anc
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> p e. ( p ( ball ` D ) r ) )
209 blssm
 |-  ( ( D e. ( *Met ` B ) /\ p e. B /\ r e. RR* ) -> ( p ( ball ` D ) r ) C_ B )
210 199 201 203 209 syl3anc
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> ( p ( ball ` D ) r ) C_ B )
211 simplrr
 |-  ( ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) /\ w e. ( p ( ball ` D ) r ) ) -> ( ( p ` k ) ( ball ` E ) r ) C_ u )
212 simplll
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> ph )
213 rpgt0
 |-  ( r e. RR+ -> 0 < r )
214 213 ad2antrl
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> 0 < r )
215 212 201 203 214 96 syl121anc
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> ( p ( ball ` D ) r ) = X_ k e. I ( ( p ` k ) ( ball ` E ) r ) )
216 215 eleq2d
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> ( w e. ( p ( ball ` D ) r ) <-> w e. X_ k e. I ( ( p ` k ) ( ball ` E ) r ) ) )
217 216 biimpa
 |-  ( ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) /\ w e. ( p ( ball ` D ) r ) ) -> w e. X_ k e. I ( ( p ` k ) ( ball ` E ) r ) )
218 vex
 |-  w e. _V
219 218 elixp
 |-  ( w e. X_ k e. I ( ( p ` k ) ( ball ` E ) r ) <-> ( w Fn I /\ A. k e. I ( w ` k ) e. ( ( p ` k ) ( ball ` E ) r ) ) )
220 219 simprbi
 |-  ( w e. X_ k e. I ( ( p ` k ) ( ball ` E ) r ) -> A. k e. I ( w ` k ) e. ( ( p ` k ) ( ball ` E ) r ) )
221 217 220 syl
 |-  ( ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) /\ w e. ( p ( ball ` D ) r ) ) -> A. k e. I ( w ` k ) e. ( ( p ` k ) ( ball ` E ) r ) )
222 simp-4r
 |-  ( ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) /\ w e. ( p ( ball ` D ) r ) ) -> k e. I )
223 rsp
 |-  ( A. k e. I ( w ` k ) e. ( ( p ` k ) ( ball ` E ) r ) -> ( k e. I -> ( w ` k ) e. ( ( p ` k ) ( ball ` E ) r ) ) )
224 221 222 223 sylc
 |-  ( ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) /\ w e. ( p ( ball ` D ) r ) ) -> ( w ` k ) e. ( ( p ` k ) ( ball ` E ) r ) )
225 211 224 sseldd
 |-  ( ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) /\ w e. ( p ( ball ` D ) r ) ) -> ( w ` k ) e. u )
226 210 225 ssrabdv
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> ( p ( ball ` D ) r ) C_ { w e. B | ( w ` k ) e. u } )
227 226 188 sseqtrrdi
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> ( p ( ball ` D ) r ) C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) )
228 eleq2
 |-  ( y = ( p ( ball ` D ) r ) -> ( p e. y <-> p e. ( p ( ball ` D ) r ) ) )
229 sseq1
 |-  ( y = ( p ( ball ` D ) r ) -> ( y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) <-> ( p ( ball ` D ) r ) C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) )
230 228 229 anbi12d
 |-  ( y = ( p ( ball ` D ) r ) -> ( ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) <-> ( p e. ( p ( ball ` D ) r ) /\ ( p ( ball ` D ) r ) C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) ) )
231 230 rspcev
 |-  ( ( ( p ( ball ` D ) r ) e. ( MetOpen ` D ) /\ ( p e. ( p ( ball ` D ) r ) /\ ( p ( ball ` D ) r ) C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) ) -> E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) )
232 205 208 227 231 syl12anc
 |-  ( ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) /\ ( r e. RR+ /\ ( ( p ` k ) ( ball ` E ) r ) C_ u ) ) -> E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) )
233 198 232 rexlimddv
 |-  ( ( ( ph /\ k e. I ) /\ ( u e. K /\ ( p e. B /\ ( p ` k ) e. u ) ) ) -> E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) )
234 233 expr
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( ( p e. B /\ ( p ` k ) e. u ) -> E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) ) )
235 189 234 syl5bi
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( p e. ( `' ( w e. B |-> ( w ` k ) ) " u ) -> E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) ) )
236 235 ralrimiv
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> A. p e. ( `' ( w e. B |-> ( w ` k ) ) " u ) E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) )
237 157 ad2antrr
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( MetOpen ` D ) e. Top )
238 eltop2
 |-  ( ( MetOpen ` D ) e. Top -> ( ( `' ( w e. B |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) <-> A. p e. ( `' ( w e. B |-> ( w ` k ) ) " u ) E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) ) )
239 237 238 syl
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( ( `' ( w e. B |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) <-> A. p e. ( `' ( w e. B |-> ( w ` k ) ) " u ) E. y e. ( MetOpen ` D ) ( p e. y /\ y C_ ( `' ( w e. B |-> ( w ` k ) ) " u ) ) ) )
240 236 239 mpbird
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( `' ( w e. B |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) )
241 184 240 eqeltrrd
 |-  ( ( ( ph /\ k e. I ) /\ u e. K ) -> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) )
242 241 ralrimiva
 |-  ( ( ph /\ k e. I ) -> A. u e. K ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) )
243 159 raleqdv
 |-  ( ( ph /\ k e. I ) -> ( A. u e. ( ( TopOpen o. R ) ` k ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) <-> A. u e. K ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) ) )
244 242 243 mpbird
 |-  ( ( ph /\ k e. I ) -> A. u e. ( ( TopOpen o. R ) ` k ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) )
245 244 ralrimiva
 |-  ( ph -> A. k e. I A. u e. ( ( TopOpen o. R ) ` k ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) )
246 fveq2
 |-  ( k = m -> ( ( TopOpen o. R ) ` k ) = ( ( TopOpen o. R ) ` m ) )
247 fveq2
 |-  ( k = m -> ( w ` k ) = ( w ` m ) )
248 247 mpteq2dv
 |-  ( k = m -> ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) = ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) )
249 248 cnveqd
 |-  ( k = m -> `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) = `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) )
250 249 imaeq1d
 |-  ( k = m -> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) = ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) )
251 250 eleq1d
 |-  ( k = m -> ( ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) <-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) e. ( MetOpen ` D ) ) )
252 246 251 raleqbidv
 |-  ( k = m -> ( A. u e. ( ( TopOpen o. R ) ` k ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) <-> A. u e. ( ( TopOpen o. R ) ` m ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) e. ( MetOpen ` D ) ) )
253 252 cbvralvw
 |-  ( A. k e. I A. u e. ( ( TopOpen o. R ) ` k ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` k ) ) " u ) e. ( MetOpen ` D ) <-> A. m e. I A. u e. ( ( TopOpen o. R ) ` m ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) e. ( MetOpen ` D ) )
254 245 253 sylib
 |-  ( ph -> A. m e. I A. u e. ( ( TopOpen o. R ) ` m ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) e. ( MetOpen ` D ) )
255 eqid
 |-  ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) = ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) )
256 255 fmpox
 |-  ( A. m e. I A. u e. ( ( TopOpen o. R ) ` m ) ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) e. ( MetOpen ` D ) <-> ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) : U_ m e. I ( { m } X. ( ( TopOpen o. R ) ` m ) ) --> ( MetOpen ` D ) )
257 254 256 sylib
 |-  ( ph -> ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) : U_ m e. I ( { m } X. ( ( TopOpen o. R ) ` m ) ) --> ( MetOpen ` D ) )
258 257 frnd
 |-  ( ph -> ran ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) C_ ( MetOpen ` D ) )
259 180 258 unssd
 |-  ( ph -> ( { X_ n e. I U. ( ( TopOpen o. R ) ` n ) } u. ran ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) ) C_ ( MetOpen ` D ) )
260 fiss
 |-  ( ( ( MetOpen ` D ) e. Top /\ ( { X_ n e. I U. ( ( TopOpen o. R ) ` n ) } u. ran ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) ) C_ ( MetOpen ` D ) ) -> ( fi ` ( { X_ n e. I U. ( ( TopOpen o. R ) ` n ) } u. ran ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) ) ) C_ ( fi ` ( MetOpen ` D ) ) )
261 157 259 260 syl2anc
 |-  ( ph -> ( fi ` ( { X_ n e. I U. ( ( TopOpen o. R ) ` n ) } u. ran ( m e. I , u e. ( ( TopOpen o. R ) ` m ) |-> ( `' ( w e. X_ n e. I U. ( ( TopOpen o. R ) ` n ) |-> ( w ` m ) ) " u ) ) ) ) C_ ( fi ` ( MetOpen ` D ) ) )
262 154 261 eqsstrd
 |-  ( ph -> C C_ ( fi ` ( MetOpen ` D ) ) )
263 fitop
 |-  ( ( MetOpen ` D ) e. Top -> ( fi ` ( MetOpen ` D ) ) = ( MetOpen ` D ) )
264 157 263 syl
 |-  ( ph -> ( fi ` ( MetOpen ` D ) ) = ( MetOpen ` D ) )
265 155 mopnval
 |-  ( D e. ( *Met ` B ) -> ( MetOpen ` D ) = ( topGen ` ran ( ball ` D ) ) )
266 21 265 syl
 |-  ( ph -> ( MetOpen ` D ) = ( topGen ` ran ( ball ` D ) ) )
267 tgdif0
 |-  ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) = ( topGen ` ran ( ball ` D ) )
268 266 267 eqtr4di
 |-  ( ph -> ( MetOpen ` D ) = ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) )
269 264 268 eqtrd
 |-  ( ph -> ( fi ` ( MetOpen ` D ) ) = ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) )
270 262 269 sseqtrd
 |-  ( ph -> C C_ ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) )
271 2basgen
 |-  ( ( ( ran ( ball ` D ) \ { (/) } ) C_ C /\ C C_ ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) ) -> ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) = ( topGen ` C ) )
272 137 270 271 syl2anc
 |-  ( ph -> ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) = ( topGen ` C ) )
273 19 272 eqtr4d
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( topGen ` ( ran ( ball ` D ) \ { (/) } ) ) )
274 1 2 3 13 7 prdstopn
 |-  ( ph -> J = ( Xt_ ` ( TopOpen o. R ) ) )
275 273 274 268 3eqtr4d
 |-  ( ph -> J = ( MetOpen ` D ) )