Description: An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mopnval.1 | β’ π½ = ( MetOpen β π· ) | |
| Assertion | mopnss | β’ ( ( π· β ( βMet β π ) β§ π΄ β π½ ) β π΄ β π ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mopnval.1 | β’ π½ = ( MetOpen β π· ) | |
| 2 | 1 | mopntopon | β’ ( π· β ( βMet β π ) β π½ β ( TopOn β π ) ) |
| 3 | toponss | β’ ( ( π½ β ( TopOn β π ) β§ π΄ β π½ ) β π΄ β π ) | |
| 4 | 2 3 | sylan | β’ ( ( π· β ( βMet β π ) β§ π΄ β π½ ) β π΄ β π ) |