| Step |
Hyp |
Ref |
Expression |
| 1 |
|
tmsval.m |
|- M = { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. } |
| 2 |
|
tmsval.k |
|- K = ( toMetSp ` D ) |
| 3 |
|
elfvdm |
|- ( D e. ( *Met ` X ) -> X e. dom *Met ) |
| 4 |
|
basendxltdsndx |
|- ( Base ` ndx ) < ( dist ` ndx ) |
| 5 |
|
dsndxnn |
|- ( dist ` ndx ) e. NN |
| 6 |
1 4 5
|
2strbas |
|- ( X e. dom *Met -> X = ( Base ` M ) ) |
| 7 |
3 6
|
syl |
|- ( D e. ( *Met ` X ) -> X = ( Base ` M ) ) |
| 8 |
|
xmetf |
|- ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* ) |
| 9 |
|
ffn |
|- ( D : ( X X. X ) --> RR* -> D Fn ( X X. X ) ) |
| 10 |
|
fnresdm |
|- ( D Fn ( X X. X ) -> ( D |` ( X X. X ) ) = D ) |
| 11 |
8 9 10
|
3syl |
|- ( D e. ( *Met ` X ) -> ( D |` ( X X. X ) ) = D ) |
| 12 |
|
dsid |
|- dist = Slot ( dist ` ndx ) |
| 13 |
1 4 5 12
|
2strop |
|- ( D e. ( *Met ` X ) -> D = ( dist ` M ) ) |
| 14 |
13
|
reseq1d |
|- ( D e. ( *Met ` X ) -> ( D |` ( X X. X ) ) = ( ( dist ` M ) |` ( X X. X ) ) ) |
| 15 |
11 14
|
eqtr3d |
|- ( D e. ( *Met ` X ) -> D = ( ( dist ` M ) |` ( X X. X ) ) ) |
| 16 |
1 2
|
tmsval |
|- ( D e. ( *Met ` X ) -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) |
| 17 |
7 15 16
|
setsmsbas |
|- ( D e. ( *Met ` X ) -> X = ( Base ` K ) ) |
| 18 |
7 15 16
|
setsmsds |
|- ( D e. ( *Met ` X ) -> ( dist ` M ) = ( dist ` K ) ) |
| 19 |
13 18
|
eqtrd |
|- ( D e. ( *Met ` X ) -> D = ( dist ` K ) ) |
| 20 |
|
prex |
|- { <. ( Base ` ndx ) , X >. , <. ( dist ` ndx ) , D >. } e. _V |
| 21 |
1 20
|
eqeltri |
|- M e. _V |
| 22 |
21
|
a1i |
|- ( D e. ( *Met ` X ) -> M e. _V ) |
| 23 |
7 15 16 22
|
setsmstopn |
|- ( D e. ( *Met ` X ) -> ( MetOpen ` D ) = ( TopOpen ` K ) ) |
| 24 |
17 19 23
|
3jca |
|- ( D e. ( *Met ` X ) -> ( X = ( Base ` K ) /\ D = ( dist ` K ) /\ ( MetOpen ` D ) = ( TopOpen ` K ) ) ) |