blnei

Description: A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Hypothesis	mopni.1	$⊢ J = MetOpen (D)$
	Assertion	blnei	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{+}) \to P ball (D) R \in nei (J) (\{P\})$

Step	Hyp	Ref	Expression
1		mopni.1	$⊢ J = MetOpen (D)$
2	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
3	2	3ad2ant1	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{+}) \to J \in Top$
4		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
5	1	blopn	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to P ball (D) R \in J$
6	4 5	syl3an3	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{+}) \to P ball (D) R \in J$
7		blcntr	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{+}) \to P \in (P ball (D) R)$
8		opnneip	$⊢ (J \in Top \land P ball (D) R \in J \land P \in (P ball (D) R)) \to P ball (D) R \in nei (J) (\{P\})$
9	3 6 7 8	syl3anc	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{+}) \to P ball (D) R \in nei (J) (\{P\})$

Metamath Proof Explorer