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 ⊢ J = MetOpen ⁡ D
Assertion mopni3 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A ∧ R ∈ ℝ + → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ A

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ J = MetOpen ⁡ D
2 1 mopni2 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → ∃ y ∈ ℝ + P ball ⁡ D y ⊆ A
3 2 adantr ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A ∧ R ∈ ℝ + → ∃ y ∈ ℝ + P ball ⁡ D y ⊆ A
4 simp1 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → D ∈ ∞Met ⁡ X
5 1 mopnss ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J → A ⊆ X
6 5 sselda ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → P ∈ X
7 6 3impa ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → P ∈ X
8 4 7 jca ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → D ∈ ∞Met ⁡ X ∧ P ∈ X
9 ssblex ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ + ∧ y ∈ ℝ + → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ P ball ⁡ D y
10 8 9 sylan ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A ∧ R ∈ ℝ + ∧ y ∈ ℝ + → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ P ball ⁡ D y
11 10 anassrs ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A ∧ R ∈ ℝ + ∧ y ∈ ℝ + → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ P ball ⁡ D y
12 sstr ⊢ P ball ⁡ D x ⊆ P ball ⁡ D y ∧ P ball ⁡ D y ⊆ A → P ball ⁡ D x ⊆ A
13 12 expcom ⊢ P ball ⁡ D y ⊆ A → P ball ⁡ D x ⊆ P ball ⁡ D y → P ball ⁡ D x ⊆ A
14 13 anim2d ⊢ P ball ⁡ D y ⊆ A → x < R ∧ P ball ⁡ D x ⊆ P ball ⁡ D y → x < R ∧ P ball ⁡ D x ⊆ A
15 14 reximdv ⊢ P ball ⁡ D y ⊆ A → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ P ball ⁡ D y → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ A
16 11 15 syl5com ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A ∧ R ∈ ℝ + ∧ y ∈ ℝ + → P ball ⁡ D y ⊆ A → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ A
17 16 rexlimdva ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A ∧ R ∈ ℝ + → ∃ y ∈ ℝ + P ball ⁡ D y ⊆ A → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ A
18 3 17 mpd ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A ∧ R ∈ ℝ + → ∃ x ∈ ℝ + x < R ∧ P ball ⁡ D x ⊆ A