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}=\mathrm{MetOpen}\left({D}\right)$
Assertion metnrm ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{Nrm}$

Proof

Step Hyp Ref Expression
1 metnrm.j ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 1 mopntop ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{Top}$
3 eqid ${⊢}\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {x}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)=\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {x}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)$
4 simp1 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in \mathrm{Clsd}\left({J}\right)\wedge {y}\in \mathrm{Clsd}\left({J}\right)\right)\wedge {x}\cap {y}=\varnothing \right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
5 simp2l ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in \mathrm{Clsd}\left({J}\right)\wedge {y}\in \mathrm{Clsd}\left({J}\right)\right)\wedge {x}\cap {y}=\varnothing \right)\to {x}\in \mathrm{Clsd}\left({J}\right)$
6 simp2r ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in \mathrm{Clsd}\left({J}\right)\wedge {y}\in \mathrm{Clsd}\left({J}\right)\right)\wedge {x}\cap {y}=\varnothing \right)\to {y}\in \mathrm{Clsd}\left({J}\right)$
7 simp3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in \mathrm{Clsd}\left({J}\right)\wedge {y}\in \mathrm{Clsd}\left({J}\right)\right)\wedge {x}\cap {y}=\varnothing \right)\to {x}\cap {y}=\varnothing$
8 eqid ${⊢}\bigcup _{{s}\in {y}}\left({s}\mathrm{ball}\left({D}\right)\left(\frac{if\left(1\le \left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {x}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({s}\right),1,\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {x}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({s}\right)\right)}{2}\right)\right)=\bigcup _{{s}\in {y}}\left({s}\mathrm{ball}\left({D}\right)\left(\frac{if\left(1\le \left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {x}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({s}\right),1,\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {x}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({s}\right)\right)}{2}\right)\right)$
9 eqid ${⊢}\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {y}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)=\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {y}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)$
10 eqid ${⊢}\bigcup _{{t}\in {x}}\left({t}\mathrm{ball}\left({D}\right)\left(\frac{if\left(1\le \left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {y}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({t}\right),1,\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {y}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({t}\right)\right)}{2}\right)\right)=\bigcup _{{t}\in {x}}\left({t}\mathrm{ball}\left({D}\right)\left(\frac{if\left(1\le \left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {y}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({t}\right),1,\left({u}\in {X}⟼sup\left(\mathrm{ran}\left({v}\in {y}⟼{u}{D}{v}\right),{ℝ}^{*},<\right)\right)\left({t}\right)\right)}{2}\right)\right)$
11 3 1 4 5 6 7 8 9 10 metnrmlem3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in \mathrm{Clsd}\left({J}\right)\wedge {y}\in \mathrm{Clsd}\left({J}\right)\right)\wedge {x}\cap {y}=\varnothing \right)\to \exists {z}\in {J}\phantom{\rule{.4em}{0ex}}\exists {w}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {z}\wedge {y}\subseteq {w}\wedge {z}\cap {w}=\varnothing \right)$
12 11 3expia ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in \mathrm{Clsd}\left({J}\right)\wedge {y}\in \mathrm{Clsd}\left({J}\right)\right)\right)\to \left({x}\cap {y}=\varnothing \to \exists {z}\in {J}\phantom{\rule{.4em}{0ex}}\exists {w}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {z}\wedge {y}\subseteq {w}\wedge {z}\cap {w}=\varnothing \right)\right)$
13 12 ralrimivva ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \forall {x}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\left({x}\cap {y}=\varnothing \to \exists {z}\in {J}\phantom{\rule{.4em}{0ex}}\exists {w}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {z}\wedge {y}\subseteq {w}\wedge {z}\cap {w}=\varnothing \right)\right)$
14 isnrm3 ${⊢}{J}\in \mathrm{Nrm}↔\left({J}\in \mathrm{Top}\wedge \forall {x}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\left({x}\cap {y}=\varnothing \to \exists {z}\in {J}\phantom{\rule{.4em}{0ex}}\exists {w}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {z}\wedge {y}\subseteq {w}\wedge {z}\cap {w}=\varnothing \right)\right)\right)$
15 2 13 14 sylanbrc ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{Nrm}$