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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | blfps | |
|
2 | 1 | frnd | |
3 | sspwuni | |
|
4 | 2 3 | sylib | |
5 | 1rp | |
|
6 | blcntrps | |
|
7 | 5 6 | mp3an3 | |
8 | 1xr | |
|
9 | blelrnps | |
|
10 | 8 9 | mp3an3 | |
11 | elunii | |
|
12 | 7 10 11 | syl2anc | |
13 | 4 12 | eqelssd | |