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 ‘ 𝐷 ) 𝑥 ) ⊆ 𝐴 ) )