Description: The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006) (Revised by Mario Carneiro, 23-Dec-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mopni.1 | ⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) | |
| Assertion | blssopn | ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ⊆ 𝐽 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mopni.1 | ⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) | |
| 2 | blbas | ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ∈ TopBases ) | |
| 3 | bastg | ⊢ ( ran ( ball ‘ 𝐷 ) ∈ TopBases → ran ( ball ‘ 𝐷 ) ⊆ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) | |
| 4 | 2 3 | syl | ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ⊆ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
| 5 | 1 | mopnval | ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
| 6 | 4 5 | sseqtrrd | ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐷 ) ⊆ 𝐽 ) |