Step |
Hyp |
Ref |
Expression |
1 |
|
tmsbas.k |
β’ πΎ = ( toMetSp β π· ) |
2 |
|
tmstopn.j |
β’ π½ = ( MetOpen β π· ) |
3 |
|
eqid |
β’ { β¨ ( Base β ndx ) , π β© , β¨ ( dist β ndx ) , π· β© } = { β¨ ( Base β ndx ) , π β© , β¨ ( dist β ndx ) , π· β© } |
4 |
3 1
|
tmslem |
β’ ( π· β ( βMet β π ) β ( π = ( Base β πΎ ) β§ π· = ( dist β πΎ ) β§ ( MetOpen β π· ) = ( TopOpen β πΎ ) ) ) |
5 |
4
|
simp3d |
β’ ( π· β ( βMet β π ) β ( MetOpen β π· ) = ( TopOpen β πΎ ) ) |
6 |
2 5
|
eqtrid |
β’ ( π· β ( βMet β π ) β π½ = ( TopOpen β πΎ ) ) |