Step |
Hyp |
Ref |
Expression |
1 |
|
xmsusp.x |
|- X = ( Base ` F ) |
2 |
|
xmsusp.d |
|- D = ( ( dist ` F ) |` ( X X. X ) ) |
3 |
|
xmsusp.u |
|- U = ( UnifSt ` F ) |
4 |
|
simp3 |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> U = ( metUnif ` D ) ) |
5 |
|
simp1 |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> X =/= (/) ) |
6 |
1 2
|
xmsxmet |
|- ( F e. *MetSp -> D e. ( *Met ` X ) ) |
7 |
6
|
3ad2ant2 |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> D e. ( *Met ` X ) ) |
8 |
|
xmetpsmet |
|- ( D e. ( *Met ` X ) -> D e. ( PsMet ` X ) ) |
9 |
|
metuust |
|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) ) |
10 |
8 9
|
sylan2 |
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) ) |
11 |
5 7 10
|
syl2anc |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) ) |
12 |
4 11
|
eqeltrd |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> U e. ( UnifOn ` X ) ) |
13 |
|
xmetutop |
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( MetOpen ` D ) ) |
14 |
5 7 13
|
syl2anc |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( MetOpen ` D ) ) |
15 |
4
|
fveq2d |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> ( unifTop ` U ) = ( unifTop ` ( metUnif ` D ) ) ) |
16 |
|
eqid |
|- ( TopOpen ` F ) = ( TopOpen ` F ) |
17 |
16 1 2
|
xmstopn |
|- ( F e. *MetSp -> ( TopOpen ` F ) = ( MetOpen ` D ) ) |
18 |
17
|
3ad2ant2 |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> ( TopOpen ` F ) = ( MetOpen ` D ) ) |
19 |
14 15 18
|
3eqtr4rd |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> ( TopOpen ` F ) = ( unifTop ` U ) ) |
20 |
1 3 16
|
isusp |
|- ( F e. UnifSp <-> ( U e. ( UnifOn ` X ) /\ ( TopOpen ` F ) = ( unifTop ` U ) ) ) |
21 |
12 19 20
|
sylanbrc |
|- ( ( X =/= (/) /\ F e. *MetSp /\ U = ( metUnif ` D ) ) -> F e. UnifSp ) |