Metamath Proof Explorer

Theorem unirnbl

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)

Ref Expression
Assertion unirnbl 
|- ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X )

Proof

Step Hyp Ref Expression
1 blf 
 |-  ( D e. ( *Met ` X ) -> ( ball ` D ) : ( X X. RR* ) --> ~P X )
2 1 frnd 
 |-  ( D e. ( *Met ` 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. ( *Met ` X ) -> U. ran ( ball ` D ) C_ X )
5 1rp 
 |-  1 e. RR+
6 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR+ ) -> x e. ( x ( ball ` D ) 1 ) )
7 5 6 mp3an3 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> x e. ( x ( ball ` D ) 1 ) )
8 1xr 
 |-  1 e. RR*
9 blelrn 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) e. ran ( ball ` D ) )
10 8 9 mp3an3 
 |-  ( ( D e. ( *Met ` 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. ( *Met ` X ) /\ x e. X ) -> x e. U. ran ( ball ` D ) )
13 4 12 eqelssd 
 |-  ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X )