Metamath Proof Explorer


Theorem mopnex

Description: The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis mopnex.1 J = MetOpen D
Assertion mopnex D ∞Met X d Met X J = MetOpen d

Proof

Step Hyp Ref Expression
1 mopnex.1 J = MetOpen D
2 1rp 1 +
3 eqid x X , y X if x D y 1 x D y 1 = x X , y X if x D y 1 x D y 1
4 3 stdbdmet D ∞Met X 1 + x X , y X if x D y 1 x D y 1 Met X
5 2 4 mpan2 D ∞Met X x X , y X if x D y 1 x D y 1 Met X
6 1xr 1 *
7 0lt1 0 < 1
8 3 1 stdbdmopn D ∞Met X 1 * 0 < 1 J = MetOpen x X , y X if x D y 1 x D y 1
9 6 7 8 mp3an23 D ∞Met X J = MetOpen x X , y X if x D y 1 x D y 1
10 fveq2 d = x X , y X if x D y 1 x D y 1 MetOpen d = MetOpen x X , y X if x D y 1 x D y 1
11 10 rspceeqv x X , y X if x D y 1 x D y 1 Met X J = MetOpen x X , y X if x D y 1 x D y 1 d Met X J = MetOpen d
12 5 9 11 syl2anc D ∞Met X d Met X J = MetOpen d