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 ⊢ D ∈ PsMet ⁡ X → ⋃ ran ⁡ ball ⁡ D = X

Proof

Step Hyp Ref Expression
1 blfps ⊢ D ∈ PsMet ⁡ X → ball ⁡ D : X × ℝ * ⟶ 𝒫 X
2 1 frnd ⊢ D ∈ PsMet ⁡ X → ran ⁡ ball ⁡ D ⊆ 𝒫 X
3 sspwuni ⊢ ran ⁡ ball ⁡ D ⊆ 𝒫 X ↔ ⋃ ran ⁡ ball ⁡ D ⊆ X
4 2 3 sylib ⊢ D ∈ PsMet ⁡ X → ⋃ ran ⁡ ball ⁡ D ⊆ X
5 1rp ⊢ 1 ∈ ℝ +
6 blcntrps ⊢ D ∈ PsMet ⁡ X ∧ x ∈ X ∧ 1 ∈ ℝ + → x ∈ x ball ⁡ D 1
7 5 6 mp3an3 ⊢ D ∈ PsMet ⁡ X ∧ x ∈ X → x ∈ x ball ⁡ D 1
8 1xr ⊢ 1 ∈ ℝ *
9 blelrnps ⊢ D ∈ PsMet ⁡ X ∧ x ∈ X ∧ 1 ∈ ℝ * → x ball ⁡ D 1 ∈ ran ⁡ ball ⁡ D
10 8 9 mp3an3 ⊢ D ∈ PsMet ⁡ X ∧ x ∈ X → x ball ⁡ D 1 ∈ ran ⁡ ball ⁡ D
11 elunii ⊢ x ∈ x ball ⁡ D 1 ∧ x ball ⁡ D 1 ∈ ran ⁡ ball ⁡ D → x ∈ ⋃ ran ⁡ ball ⁡ D
12 7 10 11 syl2anc ⊢ D ∈ PsMet ⁡ X ∧ x ∈ X → x ∈ ⋃ ran ⁡ ball ⁡ D
13 4 12 eqelssd ⊢ D ∈ PsMet ⁡ X → ⋃ ran ⁡ ball ⁡ D = X