Description: The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mopnval.1 | β’ π½ = ( MetOpen β π· ) | |
Assertion | mopntop | β’ ( π· β ( βMet β π ) β π½ β Top ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mopnval.1 | β’ π½ = ( MetOpen β π· ) | |
2 | 1 | mopntopon | β’ ( π· β ( βMet β π ) β π½ β ( TopOn β π ) ) |
3 | topontop | β’ ( π½ β ( TopOn β π ) β π½ β Top ) | |
4 | 2 3 | syl | β’ ( π· β ( βMet β π ) β π½ β Top ) |