Step |
Hyp |
Ref |
Expression |
1 |
|
tmsxps.p |
|- P = ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) |
2 |
|
tmsxps.1 |
|- ( ph -> M e. ( *Met ` X ) ) |
3 |
|
tmsxps.2 |
|- ( ph -> N e. ( *Met ` Y ) ) |
4 |
|
tmsxpsmopn.j |
|- J = ( MetOpen ` M ) |
5 |
|
tmsxpsmopn.k |
|- K = ( MetOpen ` N ) |
6 |
|
tmsxpsmopn.l |
|- L = ( MetOpen ` P ) |
7 |
|
eqid |
|- ( toMetSp ` M ) = ( toMetSp ` M ) |
8 |
7
|
tmsxms |
|- ( M e. ( *Met ` X ) -> ( toMetSp ` M ) e. *MetSp ) |
9 |
2 8
|
syl |
|- ( ph -> ( toMetSp ` M ) e. *MetSp ) |
10 |
|
xmstps |
|- ( ( toMetSp ` M ) e. *MetSp -> ( toMetSp ` M ) e. TopSp ) |
11 |
9 10
|
syl |
|- ( ph -> ( toMetSp ` M ) e. TopSp ) |
12 |
|
eqid |
|- ( toMetSp ` N ) = ( toMetSp ` N ) |
13 |
12
|
tmsxms |
|- ( N e. ( *Met ` Y ) -> ( toMetSp ` N ) e. *MetSp ) |
14 |
3 13
|
syl |
|- ( ph -> ( toMetSp ` N ) e. *MetSp ) |
15 |
|
xmstps |
|- ( ( toMetSp ` N ) e. *MetSp -> ( toMetSp ` N ) e. TopSp ) |
16 |
14 15
|
syl |
|- ( ph -> ( toMetSp ` N ) e. TopSp ) |
17 |
|
eqid |
|- ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) = ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) |
18 |
|
eqid |
|- ( TopOpen ` ( toMetSp ` M ) ) = ( TopOpen ` ( toMetSp ` M ) ) |
19 |
|
eqid |
|- ( TopOpen ` ( toMetSp ` N ) ) = ( TopOpen ` ( toMetSp ` N ) ) |
20 |
|
eqid |
|- ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) |
21 |
17 18 19 20
|
xpstopn |
|- ( ( ( toMetSp ` M ) e. TopSp /\ ( toMetSp ` N ) e. TopSp ) -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( ( TopOpen ` ( toMetSp ` M ) ) tX ( TopOpen ` ( toMetSp ` N ) ) ) ) |
22 |
11 16 21
|
syl2anc |
|- ( ph -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( ( TopOpen ` ( toMetSp ` M ) ) tX ( TopOpen ` ( toMetSp ` N ) ) ) ) |
23 |
17
|
xpsxms |
|- ( ( ( toMetSp ` M ) e. *MetSp /\ ( toMetSp ` N ) e. *MetSp ) -> ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp ) |
24 |
9 14 23
|
syl2anc |
|- ( ph -> ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp ) |
25 |
|
eqid |
|- ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) |
26 |
1
|
reseq1i |
|- ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = ( ( dist ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) |
27 |
20 25 26
|
xmstopn |
|- ( ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) e. *MetSp -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( MetOpen ` ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) ) ) |
28 |
24 27
|
syl |
|- ( ph -> ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) = ( MetOpen ` ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) ) ) |
29 |
|
eqid |
|- ( Base ` ( toMetSp ` M ) ) = ( Base ` ( toMetSp ` M ) ) |
30 |
|
eqid |
|- ( Base ` ( toMetSp ` N ) ) = ( Base ` ( toMetSp ` N ) ) |
31 |
17 29 30 9 14 1
|
xpsdsfn2 |
|- ( ph -> P Fn ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) |
32 |
|
fnresdm |
|- ( P Fn ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = P ) |
33 |
31 32
|
syl |
|- ( ph -> ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) = P ) |
34 |
33
|
fveq2d |
|- ( ph -> ( MetOpen ` ( P |` ( ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) X. ( Base ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) ) ) = ( MetOpen ` P ) ) |
35 |
28 34
|
eqtr2d |
|- ( ph -> ( MetOpen ` P ) = ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) |
36 |
6 35
|
eqtrid |
|- ( ph -> L = ( TopOpen ` ( ( toMetSp ` M ) Xs. ( toMetSp ` N ) ) ) ) |
37 |
7 4
|
tmstopn |
|- ( M e. ( *Met ` X ) -> J = ( TopOpen ` ( toMetSp ` M ) ) ) |
38 |
2 37
|
syl |
|- ( ph -> J = ( TopOpen ` ( toMetSp ` M ) ) ) |
39 |
12 5
|
tmstopn |
|- ( N e. ( *Met ` Y ) -> K = ( TopOpen ` ( toMetSp ` N ) ) ) |
40 |
3 39
|
syl |
|- ( ph -> K = ( TopOpen ` ( toMetSp ` N ) ) ) |
41 |
38 40
|
oveq12d |
|- ( ph -> ( J tX K ) = ( ( TopOpen ` ( toMetSp ` M ) ) tX ( TopOpen ` ( toMetSp ` N ) ) ) ) |
42 |
22 36 41
|
3eqtr4d |
|- ( ph -> L = ( J tX K ) ) |