Metamath Proof Explorer

Theorem metnrm

Description: A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013) (Revised by Mario Carneiro, 5-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypothesis metnrm.j ⊢ J = MetOpen ⁡ D
Assertion metnrm ⊢ D ∈ ∞Met ⁡ X → J ∈ Nrm

Proof

Step Hyp Ref Expression
1 metnrm.j ⊢ J = MetOpen ⁡ D
2 1 mopntop ⊢ D ∈ ∞Met ⁡ X → J ∈ Top
3 eqid ⊢ u ∈ X ⟼ inf ran ⁡ v ∈ x ⟼ u D v ℝ * < = u ∈ X ⟼ inf ran ⁡ v ∈ x ⟼ u D v ℝ * <
4 simp1 ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ Clsd ⁡ J ∧ y ∈ Clsd ⁡ J ∧ x ∩ y = ∅ → D ∈ ∞Met ⁡ X
5 simp2l ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ Clsd ⁡ J ∧ y ∈ Clsd ⁡ J ∧ x ∩ y = ∅ → x ∈ Clsd ⁡ J
6 simp2r ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ Clsd ⁡ J ∧ y ∈ Clsd ⁡ J ∧ x ∩ y = ∅ → y ∈ Clsd ⁡ J
7 simp3 ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ Clsd ⁡ J ∧ y ∈ Clsd ⁡ J ∧ x ∩ y = ∅ → x ∩ y = ∅
8 eqid ⊢ ⋃ s ∈ y s ball ⁡ D if 1 ≤ u ∈ X ⟼ inf ran ⁡ v ∈ x ⟼ u D v ℝ * < ⁡ s 1 u ∈ X ⟼ inf ran ⁡ v ∈ x ⟼ u D v ℝ * < ⁡ s 2 = ⋃ s ∈ y s ball ⁡ D if 1 ≤ u ∈ X ⟼ inf ran ⁡ v ∈ x ⟼ u D v ℝ * < ⁡ s 1 u ∈ X ⟼ inf ran ⁡ v ∈ x ⟼ u D v ℝ * < ⁡ s 2
9 eqid ⊢ u ∈ X ⟼ inf ran ⁡ v ∈ y ⟼ u D v ℝ * < = u ∈ X ⟼ inf ran ⁡ v ∈ y ⟼ u D v ℝ * <
10 eqid ⊢ ⋃ t ∈ x t ball ⁡ D if 1 ≤ u ∈ X ⟼ inf ran ⁡ v ∈ y ⟼ u D v ℝ * < ⁡ t 1 u ∈ X ⟼ inf ran ⁡ v ∈ y ⟼ u D v ℝ * < ⁡ t 2 = ⋃ t ∈ x t ball ⁡ D if 1 ≤ u ∈ X ⟼ inf ran ⁡ v ∈ y ⟼ u D v ℝ * < ⁡ t 1 u ∈ X ⟼ inf ran ⁡ v ∈ y ⟼ u D v ℝ * < ⁡ t 2
11 3 1 4 5 6 7 8 9 10 metnrmlem3 ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ Clsd ⁡ J ∧ y ∈ Clsd ⁡ J ∧ x ∩ y = ∅ → ∃ z ∈ J ∃ w ∈ J x ⊆ z ∧ y ⊆ w ∧ z ∩ w = ∅
12 11 3expia ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ Clsd ⁡ J ∧ y ∈ Clsd ⁡ J → x ∩ y = ∅ → ∃ z ∈ J ∃ w ∈ J x ⊆ z ∧ y ⊆ w ∧ z ∩ w = ∅
13 12 ralrimivva ⊢ D ∈ ∞Met ⁡ X → ∀ x ∈ Clsd ⁡ J ∀ y ∈ Clsd ⁡ J x ∩ y = ∅ → ∃ z ∈ J ∃ w ∈ J x ⊆ z ∧ y ⊆ w ∧ z ∩ w = ∅
14 isnrm3 ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ x ∈ Clsd ⁡ J ∀ y ∈ Clsd ⁡ J x ∩ y = ∅ → ∃ z ∈ J ∃ w ∈ J x ⊆ z ∧ y ⊆ w ∧ z ∩ w = ∅
15 2 13 14 sylanbrc ⊢ D ∈ ∞Met ⁡ X → J ∈ Nrm