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

Metamath Proof Explorer

Theorem unirnbl

Description: The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Assertion unirnbl ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 blf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
2 1 frnd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
3 sspwuni ⊢ ( ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 ↔ ∪ ran ( ball ‘ 𝐷 ) ⊆ 𝑋 )
4 2 3 sylib ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) ⊆ 𝑋 )
5 1rp ⊢ 1 ∈ ℝ+
6 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
7 5 6 mp3an3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
8 1xr ⊢ 1 ∈ ℝ*
9 blelrn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) )
10 8 9 mp3an3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) )
11 elunii ⊢ ( ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) ) → 𝑥 ∈ ∪ ran ( ball ‘ 𝐷 ) )
12 7 10 11 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ∪ ran ( ball ‘ 𝐷 ) )
13 4 12 eqelssd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )