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	biimpi	$⊢ u \in ran (.) \to \exists a \in ℝ^{} \exists b \in ℝ^{} u = (a, b)$
60	59	adantr	$⊢ (u \in ran (.) \land (B \in u \land u \subseteq v)) \to \exists a \in ℝ^{} \exists b \in ℝ^{} u = (a, b)$
61		simpll	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to B \in u$
62		simpr	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to u = (a, b)$
63	61 62	eleqtrd	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to B \in (a, b)$
64		simplr	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to u \subseteq v$
65	62 64	eqsstrrd	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to (a, b) \subseteq v$
66	63 65	jca	$⊢ ((B \in u \land u \subseteq v) \land u = (a, b)) \to (B \in (a, b) \land (a, b) \subseteq v)$
67	66	ex	$⊢ (B \in u \land u \subseteq v) \to (u = (a, b) \to (B \in (a, b) \land (a, b) \subseteq v))$
68	67	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))$
69	68	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))$
70	69	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))$
71	60 70	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)$
72	71	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)$
73	53 54 72	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)$
74		simpl3r	$⊢ ((φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \land a \in ℝ^{*}) \to v \subseteq n$
75	74	adantr	$⊢ (((φ \land v \in J \land (\{B\} \subseteq v \land v \subseteq n)) \land a \in ℝ^{}) \land b \in ℝ^{}) \to v \subseteq n$
76		sstr	$⊢ ((a, b) \subseteq v \land v \subseteq n) \to (a, b) \subseteq n$
77	76	expcom	$⊢ v \subseteq n \to ((a, b) \subseteq v \to (a, b) \subseteq n)$
78	75 77	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)$
79	78	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))$
80	79	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))$
81	80	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))$
82	73 81	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)$
83	82	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)))$
84	83	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))$
85	84	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))$
86	41 85	mpd	$⊢ (φ \land n \in nei (J) (\{B\})) \to \exists a \in ℝ^{} \exists b \in ℝ^{} (B \in (a, b) \land (a, b) \subseteq n)$
87	86	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)$
88		nfv	$⊢ Ⅎ a φ$
89		nfra1	$⊢ Ⅎ a \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
90	88 89	nfan	$⊢ Ⅎ a (φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$
91		nfv	$⊢ Ⅎ a n \in nei (J) (\{B\})$
92	90 91	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\}))$
93		nfv	$⊢ Ⅎ a n \cap (A ∖ \{B\}) \neq \emptyset$
94		nfv	$⊢ Ⅎ b φ$
95		nfra2w	$⊢ Ⅎ b \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset)$
96	94 95	nfan	$⊢ Ⅎ b (φ \land \forall a \in ℝ^{} \forall b \in ℝ^{} (B \in (a, b) \to (a, b) \cap (A ∖ \{B\}) \neq \emptyset))$
97		nfv	$⊢ Ⅎ b n \in nei (J) (\{B\})$
98	96 97	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\}))$
99		nfv	$⊢ Ⅎ b a \in ℝ^{*}$
100	98 99	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 ℝ^{*})$
101		nfv	$⊢ Ⅎ b n \cap (A ∖ \{B\}) \neq \emptyset$
102		inss1	$⊢ (a, b) \cap (A ∖ \{B\}) \subseteq (a, b)$
103		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$
104	102 103	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$
105		inss2	$⊢ (a, b) \cap (A ∖ \{B\}) \subseteq A ∖ \{B\}$
106	105	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\}$
107	104 106	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\})$
108		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)$
109	108	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)$
110		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 ℝ^{*}$
111		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 ℝ^{*}$
112	110 111	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 ℝ^{})$
113		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)$
114		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))$
115	109 112 113 114	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$
116		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$
117	107 115 116	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$
118	117	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))$
119	100 101 118	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)$
120	119	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))$
121	92 93 120	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)$
122	87 121	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$
123	122	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$
124	37 123	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))$
125	10 124	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