lpbl

Description: Every ball around a limit point P of a subset S includes a member of S (even if P e/ S ). (Contributed by NM, 9-Nov-2007) (Revised by Mario Carneiro, 23-Dec-2013)

		Ref	Expression
	Hypothesis	mopni.1	$⊢ J = MetOpen (D)$
	Assertion	lpbl	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to \exists x \in S x \in (P ball (D) R)$

Proof

Step	Hyp	Ref	Expression
1		mopni.1	$⊢ J = MetOpen (D)$
2		ineq1	$⊢ x = P ball (D) R \to x \cap (S ∖ \{P\}) = (P ball (D) R) \cap (S ∖ \{P\})$
3	2	neeq1d	$⊢ x = P ball (D) R \to (x \cap (S ∖ \{P\}) \neq \emptyset \leftrightarrow (P ball (D) R) \cap (S ∖ \{P\}) \neq \emptyset)$
4		simpl3	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to P \in limPt (J) (S)$
5		simpl1	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to D \in ∞Met (X)$
6	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
7	5 6	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to J \in Top$
8		simpl2	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to S \subseteq X$
9	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
10	5 9	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to X = ⋃ J$
11	8 10	sseqtrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to S \subseteq ⋃ J$
12		eqid	$⊢ ⋃ J = ⋃ J$
13	12	lpss	$⊢ (J \in Top \land S \subseteq ⋃ J) \to limPt (J) (S) \subseteq ⋃ J$
14	7 11 13	syl2anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to limPt (J) (S) \subseteq ⋃ J$
15	14 4	sseldd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to P \in ⋃ J$
16	12	islp2	$⊢ (J \in Top \land S \subseteq ⋃ J \land P \in ⋃ J) \to (P \in limPt (J) (S) \leftrightarrow \forall x \in nei (J) (\{P\}) x \cap (S ∖ \{P\}) \neq \emptyset)$
17	7 11 15 16	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to (P \in limPt (J) (S) \leftrightarrow \forall x \in nei (J) (\{P\}) x \cap (S ∖ \{P\}) \neq \emptyset)$
18	4 17	mpbid	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to \forall x \in nei (J) (\{P\}) x \cap (S ∖ \{P\}) \neq \emptyset$
19	15 10	eleqtrrd	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to P \in X$
20		simpr	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to R \in ℝ^{+}$
21	1	blnei	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{+}) \to P ball (D) R \in nei (J) (\{P\})$
22	5 19 20 21	syl3anc	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to P ball (D) R \in nei (J) (\{P\})$
23	3 18 22	rspcdva	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to (P ball (D) R) \cap (S ∖ \{P\}) \neq \emptyset$
24		elin	$⊢ x \in ((P ball (D) R) \cap (S ∖ \{P\})) \leftrightarrow (x \in (P ball (D) R) \land x \in (S ∖ \{P\}))$
25		eldifi	$⊢ x \in (S ∖ \{P\}) \to x \in S$
26	25	anim2i	$⊢ (x \in (P ball (D) R) \land x \in (S ∖ \{P\})) \to (x \in (P ball (D) R) \land x \in S)$
27	26	ancomd	$⊢ (x \in (P ball (D) R) \land x \in (S ∖ \{P\})) \to (x \in S \land x \in (P ball (D) R))$
28	24 27	sylbi	$⊢ x \in ((P ball (D) R) \cap (S ∖ \{P\})) \to (x \in S \land x \in (P ball (D) R))$
29	28	eximi	$⊢ \exists x x \in ((P ball (D) R) \cap (S ∖ \{P\})) \to \exists x (x \in S \land x \in (P ball (D) R))$
30		n0	$⊢ (P ball (D) R) \cap (S ∖ \{P\}) \neq \emptyset \leftrightarrow \exists x x \in ((P ball (D) R) \cap (S ∖ \{P\}))$
31		df-rex	$⊢ \exists x \in S x \in (P ball (D) R) \leftrightarrow \exists x (x \in S \land x \in (P ball (D) R))$
32	29 30 31	3imtr4i	$⊢ (P ball (D) R) \cap (S ∖ \{P\}) \neq \emptyset \to \exists x \in S x \in (P ball (D) R)$
33	23 32	syl	$⊢ ((D \in ∞Met (X) \land S \subseteq X \land P \in limPt (J) (S)) \land R \in ℝ^{+}) \to \exists x \in S x \in (P ball (D) R)$

Metamath Proof Explorer

Theorem lpbl

Proof