This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mopni3

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

Ref Expression
Hypothesis mopni.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion mopni3 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 )
3 2 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 )
4 simp1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
5 1 mopnss ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) → 𝐴 ⊆ 𝑋 )
6 5 sselda ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ) ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝑋 )
7 6 3impa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝑋 )
8 4 7 jca ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) )
9 ssblex ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ) )
10 8 9 sylan ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ) )
11 10 anassrs ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ) )
12 sstr ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 )
13 12 expcom ⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) )
14 13 anim2d ⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 → ( ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ) → ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) ) )
15 14 reximdv ⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 → ( ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) ) )
16 11 15 syl5com ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) ) )
17 16 rexlimdva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑦 ) ⊆ 𝐴 → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) ) )
18 3 17 mpd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+ ( 𝑥 < 𝑅 ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) )