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