| Step |
Hyp |
Ref |
Expression |
| 1 |
|
blin2 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 2 |
|
simpll |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
| 3 |
|
elinel1 |
⊢ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → 𝑧 ∈ 𝑥 ) |
| 4 |
|
elunii |
⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → 𝑧 ∈ ∪ ran ( ball ‘ 𝐷 ) ) |
| 5 |
3 4
|
sylan |
⊢ ( ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ) → 𝑧 ∈ ∪ ran ( ball ‘ 𝐷 ) ) |
| 6 |
5
|
ad2ant2lr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑧 ∈ ∪ ran ( ball ‘ 𝐷 ) ) |
| 7 |
|
unirnbl |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 ) |
| 8 |
7
|
ad2antrr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 ) |
| 9 |
6 8
|
eleqtrd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → 𝑧 ∈ 𝑋 ) |
| 10 |
|
blssex |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
| 11 |
2 9 10
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ( ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑧 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
| 12 |
1 11
|
mpbird |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
| 13 |
12
|
ex |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) → ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 14 |
13
|
ralrimdva |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ) → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 15 |
14
|
ralrimivv |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
| 16 |
|
fvex |
⊢ ( ball ‘ 𝐷 ) ∈ V |
| 17 |
16
|
rnex |
⊢ ran ( ball ‘ 𝐷 ) ∈ V |
| 18 |
|
isbasis2g |
⊢ ( ran ( ball ‘ 𝐷 ) ∈ V → ( ran ( ball ‘ 𝐷 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 19 |
17 18
|
ax-mp |
⊢ ( ran ( ball ‘ 𝐷 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐷 ) ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑏 ∈ ran ( ball ‘ 𝐷 ) ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) |
| 20 |
15 19
|
sylibr |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ∈ TopBases ) |