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 ) )