Description: A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | metnrm.j | |- J = ( MetOpen ` D ) |
|
Assertion | metreg | |- ( D e. ( *Met ` X ) -> J e. Reg ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metnrm.j | |- J = ( MetOpen ` D ) |
|
2 | 1 | metnrm | |- ( D e. ( *Met ` X ) -> J e. Nrm ) |
3 | 1 | methaus | |- ( D e. ( *Met ` X ) -> J e. Haus ) |
4 | haust1 | |- ( J e. Haus -> J e. Fre ) |
|
5 | 3 4 | syl | |- ( D e. ( *Met ` X ) -> J e. Fre ) |
6 | nrmreg | |- ( ( J e. Nrm /\ J e. Fre ) -> J e. Reg ) |
|
7 | 2 5 6 | syl2anc | |- ( D e. ( *Met ` X ) -> J e. Reg ) |