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 birani ⊢ ( ( 𝑢 ∈ ran (,) ∧ ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑢 = ( 𝑎 (,) 𝑏 ) )
60 simpll ⊢ ( ( ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ∧ 𝑢 = ( 𝑎 (,) 𝑏 ) ) → 𝐵 ∈ 𝑢 )
61 simpr ⊢ ( ( ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ∧ 𝑢 = ( 𝑎 (,) 𝑏 ) ) → 𝑢 = ( 𝑎 (,) 𝑏 ) )
62 60 61 eleqtrd ⊢ ( ( ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ∧ 𝑢 = ( 𝑎 (,) 𝑏 ) ) → 𝐵 ∈ ( 𝑎 (,) 𝑏 ) )
63 simplr ⊢ ( ( ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ∧ 𝑢 = ( 𝑎 (,) 𝑏 ) ) → 𝑢 ⊆ 𝑣 )
64 61 63 eqsstrrd ⊢ ( ( ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ∧ 𝑢 = ( 𝑎 (,) 𝑏 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 )
65 62 64 jca ⊢ ( ( ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ∧ 𝑢 = ( 𝑎 (,) 𝑏 ) ) → ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) )
66 65 ex ⊢ ( ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) → ( 𝑢 = ( 𝑎 (,) 𝑏 ) → ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) ) )
67 66 adantl ⊢ ( ( 𝑢 ∈ ran (,) ∧ ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ) → ( 𝑢 = ( 𝑎 (,) 𝑏 ) → ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) ) )
68 67 reximdv ⊢ ( ( 𝑢 ∈ ran (,) ∧ ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ) → ( ∃ 𝑏 ∈ ℝ* 𝑢 = ( 𝑎 (,) 𝑏 ) → ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) ) )
69 68 reximdv ⊢ ( ( 𝑢 ∈ ran (,) ∧ ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ) → ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑢 = ( 𝑎 (,) 𝑏 ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) ) )
70 59 69 mpd ⊢ ( ( 𝑢 ∈ ran (,) ∧ ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) )
71 70 rexlimiva ⊢ ( ∃ 𝑢 ∈ ran (,) ( 𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣 ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) )
72 53 54 71 3syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) )
73 simpl3r ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) ∧ 𝑎 ∈ ℝ* ) → 𝑣 ⊆ 𝑛 )
74 73 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ) → 𝑣 ⊆ 𝑛 )
75 sstr ⊢ ( ( ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) → ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 )
76 75 expcom ⊢ ( 𝑣 ⊆ 𝑛 → ( ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 → ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) )
77 74 76 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ) → ( ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 → ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) )
78 77 anim2d ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ) → ( ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) → ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) )
79 78 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) ∧ 𝑎 ∈ ℝ* ) → ( ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) → ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) )
80 79 reximdva ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) → ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑣 ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) )
81 72 80 mpd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) )
82 81 3exp ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐽 → ( ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) ) )
83 82 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝐽 ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) )
84 83 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) → ( ∃ 𝑣 ∈ 𝐽 ( { 𝐵 } ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛 ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) )
85 41 84 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) )
86 85 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) → ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) )
87 nfv ⊢ Ⅎ 𝑎 𝜑
88 nfra1 ⊢ Ⅎ 𝑎 ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ )
89 87 88 nfan ⊢ Ⅎ 𝑎 ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) )
90 nfv ⊢ Ⅎ 𝑎 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } )
91 89 90 nfan ⊢ Ⅎ 𝑎 ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) )
92 nfv ⊢ Ⅎ 𝑎 ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅
93 nfv ⊢ Ⅎ 𝑏 𝜑
94 nfra2w ⊢ Ⅎ 𝑏 ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ )
95 93 94 nfan ⊢ Ⅎ 𝑏 ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) )
96 nfv ⊢ Ⅎ 𝑏 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } )
97 95 96 nfan ⊢ Ⅎ 𝑏 ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) )
98 nfv ⊢ Ⅎ 𝑏 𝑎 ∈ ℝ*
99 97 98 nfan ⊢ Ⅎ 𝑏 ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* )
100 nfv ⊢ Ⅎ 𝑏 ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅
101 inss1 ⊢ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝑎 (,) 𝑏 )
102 simp3r ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 )
103 101 102 sstrid ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ 𝑛 )
104 inss2 ⊢ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝐴 ∖ { 𝐵 } )
105 104 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝐴 ∖ { 𝐵 } ) )
106 103 105 ssind ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) )
107 simpllr ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) → ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) )
108 107 3ad2ant1 ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) )
109 simp1r ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → 𝑎 ∈ ℝ* )
110 simp2 ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → 𝑏 ∈ ℝ* )
111 109 110 jca ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) )
112 simp3l ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → 𝐵 ∈ ( 𝑎 (,) 𝑏 ) )
113 rsp2 ⊢ ( ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) → ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) )
114 108 111 112 113 syl3c ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ )
115 ssn0 ⊢ ( ( ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ∧ ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) → ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ )
116 106 114 115 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) ∧ 𝑏 ∈ ℝ* ∧ ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) ) → ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ )
117 116 3exp ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) → ( 𝑏 ∈ ℝ* → ( ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) → ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) )
118 99 100 117 rexlimd ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) ∧ 𝑎 ∈ ℝ* ) → ( ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) → ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) )
119 118 ex ⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) → ( 𝑎 ∈ ℝ* → ( ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) → ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) )
120 91 92 119 rexlimd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) → ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ 𝑛 ) → ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) )
121 86 120 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) → ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ )
122 121 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ )
123 37 122 impbida ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ( 𝑛 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ↔ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) )
124 10 123 bitrd ⊢ ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑎 ∈ ℝ* ∀ 𝑏 ∈ ℝ* ( 𝐵 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑎 (,) 𝑏 ) ∩ ( 𝐴 ∖ { 𝐵 } ) ) ≠ ∅ ) ) )