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

Proof

Step	Hyp	Ref	Expression
1		mopni.1	$⊢ J = MetOpen (D)$
2	1	mopni	$⊢ (D \in ∞Met (X) \land A \in J \land P \in A) \to \exists y \in ran ball (D) (P \in y \land y \subseteq A)$
3	1	mopnss	$⊢ (D \in ∞Met (X) \land A \in J) \to A \subseteq X$
4	3	sselda	$⊢ ((D \in ∞Met (X) \land A \in J) \land P \in A) \to P \in X$
5		blssex	$⊢ (D \in ∞Met (X) \land P \in X) \to (\exists y \in ran ball (D) (P \in y \land y \subseteq A) \leftrightarrow \exists x \in ℝ^{+} P ball (D) x \subseteq A)$
6	5	adantlr	$⊢ ((D \in ∞Met (X) \land A \in J) \land P \in X) \to (\exists y \in ran ball (D) (P \in y \land y \subseteq A) \leftrightarrow \exists x \in ℝ^{+} P ball (D) x \subseteq A)$
7	4 6	syldan	$⊢ ((D \in ∞Met (X) \land A \in J) \land P \in A) \to (\exists y \in ran ball (D) (P \in y \land y \subseteq A) \leftrightarrow \exists x \in ℝ^{+} P ball (D) x \subseteq A)$
8	7	3impa	$⊢ (D \in ∞Met (X) \land A \in J \land P \in A) \to (\exists y \in ran ball (D) (P \in y \land y \subseteq A) \leftrightarrow \exists x \in ℝ^{+} P ball (D) x \subseteq A)$
9	2 8	mpbid	$⊢ (D \in ∞Met (X) \land A \in J \land P \in A) \to \exists x \in ℝ^{+} P ball (D) x \subseteq A$