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 e. ( PsMet ` X ) -> U. ran ( ball ` D ) = X )

Proof

Step Hyp Ref Expression
1 blfps
 |-  ( D e. ( PsMet ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
2 1 frnd
 |-  ( D e. ( PsMet ` X ) -> ran ( ball ` D ) C_ ~P X )
3 sspwuni
 |-  ( ran ( ball ` D ) C_ ~P X <-> U. ran ( ball ` D ) C_ X )
4 2 3 sylib
 |-  ( D e. ( PsMet ` X ) -> U. ran ( ball ` D ) C_ X )
5 1rp
 |-  1 e. RR+
6 blcntrps
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X /\ 1 e. RR+ ) -> x e. ( x ( ball ` D ) 1 ) )
7 5 6 mp3an3
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X ) -> x e. ( x ( ball ` D ) 1 ) )
8 1xr
 |-  1 e. RR*
9 blelrnps
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) e. ran ( ball ` D ) )
10 8 9 mp3an3
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X ) -> ( x ( ball ` D ) 1 ) e. ran ( ball ` D ) )
11 elunii
 |-  ( ( x e. ( x ( ball ` D ) 1 ) /\ ( x ( ball ` D ) 1 ) e. ran ( ball ` D ) ) -> x e. U. ran ( ball ` D ) )
12 7 10 11 syl2anc
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X ) -> x e. U. ran ( ball ` D ) )
13 4 12 eqelssd
 |-  ( D e. ( PsMet ` X ) -> U. ran ( ball ` D ) = X )