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