Step |
Hyp |
Ref |
Expression |
1 |
|
blf |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) : ( 𝑋 × ℝ* ) ⟶ 𝒫 𝑋 ) |
2 |
1
|
frnd |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 ) |
3 |
|
sspwuni |
⊢ ( ran ( ball ‘ 𝐷 ) ⊆ 𝒫 𝑋 ↔ ∪ ran ( ball ‘ 𝐷 ) ⊆ 𝑋 ) |
4 |
2 3
|
sylib |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) ⊆ 𝑋 ) |
5 |
|
1rp |
⊢ 1 ∈ ℝ+ |
6 |
|
blcntr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) |
7 |
5 6
|
mp3an3 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) |
8 |
|
1xr |
⊢ 1 ∈ ℝ* |
9 |
|
blelrn |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) ) |
10 |
8 9
|
mp3an3 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) ) |
11 |
|
elunii |
⊢ ( ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∧ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ∈ ran ( ball ‘ 𝐷 ) ) → 𝑥 ∈ ∪ ran ( ball ‘ 𝐷 ) ) |
12 |
7 10 11
|
syl2anc |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ∪ ran ( ball ‘ 𝐷 ) ) |
13 |
4 12
|
eqelssd |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 ) |