Description: A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | metnrm.j | β’ π½ = ( MetOpen β π· ) | |
| Assertion | metreg | β’ ( π· β ( βMet β π ) β π½ β Reg ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | metnrm.j | β’ π½ = ( MetOpen β π· ) | |
| 2 | 1 | metnrm | β’ ( π· β ( βMet β π ) β π½ β Nrm ) |
| 3 | 1 | methaus | β’ ( π· β ( βMet β π ) β π½ β Haus ) |
| 4 | haust1 | β’ ( π½ β Haus β π½ β Fre ) | |
| 5 | 3 4 | syl | β’ ( π· β ( βMet β π ) β π½ β Fre ) |
| 6 | nrmreg | β’ ( ( π½ β Nrm β§ π½ β Fre ) β π½ β Reg ) | |
| 7 | 2 5 6 | syl2anc | β’ ( π· β ( βMet β π ) β π½ β Reg ) |