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 𝑋 = 𝐽
Assertion neitr ( ( 𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴 ) → ( ( nei ‘ ( 𝐽t 𝐴 ) ) ‘ 𝐵 ) = ( ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ↾t 𝐴 ) )

Proof

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