Metamath Proof Explorer


Theorem unirnblps

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) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion unirnblps ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 blfps ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 )
2 1 frnd ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 )
3 sspwuni ( ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 ran ( ball ‘ 𝐷 ) ⊆ 𝑋 )
4 2 3 sylib ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ⊆ 𝑋 )
5 1rp 1 ∈ ℝ+
6 blcntrps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥𝑋 ∧ 1 ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
7 5 6 mp3an3 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥𝑋 ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) )
8 1xr 1 ∈ ℝ*
9 blelrnps ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥𝑋 ∧ 1 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) )
10 8 9 mp3an3 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) )
11 elunii ( ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) ) → 𝑥 ran ( ball ‘ 𝐷 ) )
12 7 10 11 syl2anc ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑥𝑋 ) → 𝑥 ran ( ball ‘ 𝐷 ) )
13 4 12 eqelssd ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) = 𝑋 )