This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
islptre.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
islptre.3 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion islptre ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) )

Proof

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