Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
β’ ( TopOpen β π ) = ( TopOpen β π ) |
2 |
|
eqid |
β’ ( Base β π ) = ( Base β π ) |
3 |
|
eqid |
β’ ( ( dist β π ) βΎ ( ( Base β π ) Γ ( Base β π ) ) ) = ( ( dist β π ) βΎ ( ( Base β π ) Γ ( Base β π ) ) ) |
4 |
1 2 3
|
isms |
β’ ( π β MetSp β ( π β βMetSp β§ ( ( dist β π ) βΎ ( ( Base β π ) Γ ( Base β π ) ) ) β ( Met β ( Base β π ) ) ) ) |
5 |
4
|
simplbi |
β’ ( π β MetSp β π β βMetSp ) |