islptre

Description: An equivalence condition for a limit point w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	islptre.1	$⊢ J = topGen (ran (.))$
	islptre.2	$⊢ φ \to A \subseteq ℝ$
	islptre.3	$⊢ φ \to B \in ℝ$
Assertion	islptre	$⊢ φ \to (B \in limPt (J) (A) \leftrightarrow \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		islptre.1	$⊢ J = topGen (ran (.))$
2		islptre.2	$⊢ φ \to A \subseteq ℝ$
3		islptre.3	$⊢ φ \to B \in ℝ$
4		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
5	1 4	eqeltri	$⊢ J \in TopOn (ℝ)$
6	5	topontopi	$⊢ J \in Top$
7	6	a1i	$⊢ φ \to J \in Top$
8	5	toponunii	$⊢ ℝ = ⋃ J$
9	8	islp2	$⊢ (J \in Top \land A \subseteq ℝ \land B \in ℝ) \to (B \in limPt (J) (A) \leftrightarrow \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset)$
10	7 2 3 9	syl3anc	$⊢ φ \to (B \in limPt (J) (A) \leftrightarrow \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset)$
11		simp1r	$⊢ ((φ \land \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset) \land (a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset$
12		iooretop	$⊢ (a, b) \in topGen (ran (.))$
13	12 1	eleqtrri	$⊢ (a, b) \in J$
14	13	a1i	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to (a, b) \in J$
15		snssi	$⊢ B \in (a, b) \to \{B\} \subseteq (a, b)$
16	15	adantl	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to \{B\} \subseteq (a, b)$
17		ssidd	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to (a, b) \subseteq (a, b)$
18		sseq2	$⊢ v = (a, b) \to (\{B\} \subseteq v \leftrightarrow \{B\} \subseteq (a, b))$
19		sseq1	$⊢ v = (a, b) \to (v \subseteq (a, b) \leftrightarrow (a, b) \subseteq (a, b))$
20	18 19	anbi12d	$⊢ v = (a, b) \to ((\{B\} \subseteq v \land v \subseteq (a, b)) \leftrightarrow (\{B\} \subseteq (a, b) \land (a, b) \subseteq (a, b)))$
21	20	rspcev	$⊢ ((a, b) \in J \land (\{B\} \subseteq (a, b) \land (a, b) \subseteq (a, b))) \to \exists v \in J (\{B\} \subseteq v \land v \subseteq (a, b))$
22	14 16 17 21	syl12anc	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to \exists v \in J (\{B\} \subseteq v \land v \subseteq (a, b))$
23		ioossre	$⊢ (a, b) \subseteq ℝ$
24	22 23	jctil	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to ((a, b) \subseteq ℝ \land \exists v \in J (\{B\} \subseteq v \land v \subseteq (a, b)))$
25		elioore	$⊢ B \in (a, b) \to B \in ℝ$
26	25	snssd	$⊢ B \in (a, b) \to \{B\} \subseteq ℝ$
27	26	adantl	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to \{B\} \subseteq ℝ$
28	8	isnei	$⊢ (J \in Top \land \{B\} \subseteq ℝ) \to ((a, b) \in nei (J) (\{B\}) \leftrightarrow ((a, b) \subseteq ℝ \land \exists v \in J (\{B\} \subseteq v \land v \subseteq (a, b))))$
29	6 27 28	sylancr	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to ((a, b) \in nei (J) (\{B\}) \leftrightarrow ((a, b) \subseteq ℝ \land \exists v \in J (\{B\} \subseteq v \land v \subseteq (a, b))))$
30	24 29	mpbird	$⊢ ((a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to (a, b) \in nei (J) (\{B\})$
31	30	3adant1	$⊢ ((φ \land \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset) \land (a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to (a, b) \in nei (J) (\{B\})$
32		ineq1	$⊢ n = (a, b) \to n \cap (A ∖ \{B\}) = (a, b) \cap (A ∖ \{B\})$
33	32	neeq1d	$⊢ n = (a, b) \to (n \cap (A ∖ \{B\}) \neq \emptyset \leftrightarrow (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
34	33	rspccva	$⊢ (\forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset \land (a, b) \in nei (J) (\{B\})) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset$
35	11 31 34	syl2anc	$⊢ ((φ \land \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset) \land (a \in ℝ^{} \land b \in ℝ^{}) \land B \in (a, b)) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset$
36	35	3exp	$⊢ (φ \land \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset) \to ((a \in ℝ^{} \land b \in ℝ^{}) \to (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$
37	36	ralrimivv	$⊢ (φ \land \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset) \to \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
38	3	snssd	$⊢ φ \to \{B\} \subseteq ℝ$
39	8	isnei	$⊢ (J \in Top \land \{B\} \subseteq ℝ) \to (n \in nei (J) (\{B\}) \leftrightarrow (n \subseteq ℝ \land \exists v \in J (\{B\} \subseteq v \land v \subseteq n)))$
40	6 38 39	sylancr	$⊢ φ \to (n \in nei (J) (\{B\}) \leftrightarrow (n \subseteq ℝ \land \exists v \in J (\{B\} \subseteq v \land v \subseteq n)))$
41	40	simplbda	$⊢ (φ \land n \in nei (J) (\{B\})) \to \exists v \in J (\{B\} \subseteq v \land v \subseteq n)$
42	1	eleq2i	$⊢ v \in J \leftrightarrow v \in topGen (ran (.))$
43	42	biimpi	$⊢ v \in J \to v \in topGen (ran (.))$
44	43	3ad2ant2	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to v \in topGen (ran (.))$
45		simp1	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to φ$
46		simp3l	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to \{B\} \subseteq v$
47		simpr	$⊢ (φ \land \{B\} \subseteq v) \to \{B\} \subseteq v$
48	3	adantr	$⊢ (φ \land \{B\} \subseteq v) \to B \in ℝ$
49		snssg	$⊢ B \in ℝ \to (B \in v \leftrightarrow \{B\} \subseteq v)$
50	48 49	syl	$⊢ (φ \land \{B\} \subseteq v) \to (B \in v \leftrightarrow \{B\} \subseteq v)$
51	47 50	mpbird	$⊢ (φ \land \{B\} \subseteq v) \to B \in v$
52	45 46 51	syl2anc	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to B \in v$
53	44 52	jca	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to (v \in topGen (ran (.)) \land B \in v)$
54		tg2	$⊢ (v \in topGen (ran (.)) \land B \in v) \to \exists u \in ran (.) (B \in u \land u \subseteq v)$
55		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
56		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
57		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (u \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} u = (a, b))$
58	55 56 57	mp2b	$⊢ u \in ran (.) \leftrightarrow \exists a \in ℝ^{} \exists b \in ℝ^{} u = (a, b)$
59	58	birani	$⊢ (u \in ran (.) \land (B \in u \land u \subseteq v)) \to \exists a \in ℝ^{} \exists b \in ℝ^{} u = (a, b)$
60		simpll	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to B \in u$
61		simpr	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to u = (a, b)$
62	60 61	eleqtrd	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to B \in (a, b)$
63		simplr	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to u \subseteq v$
64	61 63	eqsstrrd	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to (a, b) \subseteq v$
65	62 64	jca	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to (B \in (a, b) \land (a, b) \subseteq v)$
66	65	ex	$⊢ (B \in u \land u \subseteq v) \to (u = (a, b) \to (B \in (a, b) \land (a, b) \subseteq v))$
67	66	adantl	$⊢ (u \in ran (.) \land (B \in u \land u \subseteq v)) \to (u = (a, b) \to (B \in (a, b) \land (a, b) \subseteq v))$
68	67	reximdv	$⊢ (u \in ran (.) \land (B \in u \land u \subseteq v)) \to (\exists b \in ℝ^{} u = (a, b) \to \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq v))$
69	68	reximdv	$⊢ (u \in ran (.) \land (B \in u \land u \subseteq v)) \to (\exists a \in ℝ^{} \exists b \in ℝ^{} u = (a, b) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq v))$
70	59 69	mpd	$⊢ (u \in ran (.) \land (B \in u \land u \subseteq v)) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq v)$
71	70	rexlimiva	$⊢ \exists u \in ran (.) (B \in u \land u \subseteq v) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq v)$
72	53 54 71	3syl	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq v)$
73		simpl3r	$⊢ ((φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \land a \in ℝ^{*}) \to v \subseteq n$
74	73	adantr	$⊢ (((φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \land a \in ℝ^{}) \land b \in ℝ^{}) \to v \subseteq n$
75		sstr	$⊢ ((a, b) \subseteq v \land v \subseteq n) \to (a, b) \subseteq n$
76	75	expcom	$⊢ v \subseteq n \to ((a, b) \subseteq v \to (a, b) \subseteq n)$
77	74 76	syl	$⊢ (((φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \land a \in ℝ^{}) \land b \in ℝ^{}) \to ((a, b) \subseteq v \to (a, b) \subseteq n)$
78	77	anim2d	$⊢ (((φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \land a \in ℝ^{}) \land b \in ℝ^{}) \to ((B \in (a, b) \land (a, b) \subseteq v) \to (B \in (a, b) \land (a, b) \subseteq n))$
79	78	reximdva	$⊢ ((φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \land a \in ℝ^{}) \to (\exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq v) \to \exists b \in ℝ^{*} (B \in (a, b) \land (a, b) \subseteq n))$
80	79	reximdva	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to (\exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq v) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n))$
81	72 80	mpd	$⊢ (φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n)$
82	81	3exp	$⊢ φ \to (v \in J \to ((\{B\} \subseteq v \land v \subseteq n) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n)))$
83	82	rexlimdv	$⊢ φ \to (\exists v \in J (\{B\} \subseteq v \land v \subseteq n) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n))$
84	83	adantr	$⊢ (φ \land n \in nei (J) (\{B\})) \to (\exists v \in J (\{B\} \subseteq v \land v \subseteq n) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n))$
85	41 84	mpd	$⊢ (φ \land n \in nei (J) (\{B\})) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n)$
86	85	adantlr	$⊢ ((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n)$
87		nfv	$⊢ Ⅎ a φ$
88		nfra1	$⊢ Ⅎ a \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
89	87 88	nfan	$⊢ Ⅎ a (φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$
90		nfv	$⊢ Ⅎ a n \in nei (J) (\{B\})$
91	89 90	nfan	$⊢ Ⅎ a ((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\}))$
92		nfv	$⊢ Ⅎ a n \cap (A ∖ \{B\}) \neq \emptyset$
93		nfv	$⊢ Ⅎ b φ$
94		nfra2w	$⊢ Ⅎ b \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
95	93 94	nfan	$⊢ Ⅎ b (φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$
96		nfv	$⊢ Ⅎ b n \in nei (J) (\{B\})$
97	95 96	nfan	$⊢ Ⅎ b ((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\}))$
98		nfv	$⊢ Ⅎ b a \in ℝ^{*}$
99	97 98	nfan	$⊢ Ⅎ b (((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{*})$
100		nfv	$⊢ Ⅎ b n \cap (A ∖ \{B\}) \neq \emptyset$
101		inss1	$⊢ (a, b) \cap (A ∖ \{B\}) \subseteq (a, b)$
102		simp3r	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to (a, b) \subseteq n$
103	101 102	sstrid	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to (a, b) \cap (A ∖ \{B\}) \subseteq n$
104		inss2	$⊢ (a, b) \cap (A ∖ \{B\}) \subseteq A ∖ \{B\}$
105	104	a1i	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to (a, b) \cap (A ∖ \{B\}) \subseteq A ∖ \{B\}$
106	103 105	ssind	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to (a, b) \cap (A ∖ \{B\}) \subseteq n \cap (A ∖ \{B\})$
107		simpllr	$⊢ (((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \to \forall a \in ℝ^{} \forall b \in ℝ^{*} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
108	107	3ad2ant1	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
109		simp1r	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to a \in ℝ^{*}$
110		simp2	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to b \in ℝ^{*}$
111	109 110	jca	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to (a \in ℝ^{} \land b \in ℝ^{})$
112		simp3l	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to B \in (a, b)$
113		rsp2	$⊢ \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset) \to ((a \in ℝ^{} \land b \in ℝ^{}) \to (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$
114	108 111 112 113	syl3c	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset$
115		ssn0	$⊢ ((a, b) \cap (A ∖ \{B\}) \subseteq n \cap (A ∖ \{B\}) \land (a, b) \cap (A ∖ \{B\}) \neq \emptyset) \to n \cap (A ∖ \{B\}) \neq \emptyset$
116	106 114 115	syl2anc	$⊢ ((((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \land b \in ℝ^{} \land (B \in (a, b) \land (a, b) \subseteq n)) \to n \cap (A ∖ \{B\}) \neq \emptyset$
117	116	3exp	$⊢ (((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \to (b \in ℝ^{} \to ((B \in (a, b) \land (a, b) \subseteq n) \to n \cap (A ∖ \{B\}) \neq \emptyset))$
118	99 100 117	rexlimd	$⊢ (((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \land a \in ℝ^{}) \to (\exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n) \to n \cap (A ∖ \{B\}) \neq \emptyset)$
119	118	ex	$⊢ ((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \to (a \in ℝ^{} \to (\exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n) \to n \cap (A ∖ \{B\}) \neq \emptyset))$
120	91 92 119	rexlimd	$⊢ ((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \to (\exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n) \to n \cap (A ∖ \{B\}) \neq \emptyset)$
121	86 120	mpd	$⊢ ((φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \land n \in nei (J) (\{B\})) \to n \cap (A ∖ \{B\}) \neq \emptyset$
122	121	ralrimiva	$⊢ (φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)) \to \forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset$
123	37 122	impbida	$⊢ φ \to (\forall n \in nei (J) (\{B\}) n \cap (A ∖ \{B\}) \neq \emptyset \leftrightarrow \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$
124	10 123	bitrd	$⊢ φ \to (B \in limPt (J) (A) \leftrightarrow \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$

Metamath Proof Explorer

Theorem islptre

Proof