Metamath Proof Explorer

Theorem neitr

Description: The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018)

Ref Expression
Hypothesis neitr.1 
|- X = U. J
Assertion neitr 
|- ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( nei ` ( J |`t A ) ) ` B ) = ( ( ( nei ` J ) ` B ) |`t A ) )

Proof

Step Hyp Ref Expression
1 neitr.1 
 |-  X = U. J
2 nfv 
 |-  F/ d ( J e. Top /\ A C_ X /\ B C_ A )
3 nfv 
 |-  F/ d c C_ U. ( J |`t A )
4 nfre1 
 |-  F/ d E. d e. ( J |`t A ) ( B C_ d /\ d C_ c )
5 3 4 nfan 
 |-  F/ d ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) )
6 2 5 nfan 
 |-  F/ d ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) )
7 simpl 
 |-  ( ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) -> c C_ U. ( J |`t A ) )
8 7 anim2i 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) ) -> ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) )
9 simp-5r 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> c C_ U. ( J |`t A ) )
10 simp1 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> J e. Top )
11 simp2 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> A C_ X )
12 1 restuni 
 |-  ( ( J e. Top /\ A C_ X ) -> A = U. ( J |`t A ) )
13 10 11 12 syl2anc 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> A = U. ( J |`t A ) )
14 13 ad5antr 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> A = U. ( J |`t A ) )
15 9 14 sseqtrrd 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> c C_ A )
16 11 ad5antr 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> A C_ X )
17 15 16 sstrd 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> c C_ X )
18 10 ad5antr 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> J e. Top )
19 simplr 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> e e. J )
20 1 eltopss 
 |-  ( ( J e. Top /\ e e. J ) -> e C_ X )
21 18 19 20 syl2anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> e C_ X )
22 21 ssdifssd 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> ( e \ A ) C_ X )
23 17 22 unssd 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> ( c u. ( e \ A ) ) C_ X )
24 simpr1l 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( ( B C_ d /\ d C_ c ) /\ e e. J /\ d = ( e i^i A ) ) ) -> B C_ d )
25 24 3anassrs 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> B C_ d )
26 simpr 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> d = ( e i^i A ) )
27 25 26 sseqtrd 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> B C_ ( e i^i A ) )
28 inss1 
 |-  ( e i^i A ) C_ e
29 27 28 sstrdi 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> B C_ e )
30 inundif 
 |-  ( ( e i^i A ) u. ( e \ A ) ) = e
31 simpr1r 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( ( B C_ d /\ d C_ c ) /\ e e. J /\ d = ( e i^i A ) ) ) -> d C_ c )
32 31 3anassrs 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> d C_ c )
33 26 32 eqsstrrd 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> ( e i^i A ) C_ c )
34 unss1 
 |-  ( ( e i^i A ) C_ c -> ( ( e i^i A ) u. ( e \ A ) ) C_ ( c u. ( e \ A ) ) )
35 33 34 syl 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> ( ( e i^i A ) u. ( e \ A ) ) C_ ( c u. ( e \ A ) ) )
36 30 35 eqsstrrid 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> e C_ ( c u. ( e \ A ) ) )
37 sseq2 
 |-  ( b = e -> ( B C_ b <-> B C_ e ) )
38 sseq1 
 |-  ( b = e -> ( b C_ ( c u. ( e \ A ) ) <-> e C_ ( c u. ( e \ A ) ) ) )
39 37 38 anbi12d 
 |-  ( b = e -> ( ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) <-> ( B C_ e /\ e C_ ( c u. ( e \ A ) ) ) ) )
40 39 rspcev 
 |-  ( ( e e. J /\ ( B C_ e /\ e C_ ( c u. ( e \ A ) ) ) ) -> E. b e. J ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) )
41 19 29 36 40 syl12anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> E. b e. J ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) )
42 indir 
 |-  ( ( c u. ( e \ A ) ) i^i A ) = ( ( c i^i A ) u. ( ( e \ A ) i^i A ) )
43 incom 
 |-  ( A i^i ( e \ A ) ) = ( ( e \ A ) i^i A )
44 disjdif 
 |-  ( A i^i ( e \ A ) ) = (/)
45 43 44 eqtr3i 
 |-  ( ( e \ A ) i^i A ) = (/)
46 45 uneq2i 
 |-  ( ( c i^i A ) u. ( ( e \ A ) i^i A ) ) = ( ( c i^i A ) u. (/) )
47 un0 
 |-  ( ( c i^i A ) u. (/) ) = ( c i^i A )
48 42 46 47 3eqtri 
 |-  ( ( c u. ( e \ A ) ) i^i A ) = ( c i^i A )
49 df-ss 
 |-  ( c C_ A <-> ( c i^i A ) = c )
50 49 biimpi 
 |-  ( c C_ A -> ( c i^i A ) = c )
51 48 50 syl5req 
 |-  ( c C_ A -> c = ( ( c u. ( e \ A ) ) i^i A ) )
52 15 51 syl 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> c = ( ( c u. ( e \ A ) ) i^i A ) )
53 vex 
 |-  c e. _V
54 vex 
 |-  e e. _V
55 54 difexi 
 |-  ( e \ A ) e. _V
56 53 55 unex 
 |-  ( c u. ( e \ A ) ) e. _V
57 sseq1 
 |-  ( a = ( c u. ( e \ A ) ) -> ( a C_ X <-> ( c u. ( e \ A ) ) C_ X ) )
58 sseq2 
 |-  ( a = ( c u. ( e \ A ) ) -> ( b C_ a <-> b C_ ( c u. ( e \ A ) ) ) )
59 58 anbi2d 
 |-  ( a = ( c u. ( e \ A ) ) -> ( ( B C_ b /\ b C_ a ) <-> ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) ) )
60 59 rexbidv 
 |-  ( a = ( c u. ( e \ A ) ) -> ( E. b e. J ( B C_ b /\ b C_ a ) <-> E. b e. J ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) ) )
61 57 60 anbi12d 
 |-  ( a = ( c u. ( e \ A ) ) -> ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) <-> ( ( c u. ( e \ A ) ) C_ X /\ E. b e. J ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) ) ) )
62 ineq1 
 |-  ( a = ( c u. ( e \ A ) ) -> ( a i^i A ) = ( ( c u. ( e \ A ) ) i^i A ) )
63 62 eqeq2d 
 |-  ( a = ( c u. ( e \ A ) ) -> ( c = ( a i^i A ) <-> c = ( ( c u. ( e \ A ) ) i^i A ) ) )
64 61 63 anbi12d 
 |-  ( a = ( c u. ( e \ A ) ) -> ( ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) <-> ( ( ( c u. ( e \ A ) ) C_ X /\ E. b e. J ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) ) /\ c = ( ( c u. ( e \ A ) ) i^i A ) ) ) )
65 56 64 spcev 
 |-  ( ( ( ( c u. ( e \ A ) ) C_ X /\ E. b e. J ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) ) /\ c = ( ( c u. ( e \ A ) ) i^i A ) ) -> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) )
66 23 41 52 65 syl21anc 
 |-  ( ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) /\ e e. J ) /\ d = ( e i^i A ) ) -> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) )
67 10 ad3antrrr 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) -> J e. Top )
68 10 uniexd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> U. J e. _V )
69 1 68 eqeltrid 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> X e. _V )
70 69 11 ssexd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> A e. _V )
71 70 ad3antrrr 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) -> A e. _V )
72 simplr 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) -> d e. ( J |`t A ) )
73 elrest 
 |-  ( ( J e. Top /\ A e. _V ) -> ( d e. ( J |`t A ) <-> E. e e. J d = ( e i^i A ) ) )
74 73 biimpa 
 |-  ( ( ( J e. Top /\ A e. _V ) /\ d e. ( J |`t A ) ) -> E. e e. J d = ( e i^i A ) )
