Metamath Proof Explorer


Theorem rnblopn

Description: A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006)

Ref Expression
Hypothesis mopni.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion rnblopn ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ran ( ball β€˜ 𝐷 ) ) β†’ 𝐡 ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 mopni.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 1 blssopn ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ran ( ball β€˜ 𝐷 ) βŠ† 𝐽 )
3 2 sselda ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ran ( ball β€˜ 𝐷 ) ) β†’ 𝐡 ∈ 𝐽 )