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