Step |
Hyp |
Ref |
Expression |
1 |
|
prdsxms.y |
|- Y = ( S Xs_ R ) |
2 |
|
simp1 |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> S e. W ) |
3 |
|
simp2 |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> I e. Fin ) |
4 |
|
eqid |
|- ( dist ` Y ) = ( dist ` Y ) |
5 |
|
eqid |
|- ( Base ` Y ) = ( Base ` Y ) |
6 |
|
simp3 |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> R : I --> *MetSp ) |
7 |
1 2 3 4 5 6
|
prdsxmslem1 |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> ( dist ` Y ) e. ( *Met ` ( Base ` Y ) ) ) |
8 |
|
ssid |
|- ( Base ` Y ) C_ ( Base ` Y ) |
9 |
|
xmetres2 |
|- ( ( ( dist ` Y ) e. ( *Met ` ( Base ` Y ) ) /\ ( Base ` Y ) C_ ( Base ` Y ) ) -> ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) e. ( *Met ` ( Base ` Y ) ) ) |
10 |
7 8 9
|
sylancl |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) e. ( *Met ` ( Base ` Y ) ) ) |
11 |
|
eqid |
|- ( TopOpen ` Y ) = ( TopOpen ` Y ) |
12 |
|
eqid |
|- ( Base ` ( R ` k ) ) = ( Base ` ( R ` k ) ) |
13 |
|
eqid |
|- ( ( dist ` ( R ` k ) ) |` ( ( Base ` ( R ` k ) ) X. ( Base ` ( R ` k ) ) ) ) = ( ( dist ` ( R ` k ) ) |` ( ( Base ` ( R ` k ) ) X. ( Base ` ( R ` k ) ) ) ) |
14 |
|
eqid |
|- ( TopOpen ` ( R ` k ) ) = ( TopOpen ` ( R ` k ) ) |
15 |
|
eqid |
|- { 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 ) ) } = { 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 ) ) } |
16 |
1 2 3 4 5 6 11 12 13 14 15
|
prdsxmslem2 |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> ( TopOpen ` Y ) = ( MetOpen ` ( dist ` Y ) ) ) |
17 |
|
xmetf |
|- ( ( dist ` Y ) e. ( *Met ` ( Base ` Y ) ) -> ( dist ` Y ) : ( ( Base ` Y ) X. ( Base ` Y ) ) --> RR* ) |
18 |
|
ffn |
|- ( ( dist ` Y ) : ( ( Base ` Y ) X. ( Base ` Y ) ) --> RR* -> ( dist ` Y ) Fn ( ( Base ` Y ) X. ( Base ` Y ) ) ) |
19 |
|
fnresdm |
|- ( ( dist ` Y ) Fn ( ( Base ` Y ) X. ( Base ` Y ) ) -> ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) = ( dist ` Y ) ) |
20 |
7 17 18 19
|
4syl |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) = ( dist ` Y ) ) |
21 |
20
|
fveq2d |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> ( MetOpen ` ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) ) = ( MetOpen ` ( dist ` Y ) ) ) |
22 |
16 21
|
eqtr4d |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> ( TopOpen ` Y ) = ( MetOpen ` ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) ) ) |
23 |
|
eqid |
|- ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) = ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) |
24 |
11 5 23
|
isxms2 |
|- ( Y e. *MetSp <-> ( ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) e. ( *Met ` ( Base ` Y ) ) /\ ( TopOpen ` Y ) = ( MetOpen ` ( ( dist ` Y ) |` ( ( Base ` Y ) X. ( Base ` Y ) ) ) ) ) ) |
25 |
10 22 24
|
sylanbrc |
|- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> Y e. *MetSp ) |