neibl

Description: The neighborhoods around a point P of a metric space are those subsets containing a ball around P . Definition of neighborhood in Kreyszig p. 19. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 23-Dec-2013)

		Ref	Expression
	Hypothesis	mopni.1	$⊢ J = MetOpen (D)$
	Assertion	neibl	$⊢ (D \in ∞Met (X) \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists r \in ℝ^{+} P ball (D) r \subseteq N))$

Proof

Step	Hyp	Ref	Expression
1		mopni.1	$⊢ J = MetOpen (D)$
2	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
3	2	adantr	$⊢ (D \in ∞Met (X) \land P \in X) \to J \in Top$
4	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
5	4	eleq2d	$⊢ D \in ∞Met (X) \to (P \in X \leftrightarrow P \in ⋃ J)$
6	5	biimpa	$⊢ (D \in ∞Met (X) \land P \in X) \to P \in ⋃ J$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	7	isneip	$⊢ (J \in Top \land P \in ⋃ J) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq ⋃ J \land \exists y \in J (P \in y \land y \subseteq N)))$
9	3 6 8	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq ⋃ J \land \exists y \in J (P \in y \land y \subseteq N)))$
10	4	sseq2d	$⊢ D \in ∞Met (X) \to (N \subseteq X \leftrightarrow N \subseteq ⋃ J)$
11	10	adantr	$⊢ (D \in ∞Met (X) \land P \in X) \to (N \subseteq X \leftrightarrow N \subseteq ⋃ J)$
12	11	anbi1d	$⊢ (D \in ∞Met (X) \land P \in X) \to ((N \subseteq X \land \exists y \in J (P \in y \land y \subseteq N)) \leftrightarrow (N \subseteq ⋃ J \land \exists y \in J (P \in y \land y \subseteq N)))$
13	1	mopni2	$⊢ (D \in ∞Met (X) \land y \in J \land P \in y) \to \exists r \in ℝ^{+} P ball (D) r \subseteq y$
14		sstr2	$⊢ P ball (D) r \subseteq y \to (y \subseteq N \to P ball (D) r \subseteq N)$
15	14	com12	$⊢ y \subseteq N \to (P ball (D) r \subseteq y \to P ball (D) r \subseteq N)$
16	15	reximdv	$⊢ y \subseteq N \to (\exists r \in ℝ^{+} P ball (D) r \subseteq y \to \exists r \in ℝ^{+} P ball (D) r \subseteq N)$
17	13 16	syl5com	$⊢ (D \in ∞Met (X) \land y \in J \land P \in y) \to (y \subseteq N \to \exists r \in ℝ^{+} P ball (D) r \subseteq N)$
18	17	3exp	$⊢ D \in ∞Met (X) \to (y \in J \to (P \in y \to (y \subseteq N \to \exists r \in ℝ^{+} P ball (D) r \subseteq N)))$
19	18	imp4a	$⊢ D \in ∞Met (X) \to (y \in J \to ((P \in y \land y \subseteq N) \to \exists r \in ℝ^{+} P ball (D) r \subseteq N))$
20	19	ad2antrr	$⊢ ((D \in ∞Met (X) \land P \in X) \land N \subseteq X) \to (y \in J \to ((P \in y \land y \subseteq N) \to \exists r \in ℝ^{+} P ball (D) r \subseteq N))$
21	20	rexlimdv	$⊢ ((D \in ∞Met (X) \land P \in X) \land N \subseteq X) \to (\exists y \in J (P \in y \land y \subseteq N) \to \exists r \in ℝ^{+} P ball (D) r \subseteq N)$
22		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
23	1	blopn	$⊢ (D \in ∞Met (X) \land P \in X \land r \in ℝ^{*}) \to P ball (D) r \in J$
24	22 23	syl3an3	$⊢ (D \in ∞Met (X) \land P \in X \land r \in ℝ^{+}) \to P ball (D) r \in J$
25		blcntr	$⊢ (D \in ∞Met (X) \land P \in X \land r \in ℝ^{+}) \to P \in (P ball (D) r)$
26		eleq2	$⊢ y = P ball (D) r \to (P \in y \leftrightarrow P \in (P ball (D) r))$
27		sseq1	$⊢ y = P ball (D) r \to (y \subseteq N \leftrightarrow P ball (D) r \subseteq N)$
28	26 27	anbi12d	$⊢ y = P ball (D) r \to ((P \in y \land y \subseteq N) \leftrightarrow (P \in (P ball (D) r) \land P ball (D) r \subseteq N))$
29	28	rspcev	$⊢ (P ball (D) r \in J \land (P \in (P ball (D) r) \land P ball (D) r \subseteq N)) \to \exists y \in J (P \in y \land y \subseteq N)$
30	29	expr	$⊢ (P ball (D) r \in J \land P \in (P ball (D) r)) \to (P ball (D) r \subseteq N \to \exists y \in J (P \in y \land y \subseteq N))$
31	24 25 30	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X \land r \in ℝ^{+}) \to (P ball (D) r \subseteq N \to \exists y \in J (P \in y \land y \subseteq N))$
32	31	3expia	$⊢ (D \in ∞Met (X) \land P \in X) \to (r \in ℝ^{+} \to (P ball (D) r \subseteq N \to \exists y \in J (P \in y \land y \subseteq N)))$
33	32	rexlimdv	$⊢ (D \in ∞Met (X) \land P \in X) \to (\exists r \in ℝ^{+} P ball (D) r \subseteq N \to \exists y \in J (P \in y \land y \subseteq N))$
34	33	adantr	$⊢ ((D \in ∞Met (X) \land P \in X) \land N \subseteq X) \to (\exists r \in ℝ^{+} P ball (D) r \subseteq N \to \exists y \in J (P \in y \land y \subseteq N))$
35	21 34	impbid	$⊢ ((D \in ∞Met (X) \land P \in X) \land N \subseteq X) \to (\exists y \in J (P \in y \land y \subseteq N) \leftrightarrow \exists r \in ℝ^{+} P ball (D) r \subseteq N)$
36	35	pm5.32da	$⊢ (D \in ∞Met (X) \land P \in X) \to ((N \subseteq X \land \exists y \in J (P \in y \land y \subseteq N)) \leftrightarrow (N \subseteq X \land \exists r \in ℝ^{+} P ball (D) r \subseteq N))$
37	9 12 36	3bitr2d	$⊢ (D \in ∞Met (X) \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists r \in ℝ^{+} P ball (D) r \subseteq N))$

Metamath Proof Explorer

Theorem neibl

Proof