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 = ( topGen ` ran (,) )
islptre.2 
|- ( ph -> A C_ RR )
islptre.3 
|- ( ph -> B e. RR )
Assertion islptre 
|- ( ph -> ( B e. ( ( limPt ` J ) ` A ) <-> A. a e. RR* A. b e. RR* ( B e. ( a (,) b ) -> ( ( a (,) b ) i^i ( A \ { B } ) ) =/= (/) ) ) )

Proof

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