Metamath Proof Explorer

Theorem mopnm

Description: The base set of a metric space is open. Part of Theorem T1 of Kreyszig p. 19. (Contributed by NM, 4-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopnval.1 J = MetOpen D
Assertion mopnm D ∞Met X X J


Step Hyp Ref Expression
1 mopnval.1 J = MetOpen D
2 1 mopntopon D ∞Met X J TopOn X
3 toponmax J TopOn X X J
4 2 3 syl D ∞Met X X J