# Metamath Proof Explorer

## Theorem 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}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
islptre.2 ${⊢}{\phi }\to {A}\subseteq ℝ$
islptre.3 ${⊢}{\phi }\to {B}\in ℝ$
Assertion islptre ${⊢}{\phi }\to \left({B}\in \mathrm{limPt}\left({J}\right)\left({A}\right)↔\forall {a}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {b}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({a},{b}\right)\to \left({a},{b}\right)\cap \left({A}\setminus \left\{{B}\right\}\right)\ne \varnothing \right)\right)$

### Proof

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