75 67 71 72 74 syl21anc 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) -> E. e e. J d = ( e i^i A ) )
76 66 75 r19.29a 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c C_ U. ( J |`t A ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) -> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) )
77 8 76 sylanl1 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) ) /\ d e. ( J |`t A ) ) /\ ( B C_ d /\ d C_ c ) ) -> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) )
78 simprr 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) ) -> E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) )
79 6 77 78 r19.29af 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) ) -> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) )
80 inss2 
 |-  ( a i^i A ) C_ A
81 sseq1 
 |-  ( c = ( a i^i A ) -> ( c C_ A <-> ( a i^i A ) C_ A ) )
82 80 81 mpbiri 
 |-  ( c = ( a i^i A ) -> c C_ A )
83 82 adantl 
 |-  ( ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) -> c C_ A )
84 83 exlimiv 
 |-  ( E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) -> c C_ A )
85 84 adantl 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) -> c C_ A )
86 13 adantr 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) -> A = U. ( J |`t A ) )
87 85 86 sseqtrd 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) -> c C_ U. ( J |`t A ) )
88 10 ad4antr 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> J e. Top )
89 70 ad4antr 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> A e. _V )
90 simplr 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> b e. J )
91 elrestr 
 |-  ( ( J e. Top /\ A e. _V /\ b e. J ) -> ( b i^i A ) e. ( J |`t A ) )
92 88 89 90 91 syl3anc 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> ( b i^i A ) e. ( J |`t A ) )
93 simprl 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> B C_ b )
94 simp3 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> B C_ A )
95 94 ad4antr 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> B C_ A )
96 93 95 ssind 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> B C_ ( b i^i A ) )
97 simprr 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> b C_ a )
98 97 ssrind 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> ( b i^i A ) C_ ( a i^i A ) )
99 simp-4r 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> c = ( a i^i A ) )
100 98 99 sseqtrrd 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> ( b i^i A ) C_ c )
101 92 96 100 jca32 
 |-  ( ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) /\ ( B C_ b /\ b C_ a ) ) -> ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) )
