This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dfss2 ⊢ ( 𝑐 ⊆ 𝐴 ↔ ( 𝑐 ∩ 𝐴 ) = 𝑐 )
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 bitrid ⊢ ( ( 𝐽 ∈ 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 𝐴 ) )