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⁡XJ=MetOpen⁡d

Proof

Step Hyp Ref Expression
1 mopnex.1 ⊢J=MetOpen⁡D
2 1rp ⊢1∈ℝ+
3 eqid ⊢x∈X,y∈X⟼ifxDy≤1xDy1=x∈X,y∈X⟼ifxDy≤1xDy1
4 3 stdbdmet ⊢D∈∞Met⁡X∧1∈ℝ+→x∈X,y∈X⟼ifxDy≤1xDy1∈Met⁡X
5 2 4 mpan2 ⊢D∈∞Met⁡X→x∈X,y∈X⟼ifxDy≤1xDy1∈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⟼ifxDy≤1xDy1
9 6 7 8 mp3an23 ⊢D∈∞Met⁡X→J=MetOpen⁡x∈X,y∈X⟼ifxDy≤1xDy1
10 fveq2 ⊢d=x∈X,y∈X⟼ifxDy≤1xDy1→MetOpen⁡d=MetOpen⁡x∈X,y∈X⟼ifxDy≤1xDy1
11 10 rspceeqv ⊢x∈X,y∈X⟼ifxDy≤1xDy1∈Met⁡X∧J=MetOpen⁡x∈X,y∈X⟼ifxDy≤1xDy1→∃d∈Met⁡XJ=MetOpen⁡d
12 5 9 11 syl2anc ⊢D∈∞Met⁡X→∃d∈Met⁡XJ=MetOpen⁡d