102 101 ex 
 |-  ( ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) /\ b e. J ) -> ( ( B C_ b /\ b C_ a ) -> ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) ) )
103 102 reximdva 
 |-  ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ a C_ X ) -> ( E. b e. J ( B C_ b /\ b C_ a ) -> E. b e. J ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) ) )
104 103 impr 
 |-  ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ c = ( a i^i A ) ) /\ ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) ) -> E. b e. J ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) )
105 104 an32s 
 |-  ( ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) ) /\ c = ( a i^i A ) ) -> E. b e. J ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) )
106 105 expl 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) -> E. b e. J ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) ) )
107 106 exlimdv 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) -> E. b e. J ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) ) )
108 107 imp 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) -> E. b e. J ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) )
109 sseq2 
 |-  ( d = ( b i^i A ) -> ( B C_ d <-> B C_ ( b i^i A ) ) )
110 sseq1 
 |-  ( d = ( b i^i A ) -> ( d C_ c <-> ( b i^i A ) C_ c ) )
111 109 110 anbi12d 
 |-  ( d = ( b i^i A ) -> ( ( B C_ d /\ d C_ c ) <-> ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) )
112 111 rspcev 
 |-  ( ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) -> E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) )
113 112 rexlimivw 
 |-  ( E. b e. J ( ( b i^i A ) e. ( J |`t A ) /\ ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) -> E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) )
114 108 113 syl 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) -> E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) )
115 87 114 jca 
 |-  ( ( ( J e. Top /\ A C_ X /\ B C_ A ) /\ E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) -> ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) )
116 79 115 impbida 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) <-> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) )
117 resttop 
 |-  ( ( J e. Top /\ A e. _V ) -> ( J |`t A ) e. Top )
118 10 70 117 syl2anc 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( J |`t A ) e. Top )
119 94 13 sseqtrd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> B C_ U. ( J |`t A ) )
120 eqid 
 |-  U. ( J |`t A ) = U. ( J |`t A )
121 120 isnei 
 |-  ( ( ( J |`t A ) e. Top /\ B C_ U. ( J |`t A ) ) -> ( c e. ( ( nei ` ( J |`t A ) ) ` B ) <-> ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) ) )
122 118 119 121 syl2anc 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( c e. ( ( nei ` ( J |`t A ) ) ` B ) <-> ( c C_ U. ( J |`t A ) /\ E. d e. ( J |`t A ) ( B C_ d /\ d C_ c ) ) ) )
123 fvex 
 |-  ( ( nei ` J ) ` B ) e. _V
124 restval 
 |-  ( ( ( ( nei ` J ) ` B ) e. _V /\ A e. _V ) -> ( ( ( nei ` J ) ` B ) |`t A ) = ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) )
125 123 70 124 sylancr 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( ( nei ` J ) ` B ) |`t A ) = ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) )
126 125 eleq2d 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( c e. ( ( ( nei ` J ) ` B ) |`t A ) <-> c e. ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) ) )
127 94 11 sstrd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> B C_ X )
128 eqid 
 |-  ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) = ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) )
129 128 elrnmpt 
 |-  ( c e. _V -> ( c e. ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) <-> E. a e. ( ( nei ` J ) ` B ) c = ( a i^i A ) ) )
130 129 elv 
 |-  ( c e. ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) <-> E. a e. ( ( nei ` J ) ` B ) c = ( a i^i A ) )
131 df-rex 
 |-  ( E. a e. ( ( nei ` J ) ` B ) c = ( a i^i A ) <-> E. a ( a e. ( ( nei ` J ) ` B ) /\ c = ( a i^i A ) ) )
132 130 131 bitri 
 |-  ( c e. ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) <-> E. a ( a e. ( ( nei ` J ) ` B ) /\ c = ( a i^i A ) ) )
133 1 isnei 
 |-  ( ( J e. Top /\ B C_ X ) -> ( a e. ( ( nei ` J ) ` B ) <-> ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) ) )
134 133 anbi1d 
 |-  ( ( J e. Top /\ B C_ X ) -> ( ( a e. ( ( nei ` J ) ` B ) /\ c = ( a i^i A ) ) <-> ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) )
135 134 exbidv 
 |-  ( ( J e. Top /\ B C_ X ) -> ( E. a ( a e. ( ( nei ` J ) ` B ) /\ c = ( a i^i A ) ) <-> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) )
136 132 135 syl5bb 
 |-  ( ( J e. Top /\ B C_ X ) -> ( c e. ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) <-> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) )
137 10 127 136 syl2anc 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( c e. ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) <-> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) )
138 126 137 bitrd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( c e. ( ( ( nei ` J ) ` B ) |`t A ) <-> E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) ) )
139 116 122 138 3bitr4d 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( c e. ( ( nei ` ( J |`t A ) ) ` B ) <-> c e. ( ( ( nei ` J ) ` B ) |`t A ) ) )
140 139 eqrdv 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( nei ` ( J |`t A ) ) ` B ) = ( ( ( nei ` J ) ` B ) |`t A ) )