Step |
Hyp |
Ref |
Expression |
1 |
|
mopnval.1 |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
2 |
1
|
elmopn |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐴 ∈ 𝐽 ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐴 ) ) ) ) |
3 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑋 ) |
4 |
|
blssex |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐴 ) ↔ ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 ) ) |
5 |
3 4
|
sylan2 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐴 ) ↔ ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 ) ) |
6 |
5
|
anassrs |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐴 ) ↔ ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 ) ) |
7 |
6
|
ralbidva |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 ) ) |
8 |
7
|
pm5.32da |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐴 ) ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 ) ) ) |
9 |
2 8
|
bitrd |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐴 ∈ 𝐽 ↔ ( 𝐴 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 ) ) ) |