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 DPsMetXranballD=X

Proof

Step Hyp Ref Expression
1 blfps DPsMetXballD:X×*𝒫X
2 1 frnd DPsMetXranballD𝒫X
3 sspwuni ranballD𝒫XranballDX
4 2 3 sylib DPsMetXranballDX
5 1rp 1+
6 blcntrps DPsMetXxX1+xxballD1
7 5 6 mp3an3 DPsMetXxXxxballD1
8 1xr 1*
9 blelrnps DPsMetXxX1*xballD1ranballD
10 8 9 mp3an3 DPsMetXxXxballD1ranballD
11 elunii xxballD1xballD1ranballDxranballD
12 7 10 11 syl2anc DPsMetXxXxranballD
13 4 12 eqelssd DPsMetXranballD=X