islpcn

Description: A characterization for a limit point for the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	islpcn.s	$⊢ φ \to S \subseteq ℂ$
	islpcn.p	$⊢ φ \to P \in ℂ$
Assertion	islpcn	$⊢ φ \to (P \in limPt (TopOpen (ℂ_{fld})) (S) \leftrightarrow \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e)$

Proof

Step	Hyp	Ref	Expression
1		islpcn.s	$⊢ φ \to S \subseteq ℂ$
2		islpcn.p	$⊢ φ \to P \in ℂ$
3		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
4	3	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
5	4	a1i	$⊢ φ \to TopOpen (ℂ_{fld}) \in Top$
6		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
7	6	islp2	$⊢ (TopOpen (ℂ_{fld}) \in Top \land S \subseteq ℂ \land P \in ℂ) \to (P \in limPt (TopOpen (ℂ_{fld})) (S) \leftrightarrow \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset)$
8	5 1 2 7	syl3anc	$⊢ φ \to (P \in limPt (TopOpen (ℂ_{fld})) (S) \leftrightarrow \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset)$
9		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
10	9	a1i	$⊢ (φ \land e \in ℝ^{+}) \to abs \circ - \in ∞Met (ℂ)$
11	2	adantr	$⊢ (φ \land e \in ℝ^{+}) \to P \in ℂ$
12		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
13	3	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
14	13	blnei	$⊢ (abs \circ - \in ∞Met (ℂ) \land P \in ℂ \land e \in ℝ^{+}) \to P ball (abs \circ -) e \in nei (TopOpen (ℂ_{fld})) (\{P\})$
15	10 11 12 14	syl3anc	$⊢ (φ \land e \in ℝ^{+}) \to P ball (abs \circ -) e \in nei (TopOpen (ℂ_{fld})) (\{P\})$
16	15	adantlr	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to P ball (abs \circ -) e \in nei (TopOpen (ℂ_{fld})) (\{P\})$
17		simplr	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset$
18		ineq1	$⊢ n = P ball (abs \circ -) e \to n \cap (S ∖ \{P\}) = (P ball (abs \circ -) e) \cap (S ∖ \{P\})$
19	18	neeq1d	$⊢ n = P ball (abs \circ -) e \to (n \cap (S ∖ \{P\}) \neq \emptyset \leftrightarrow (P ball (abs \circ -) e) \cap (S ∖ \{P\}) \neq \emptyset)$
20	19	rspcva	$⊢ (P ball (abs \circ -) e \in nei (TopOpen (ℂ_{fld})) (\{P\}) \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \to (P ball (abs \circ -) e) \cap (S ∖ \{P\}) \neq \emptyset$
21	16 17 20	syl2anc	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to (P ball (abs \circ -) e) \cap (S ∖ \{P\}) \neq \emptyset$
22		n0	$⊢ (P ball (abs \circ -) e) \cap (S ∖ \{P\}) \neq \emptyset \leftrightarrow \exists x x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))$
23	21 22	sylib	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to \exists x x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))$
24		elinel2	$⊢ x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\})) \to x \in (S ∖ \{P\})$
25	24	adantl	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to x \in (S ∖ \{P\})$
26	1	adantr	$⊢ (φ \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to S \subseteq ℂ$
27	24	eldifad	$⊢ x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\})) \to x \in S$
28	27	adantl	$⊢ (φ \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to x \in S$
29	26 28	sseldd	$⊢ (φ \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to x \in ℂ$
30	2	adantr	$⊢ (φ \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to P \in ℂ$
31	29 30	abssubd	$⊢ (φ \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to \|x - P\| = \|P - x\|$
32		eqid	$⊢ abs \circ - = abs \circ -$
33	32	cnmetdval	$⊢ (P \in ℂ \land x \in ℂ) \to P (abs \circ -) x = \|P - x\|$
34	30 29 33	syl2anc	$⊢ (φ \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to P (abs \circ -) x = \|P - x\|$
35	31 34	eqtr4d	$⊢ (φ \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to \|x - P\| = P (abs \circ -) x$
36	35	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to \|x - P\| = P (abs \circ -) x$
37		elinel1	$⊢ x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\})) \to x \in (P ball (abs \circ -) e)$
38	37	adantl	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to x \in (P ball (abs \circ -) e)$
39	9	a1i	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to abs \circ - \in ∞Met (ℂ)$
40	11	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to P \in ℂ$
41		rpxr	$⊢ e \in ℝ^{+} \to e \in ℝ^{*}$
42	41	ad2antlr	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to e \in ℝ^{*}$
43		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land P \in ℂ \land e \in ℝ^{*}) \to (x \in (P ball (abs \circ -) e) \leftrightarrow (x \in ℂ \land P (abs \circ -) x < e))$
44	39 40 42 43	syl3anc	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to (x \in (P ball (abs \circ -) e) \leftrightarrow (x \in ℂ \land P (abs \circ -) x < e))$
45	38 44	mpbid	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to (x \in ℂ \land P (abs \circ -) x < e)$
46	45	simprd	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to P (abs \circ -) x < e$
47	36 46	eqbrtrd	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to \|x - P\| < e$
48	25 47	jca	$⊢ ((φ \land e \in ℝ^{+}) \land x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\}))) \to (x \in (S ∖ \{P\}) \land \|x - P\| < e)$
49	48	ex	$⊢ (φ \land e \in ℝ^{+}) \to (x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\})) \to (x \in (S ∖ \{P\}) \land \|x - P\| < e))$
50	49	adantlr	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to (x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\})) \to (x \in (S ∖ \{P\}) \land \|x - P\| < e))$
51	50	eximdv	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to (\exists x x \in ((P ball (abs \circ -) e) \cap (S ∖ \{P\})) \to \exists x (x \in (S ∖ \{P\}) \land \|x - P\| < e))$
52	23 51	mpd	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to \exists x (x \in (S ∖ \{P\}) \land \|x - P\| < e)$
53		df-rex	$⊢ \exists x \in (S ∖ \{P\}) \|x - P\| < e \leftrightarrow \exists x (x \in (S ∖ \{P\}) \land \|x - P\| < e)$
54	52 53	sylibr	$⊢ ((φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \land e \in ℝ^{+}) \to \exists x \in (S ∖ \{P\}) \|x - P\| < e$
55	54	ralrimiva	$⊢ (φ \land \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset) \to \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e$
56	9	a1i	$⊢ φ \to abs \circ - \in ∞Met (ℂ)$
57	13	neibl	$⊢ (abs \circ - \in ∞Met (ℂ) \land P \in ℂ) \to (n \in nei (TopOpen (ℂ_{fld})) (\{P\}) \leftrightarrow (n \subseteq ℂ \land \exists e \in ℝ^{+} P ball (abs \circ -) e \subseteq n))$
58	56 2 57	syl2anc	$⊢ φ \to (n \in nei (TopOpen (ℂ_{fld})) (\{P\}) \leftrightarrow (n \subseteq ℂ \land \exists e \in ℝ^{+} P ball (abs \circ -) e \subseteq n))$
59	58	simplbda	$⊢ (φ \land n \in nei (TopOpen (ℂ_{fld})) (\{P\})) \to \exists e \in ℝ^{+} P ball (abs \circ -) e \subseteq n$
60	59	adantlr	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land n \in nei (TopOpen (ℂ_{fld})) (\{P\})) \to \exists e \in ℝ^{+} P ball (abs \circ -) e \subseteq n$
61		nfv	$⊢ Ⅎ e φ$
62		nfra1	$⊢ Ⅎ e \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e$
63	61 62	nfan	$⊢ Ⅎ e (φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e)$
64		nfv	$⊢ Ⅎ e n \in nei (TopOpen (ℂ_{fld})) (\{P\})$
65	63 64	nfan	$⊢ Ⅎ e ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land n \in nei (TopOpen (ℂ_{fld})) (\{P\}))$
66		nfv	$⊢ Ⅎ e n \cap (S ∖ \{P\}) \neq \emptyset$
67		simp1l	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land e \in ℝ^{+} \land P ball (abs \circ -) e \subseteq n) \to φ$
68		simp2	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land e \in ℝ^{+} \land P ball (abs \circ -) e \subseteq n) \to e \in ℝ^{+}$
69	67 68	jca	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land e \in ℝ^{+} \land P ball (abs \circ -) e \subseteq n) \to (φ \land e \in ℝ^{+})$
70		rspa	$⊢ (\forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e \land e \in ℝ^{+}) \to \exists x \in (S ∖ \{P\}) \|x - P\| < e$
71	70	adantll	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land e \in ℝ^{+}) \to \exists x \in (S ∖ \{P\}) \|x - P\| < e$
72	71	3adant3	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land e \in ℝ^{+} \land P ball (abs \circ -) e \subseteq n) \to \exists x \in (S ∖ \{P\}) \|x - P\| < e$
73		simp3	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land e \in ℝ^{+} \land P ball (abs \circ -) e \subseteq n) \to P ball (abs \circ -) e \subseteq n$
74	53	biimpi	$⊢ \exists x \in (S ∖ \{P\}) \|x - P\| < e \to \exists x (x \in (S ∖ \{P\}) \land \|x - P\| < e)$
75	74	ad2antlr	$⊢ (((φ \land e \in ℝ^{+}) \land \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land P ball (abs \circ -) e \subseteq n) \to \exists x (x \in (S ∖ \{P\}) \land \|x - P\| < e)$
76		nfv	$⊢ Ⅎ x (φ \land e \in ℝ^{+})$
77		nfre1	$⊢ Ⅎ x \exists x \in (S ∖ \{P\}) \|x - P\| < e$
78	76 77	nfan	$⊢ Ⅎ x ((φ \land e \in ℝ^{+}) \land \exists x \in (S ∖ \{P\}) \|x - P\| < e)$
79		nfv	$⊢ Ⅎ x P ball (abs \circ -) e \subseteq n$
80	78 79	nfan	$⊢ Ⅎ x (((φ \land e \in ℝ^{+}) \land \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land P ball (abs \circ -) e \subseteq n)$
81		simplr	$⊢ (((φ \land e \in ℝ^{+}) \land P ball (abs \circ -) e \subseteq n) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to P ball (abs \circ -) e \subseteq n$
82	1	adantr	$⊢ (φ \land x \in (S ∖ \{P\})) \to S \subseteq ℂ$
83		eldifi	$⊢ x \in (S ∖ \{P\}) \to x \in S$
84	83	adantl	$⊢ (φ \land x \in (S ∖ \{P\})) \to x \in S$
85	82 84	sseldd	$⊢ (φ \land x \in (S ∖ \{P\})) \to x \in ℂ$
86	85	adantrr	$⊢ (φ \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to x \in ℂ$
87	2	adantr	$⊢ (φ \land x \in (S ∖ \{P\})) \to P \in ℂ$
88	87 85 33	syl2anc	$⊢ (φ \land x \in (S ∖ \{P\})) \to P (abs \circ -) x = \|P - x\|$
89	87 85	abssubd	$⊢ (φ \land x \in (S ∖ \{P\})) \to \|P - x\| = \|x - P\|$
90	88 89	eqtrd	$⊢ (φ \land x \in (S ∖ \{P\})) \to P (abs \circ -) x = \|x - P\|$
91	90	adantrr	$⊢ (φ \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to P (abs \circ -) x = \|x - P\|$
92		simprr	$⊢ (φ \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to \|x - P\| < e$
93	91 92	eqbrtrd	$⊢ (φ \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to P (abs \circ -) x < e$
94	86 93	jca	$⊢ (φ \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to (x \in ℂ \land P (abs \circ -) x < e)$
95	94	adantlr	$⊢ ((φ \land e \in ℝ^{+}) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to (x \in ℂ \land P (abs \circ -) x < e)$
96	9	a1i	$⊢ ((φ \land e \in ℝ^{+}) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to abs \circ - \in ∞Met (ℂ)$
97	11	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to P \in ℂ$
98	41	ad2antlr	$⊢ ((φ \land e \in ℝ^{+}) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to e \in ℝ^{*}$
99	96 97 98 43	syl3anc	$⊢ ((φ \land e \in ℝ^{+}) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to (x \in (P ball (abs \circ -) e) \leftrightarrow (x \in ℂ \land P (abs \circ -) x < e))$
100	95 99	mpbird	$⊢ ((φ \land e \in ℝ^{+}) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to x \in (P ball (abs \circ -) e)$
101	100	adantlr	$⊢ (((φ \land e \in ℝ^{+}) \land P ball (abs \circ -) e \subseteq n) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to x \in (P ball (abs \circ -) e)$
102	81 101	sseldd	$⊢ (((φ \land e \in ℝ^{+}) \land P ball (abs \circ -) e \subseteq n) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to x \in n$
103		simprl	$⊢ (((φ \land e \in ℝ^{+}) \land P ball (abs \circ -) e \subseteq n) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to x \in (S ∖ \{P\})$
104	102 103	elind	$⊢ (((φ \land e \in ℝ^{+}) \land P ball (abs \circ -) e \subseteq n) \land (x \in (S ∖ \{P\}) \land \|x - P\| < e)) \to x \in (n \cap (S ∖ \{P\}))$
105	104	ex	$⊢ ((φ \land e \in ℝ^{+}) \land P ball (abs \circ -) e \subseteq n) \to ((x \in (S ∖ \{P\}) \land \|x - P\| < e) \to x \in (n \cap (S ∖ \{P\})))$
106	105	adantlr	$⊢ (((φ \land e \in ℝ^{+}) \land \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land P ball (abs \circ -) e \subseteq n) \to ((x \in (S ∖ \{P\}) \land \|x - P\| < e) \to x \in (n \cap (S ∖ \{P\})))$
107	80 106	eximd	$⊢ (((φ \land e \in ℝ^{+}) \land \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land P ball (abs \circ -) e \subseteq n) \to (\exists x (x \in (S ∖ \{P\}) \land \|x - P\| < e) \to \exists x x \in (n \cap (S ∖ \{P\})))$
108	75 107	mpd	$⊢ (((φ \land e \in ℝ^{+}) \land \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land P ball (abs \circ -) e \subseteq n) \to \exists x x \in (n \cap (S ∖ \{P\}))$
109		n0	$⊢ n \cap (S ∖ \{P\}) \neq \emptyset \leftrightarrow \exists x x \in (n \cap (S ∖ \{P\}))$
110	108 109	sylibr	$⊢ (((φ \land e \in ℝ^{+}) \land \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land P ball (abs \circ -) e \subseteq n) \to n \cap (S ∖ \{P\}) \neq \emptyset$
111	69 72 73 110	syl21anc	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land e \in ℝ^{+} \land P ball (abs \circ -) e \subseteq n) \to n \cap (S ∖ \{P\}) \neq \emptyset$
112	111	3exp	$⊢ (φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \to (e \in ℝ^{+} \to (P ball (abs \circ -) e \subseteq n \to n \cap (S ∖ \{P\}) \neq \emptyset))$
113	112	adantr	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land n \in nei (TopOpen (ℂ_{fld})) (\{P\})) \to (e \in ℝ^{+} \to (P ball (abs \circ -) e \subseteq n \to n \cap (S ∖ \{P\}) \neq \emptyset))$
114	65 66 113	rexlimd	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land n \in nei (TopOpen (ℂ_{fld})) (\{P\})) \to (\exists e \in ℝ^{+} P ball (abs \circ -) e \subseteq n \to n \cap (S ∖ \{P\}) \neq \emptyset)$
115	60 114	mpd	$⊢ ((φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \land n \in nei (TopOpen (ℂ_{fld})) (\{P\})) \to n \cap (S ∖ \{P\}) \neq \emptyset$
116	115	ralrimiva	$⊢ (φ \land \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e) \to \forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset$
117	55 116	impbida	$⊢ φ \to (\forall n \in nei (TopOpen (ℂ_{fld})) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset \leftrightarrow \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e)$
118	8 117	bitrd	$⊢ φ \to (P \in limPt (TopOpen (ℂ_{fld})) (S) \leftrightarrow \forall e \in ℝ^{+} \exists x \in (S ∖ \{P\}) \|x - P\| < e)$

Metamath Proof Explorer

Theorem islpcn

Proof