This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion metnrm ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Nrm )

Proof

Step Hyp Ref Expression
1 metnrm.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3 eqid ⊢ ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) = ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) )
4 simp1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5 simp2l ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
6 simp2r ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ ( Clsd ‘ 𝐽 ) )
7 simp3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
8 eqid ⊢ ∪ 𝑠 ∈ 𝑦 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑠 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑠 ) ) / 2 ) ) = ∪ 𝑠 ∈ 𝑦 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑠 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑥 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑠 ) ) / 2 ) )
9 eqid ⊢ ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) = ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) )
10 eqid ⊢ ∪ 𝑡 ∈ 𝑥 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑡 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑡 ) ) / 2 ) ) = ∪ 𝑡 ∈ 𝑥 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑡 ) , 1 , ( ( 𝑢 ∈ 𝑋 ↦ inf ( ran ( 𝑣 ∈ 𝑦 ↦ ( 𝑢 𝐷 𝑣 ) ) , ℝ* , < ) ) ‘ 𝑡 ) ) / 2 ) )
11 3 1 4 5 6 7 8 9 10 metnrmlem3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
12 11 3expia ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
13 12 ralrimivva ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑥 ∩ 𝑦 ) = ∅ → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
14 isnrm3 ⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑥 ∩ 𝑦 ) = ∅ → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑥 ⊆ 𝑧 ∧ 𝑦 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ) ) )
15 2 13 14 sylanbrc ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Nrm )