Step |
Hyp |
Ref |
Expression |
1 |
|
isms.j |
|- J = ( TopOpen ` K ) |
2 |
|
isms.x |
|- X = ( Base ` K ) |
3 |
|
isms.d |
|- D = ( ( dist ` K ) |` ( X X. X ) ) |
4 |
|
fveq2 |
|- ( f = K -> ( TopOpen ` f ) = ( TopOpen ` K ) ) |
5 |
4 1
|
eqtr4di |
|- ( f = K -> ( TopOpen ` f ) = J ) |
6 |
|
fveq2 |
|- ( f = K -> ( dist ` f ) = ( dist ` K ) ) |
7 |
|
fveq2 |
|- ( f = K -> ( Base ` f ) = ( Base ` K ) ) |
8 |
7 2
|
eqtr4di |
|- ( f = K -> ( Base ` f ) = X ) |
9 |
8
|
sqxpeqd |
|- ( f = K -> ( ( Base ` f ) X. ( Base ` f ) ) = ( X X. X ) ) |
10 |
6 9
|
reseq12d |
|- ( f = K -> ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) = ( ( dist ` K ) |` ( X X. X ) ) ) |
11 |
10 3
|
eqtr4di |
|- ( f = K -> ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) = D ) |
12 |
11
|
fveq2d |
|- ( f = K -> ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) = ( MetOpen ` D ) ) |
13 |
5 12
|
eqeq12d |
|- ( f = K -> ( ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) <-> J = ( MetOpen ` D ) ) ) |
14 |
|
df-xms |
|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) } |
15 |
13 14
|
elrab2 |
|- ( K e. *MetSp <-> ( K e. TopSp /\ J = ( MetOpen ` D ) ) ) |