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 \in ∞Met (X) \land A \in J \land P \in A) \land R \in ℝ^{+}) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq A)$

Proof

Step	Hyp	Ref	Expression
1		mopni.1	$⊢ J = MetOpen (D)$
2	1	mopni2	$⊢ (D \in ∞Met (X) \land A \in J \land P \in A) \to \exists y \in ℝ^{+} P ball (D) y \subseteq A$
3	2	adantr	$⊢ ((D \in ∞Met (X) \land A \in J \land P \in A) \land R \in ℝ^{+}) \to \exists y \in ℝ^{+} P ball (D) y \subseteq A$
4		simp1	$⊢ (D \in ∞Met (X) \land A \in J \land P \in A) \to D \in ∞Met (X)$
5	1	mopnss	$⊢ (D \in ∞Met (X) \land A \in J) \to A \subseteq X$
6	5	sselda	$⊢ ((D \in ∞Met (X) \land A \in J) \land P \in A) \to P \in X$
7	6	3impa	$⊢ (D \in ∞Met (X) \land A \in J \land P \in A) \to P \in X$
8	4 7	jca	$⊢ (D \in ∞Met (X) \land A \in J \land P \in A) \to (D \in ∞Met (X) \land P \in X)$
9		ssblex	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land y \in ℝ^{+})) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq P ball (D) y)$
10	8 9	sylan	$⊢ ((D \in ∞Met (X) \land A \in J \land P \in A) \land (R \in ℝ^{+} \land y \in ℝ^{+})) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq P ball (D) y)$
11	10	anassrs	$⊢ (((D \in ∞Met (X) \land A \in J \land P \in A) \land R \in ℝ^{+}) \land y \in ℝ^{+}) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq P ball (D) y)$
12		sstr	$⊢ (P ball (D) x \subseteq P ball (D) y \land P ball (D) y \subseteq A) \to P ball (D) x \subseteq A$
13	12	expcom	$⊢ P ball (D) y \subseteq A \to (P ball (D) x \subseteq P ball (D) y \to P ball (D) x \subseteq A)$
14	13	anim2d	$⊢ P ball (D) y \subseteq A \to ((x < R \land P ball (D) x \subseteq P ball (D) y) \to (x < R \land P ball (D) x \subseteq A))$
15	14	reximdv	$⊢ P ball (D) y \subseteq A \to (\exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq P ball (D) y) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq A))$
16	11 15	syl5com	$⊢ (((D \in ∞Met (X) \land A \in J \land P \in A) \land R \in ℝ^{+}) \land y \in ℝ^{+}) \to (P ball (D) y \subseteq A \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq A))$
17	16	rexlimdva	$⊢ ((D \in ∞Met (X) \land A \in J \land P \in A) \land R \in ℝ^{+}) \to (\exists y \in ℝ^{+} P ball (D) y \subseteq A \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq A))$
18	3 17	mpd	$⊢ ((D \in ∞Met (X) \land A \in J \land P \in A) \land R \in ℝ^{+}) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq A)$