Metamath Proof Explorer

Theorem mopni2

Description: An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopni.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion mopni2 ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) β†’ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝐴 )

Proof

Step Hyp Ref Expression
1 mopni.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 1 mopni ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) β†’ βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑃 ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) )
3 1 mopnss ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) β†’ 𝐴 βŠ† 𝑋 )
4 3 sselda ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) ∧ 𝑃 ∈ 𝐴 ) β†’ 𝑃 ∈ 𝑋 )
5 blssex ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑃 ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ↔ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝐴 ) )
6 5 adantlr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑃 ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ↔ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝐴 ) )
7 4 6 syldan ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) ∧ 𝑃 ∈ 𝐴 ) β†’ ( βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑃 ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ↔ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝐴 ) )
8 7 3impa ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) β†’ ( βˆƒ 𝑦 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑃 ∈ 𝑦 ∧ 𝑦 βŠ† 𝐴 ) ↔ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝐴 ) )
9 2 8 mpbid ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) β†’ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝐴 )