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 disjdifr 
 |-  ( ( e \ A ) i^i A ) = (/)
44 43 uneq2i 
 |-  ( ( c i^i A ) u. ( ( e \ A ) i^i A ) ) = ( ( c i^i A ) u. (/) )
45 un0 
 |-  ( ( c i^i A ) u. (/) ) = ( c i^i A )
46 42 44 45 3eqtri 
 |-  ( ( c u. ( e \ A ) ) i^i A ) = ( c i^i A )
47 df-ss 
 |-  ( c C_ A <-> ( c i^i A ) = c )
48 47 biimpi 
 |-  ( c C_ A -> ( c i^i A ) = c )
49 46 48 eqtr2id 
 |-  ( c C_ A -> c = ( ( c u. ( e \ A ) ) i^i A ) )
50 15 49 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 ) )
51 vex 
 |-  c e. _V
52 vex 
 |-  e e. _V
53 52 difexi 
 |-  ( e \ A ) e. _V
54 51 53 unex 
 |-  ( c u. ( e \ A ) ) e. _V
55 sseq1 
 |-  ( a = ( c u. ( e \ A ) ) -> ( a C_ X <-> ( c u. ( e \ A ) ) C_ X ) )
56 sseq2 
 |-  ( a = ( c u. ( e \ A ) ) -> ( b C_ a <-> b C_ ( c u. ( e \ A ) ) ) )
57 56 anbi2d 
 |-  ( a = ( c u. ( e \ A ) ) -> ( ( B C_ b /\ b C_ a ) <-> ( B C_ b /\ b C_ ( c u. ( e \ A ) ) ) ) )
58 57 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 ) ) ) ) )
59 55 58 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 ) ) ) ) ) )
60 ineq1 
 |-  ( a = ( c u. ( e \ A ) ) -> ( a i^i A ) = ( ( c u. ( e \ A ) ) i^i A ) )
61 60 eqeq2d 
 |-  ( a = ( c u. ( e \ A ) ) -> ( c = ( a i^i A ) <-> c = ( ( c u. ( e \ A ) ) i^i A ) ) )
62 59 61 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 ) ) ) )
63 54 62 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 ) ) )
64 23 41 50 63 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 ) ) )
65 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 )
66 10 uniexd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> U. J e. _V )
67 1 66 eqeltrid 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> X e. _V )
68 67 11 ssexd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> A e. _V )
69 68 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 )
70 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 ) )
71 elrest 
 |-  ( ( J e. Top /\ A e. _V ) -> ( d e. ( J |`t A ) <-> E. e e. J d = ( e i^i A ) ) )
72 71 biimpa 
 |-  ( ( ( J e. Top /\ A e. _V ) /\ d e. ( J |`t A ) ) -> E. e e. J d = ( e i^i A ) )
73 65 69 70 72 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 ) )
74 64 73 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 ) ) )
75 8 74 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 ) ) )
76 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 ) )
77 6 75 76 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 ) ) )
78 inss2 
 |-  ( a i^i A ) C_ A
79 sseq1 
 |-  ( c = ( a i^i A ) -> ( c C_ A <-> ( a i^i A ) C_ A ) )
80 78 79 mpbiri 
 |-  ( c = ( a i^i A ) -> c C_ A )
81 80 adantl 
 |-  ( ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) -> c C_ A )
82 81 exlimiv 
 |-  ( E. a ( ( a C_ X /\ E. b e. J ( B C_ b /\ b C_ a ) ) /\ c = ( a i^i A ) ) -> c C_ A )
83 82 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 )
84 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 ) )
85 83 84 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 ) )
86 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 )
87 68 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 )
88 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 )
89 elrestr 
 |-  ( ( J e. Top /\ A e. _V /\ b e. J ) -> ( b i^i A ) e. ( J |`t A ) )
90 86 87 88 89 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 ) )
91 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 )
92 simp3 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> B C_ A )
93 92 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 )
94 91 93 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 ) )
95 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 )
96 95 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 ) )
97 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 ) )
98 96 97 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 )
99 90 94 98 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 ) ) )
100 99 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 ) ) ) )
101 100 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 ) ) ) )
102 101 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 ) ) )
103 102 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 ) ) )
104 103 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 ) ) ) )
105 104 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 ) ) ) )
106 105 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 ) ) )
107 sseq2 
 |-  ( d = ( b i^i A ) -> ( B C_ d <-> B C_ ( b i^i A ) ) )
108 sseq1 
 |-  ( d = ( b i^i A ) -> ( d C_ c <-> ( b i^i A ) C_ c ) )
109 107 108 anbi12d 
 |-  ( d = ( b i^i A ) -> ( ( B C_ d /\ d C_ c ) <-> ( B C_ ( b i^i A ) /\ ( b i^i A ) C_ c ) ) )
110 109 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 ) )
111 110 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 ) )
112 106 111 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 ) )
113 85 112 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 ) ) )
114 77 113 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 ) ) ) )
115 resttop 
 |-  ( ( J e. Top /\ A e. _V ) -> ( J |`t A ) e. Top )
116 10 68 115 syl2anc 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( J |`t A ) e. Top )
117 92 13 sseqtrd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> B C_ U. ( J |`t A ) )
118 eqid 
 |-  U. ( J |`t A ) = U. ( J |`t A )
119 118 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 ) ) ) )
120 116 117 119 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 ) ) ) )
121 fvex 
 |-  ( ( nei ` J ) ` B ) e. _V
122 restval 
 |-  ( ( ( ( nei ` J ) ` B ) e. _V /\ A e. _V ) -> ( ( ( nei ` J ) ` B ) |`t A ) = ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) )
123 121 68 122 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 ) ) )
124 123 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 ) ) ) )
125 92 11 sstrd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> B C_ X )
126 eqid 
 |-  ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) = ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) )
127 126 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 ) ) )
128 127 elv 
 |-  ( c e. ran ( a e. ( ( nei ` J ) ` B ) |-> ( a i^i A ) ) <-> E. a e. ( ( nei ` J ) ` B ) c = ( a i^i A ) )
129 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 ) ) )
130 128 129 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 ) ) )
131 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 ) ) ) )
132 131 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 ) ) ) )
133 132 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 ) ) ) )
134 130 133 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 ) ) ) )
135 10 125 134 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 ) ) ) )
136 124 135 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 ) ) ) )
137 114 120 136 3bitr4d 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( c e. ( ( nei ` ( J |`t A ) ) ` B ) <-> c e. ( ( ( nei ` J ) ` B ) |`t A ) ) )
138 137 eqrdv 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( nei ` ( J |`t A ) ) ` B ) = ( ( ( nei ` J ) ` B ) |`t A ) )