MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neitr Structured version   Visualization version   GIF version

Theorem neitr 23203
Description: The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018.)
Hypothesis
Ref Expression
neitr.1 𝑋 = 𝐽
Assertion
Ref Expression
neitr ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((nei‘(𝐽t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))

Proof of Theorem neitr
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1911 . . . . . 6 𝑑(𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴)
2 nfv 1911 . . . . . . 7 𝑑 𝑐 (𝐽t 𝐴)
3 nfre1 3282 . . . . . . 7 𝑑𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)
42, 3nfan 1896 . . . . . 6 𝑑(𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
51, 4nfan 1896 . . . . 5 𝑑((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
6 simpl 482 . . . . . . 7 ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) → 𝑐 (𝐽t 𝐴))
76anim2i 617 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)))
8 simp-5r 786 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 (𝐽t 𝐴))
9 simp1 1135 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ Top)
10 simp2 1136 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴𝑋)
11 neitr.1 . . . . . . . . . . . . . 14 𝑋 = 𝐽
1211restuni 23185 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 = (𝐽t 𝐴))
139, 10, 12syl2anc 584 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 = (𝐽t 𝐴))
1413ad5antr 734 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴 = (𝐽t 𝐴))
158, 14sseqtrrd 4036 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝐴)
1610ad5antr 734 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴𝑋)
1715, 16sstrd 4005 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝑋)
189ad5antr 734 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐽 ∈ Top)
19 simplr 769 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝐽)
2011eltopss 22928 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑒𝐽) → 𝑒𝑋)
2118, 19, 20syl2anc 584 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝑋)
2221ssdifssd 4156 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑋)
2317, 22unssd 4201 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋)
24 simpr1l 1229 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝐵𝑑)
25243anassrs 1359 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑑)
26 simpr 484 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑 = (𝑒𝐴))
2725, 26sseqtrd 4035 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵 ⊆ (𝑒𝐴))
28 inss1 4244 . . . . . . . . . 10 (𝑒𝐴) ⊆ 𝑒
2927, 28sstrdi 4007 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑒)
30 inundif 4484 . . . . . . . . . 10 ((𝑒𝐴) ∪ (𝑒𝐴)) = 𝑒
31 simpr1r 1230 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝑑𝑐)
32313anassrs 1359 . . . . . . . . . . . 12 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑𝑐)
3326, 32eqsstrrd 4034 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑐)
34 unss1 4194 . . . . . . . . . . 11 ((𝑒𝐴) ⊆ 𝑐 → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3533, 34syl 17 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3630, 35eqsstrrid 4044 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))
37 sseq2 4021 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝐵𝑏𝐵𝑒))
38 sseq1 4020 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴))))
3937, 38anbi12d 632 . . . . . . . . . 10 (𝑏 = 𝑒 → ((𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))) ↔ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))))
4039rspcev 3621 . . . . . . . . 9 ((𝑒𝐽 ∧ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
4119, 29, 36, 40syl12anc 837 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
42 indir 4291 . . . . . . . . . . 11 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴))
43 disjdifr 4478 . . . . . . . . . . . 12 ((𝑒𝐴) ∩ 𝐴) = ∅
4443uneq2i 4174 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴)) = ((𝑐𝐴) ∪ ∅)
45 un0 4399 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ∅) = (𝑐𝐴)
4642, 44, 453eqtri 2766 . . . . . . . . . 10 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = (𝑐𝐴)
47 dfss2 3980 . . . . . . . . . . 11 (𝑐𝐴 ↔ (𝑐𝐴) = 𝑐)
4847biimpi 216 . . . . . . . . . 10 (𝑐𝐴 → (𝑐𝐴) = 𝑐)
4946, 48eqtr2id 2787 . . . . . . . . 9 (𝑐𝐴𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
5015, 49syl 17 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
51 vex 3481 . . . . . . . . . 10 𝑐 ∈ V
52 vex 3481 . . . . . . . . . . 11 𝑒 ∈ V
5352difexi 5335 . . . . . . . . . 10 (𝑒𝐴) ∈ V
5451, 53unex 7762 . . . . . . . . 9 (𝑐 ∪ (𝑒𝐴)) ∈ V
55 sseq1 4020 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝑋 ↔ (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋))
56 sseq2 4021 . . . . . . . . . . . . 13 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑏𝑎𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
5756anbi2d 630 . . . . . . . . . . . 12 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝐵𝑏𝑏𝑎) ↔ (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
5857rexbidv 3176 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) ↔ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
5955, 58anbi12d 632 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ↔ ((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))))
60 ineq1 4220 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝐴) = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
6160eqeq2d 2745 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑐 = (𝑎𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)))
6259, 61anbi12d 632 . . . . . . . . 9 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) ↔ (((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))))
6354, 62spcev 3605 . . . . . . . 8 ((((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
6423, 41, 50, 63syl21anc 838 . . . . . . 7 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
659ad3antrrr 730 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐽 ∈ Top)
669uniexd 7760 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ V)
6711, 66eqeltrid 2842 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝑋 ∈ V)
6867, 10ssexd 5329 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 ∈ V)
6968ad3antrrr 730 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐴 ∈ V)
70 simplr 769 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝑑 ∈ (𝐽t 𝐴))
71 elrest 17473 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽t 𝐴) ↔ ∃𝑒𝐽 𝑑 = (𝑒𝐴)))
7271biimpa 476 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽t 𝐴)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7365, 69, 70, 72syl21anc 838 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7464, 73r19.29a 3159 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
757, 74sylanl1 680 . . . . 5 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
76 simprr 773 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
775, 75, 76r19.29af 3265 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
78 inss2 4245 . . . . . . . . . 10 (𝑎𝐴) ⊆ 𝐴
79 sseq1 4020 . . . . . . . . . 10 (𝑐 = (𝑎𝐴) → (𝑐𝐴 ↔ (𝑎𝐴) ⊆ 𝐴))
8078, 79mpbiri 258 . . . . . . . . 9 (𝑐 = (𝑎𝐴) → 𝑐𝐴)
8180adantl 481 . . . . . . . 8 (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8281exlimiv 1927 . . . . . . 7 (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8382adantl 481 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐𝐴)
8413adantr 480 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝐴 = (𝐽t 𝐴))
8583, 84sseqtrd 4035 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐 (𝐽t 𝐴))
869ad4antr 732 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐽 ∈ Top)
8768ad4antr 732 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐴 ∈ V)
88 simplr 769 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝐽)
89 elrestr 17474 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏𝐽) → (𝑏𝐴) ∈ (𝐽t 𝐴))
9086, 87, 88, 89syl3anc 1370 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ∈ (𝐽t 𝐴))
91 simprl 771 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝑏)
92 simp3 1137 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝐴)
9392ad4antr 732 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝐴)
9491, 93ssind 4248 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵 ⊆ (𝑏𝐴))
95 simprr 773 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝑎)
9695ssrind 4251 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ (𝑎𝐴))
97 simp-4r 784 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑐 = (𝑎𝐴))
9896, 97sseqtrrd 4036 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ 𝑐)
9990, 94, 98jca32 515 . . . . . . . . . . . . 13 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
10099ex 412 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) → ((𝐵𝑏𝑏𝑎) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
101100reximdva 3165 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
102101impr 454 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
103102an32s 652 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
104103expl 457 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
105104exlimdv 1930 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
106105imp 406 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
107 sseq2 4021 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝐵𝑑𝐵 ⊆ (𝑏𝐴)))
108 sseq1 4020 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝑑𝑐 ↔ (𝑏𝐴) ⊆ 𝑐))
109107, 108anbi12d 632 . . . . . . . 8 (𝑑 = (𝑏𝐴) → ((𝐵𝑑𝑑𝑐) ↔ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
110109rspcev 3621 . . . . . . 7 (((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
111110rexlimivw 3148 . . . . . 6 (∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
112106, 111syl 17 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
11385, 112jca 511 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
11477, 113impbida 801 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
115 resttop 23183 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽t 𝐴) ∈ Top)
1169, 68, 115syl2anc 584 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝐽t 𝐴) ∈ Top)
11792, 13sseqtrd 4035 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵 (𝐽t 𝐴))
118 eqid 2734 . . . . 5 (𝐽t 𝐴) = (𝐽t 𝐴)
119118isnei 23126 . . . 4 (((𝐽t 𝐴) ∈ Top ∧ 𝐵 (𝐽t 𝐴)) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
120116, 117, 119syl2anc 584 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
121 fvex 6919 . . . . . 6 ((nei‘𝐽)‘𝐵) ∈ V
122 restval 17472 . . . . . 6 ((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
123121, 68, 122sylancr 587 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
124123eleq2d 2824 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))))
12592, 10sstrd 4005 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝑋)
126 eqid 2734 . . . . . . . . 9 (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))
127126elrnmpt 5971 . . . . . . . 8 (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴)))
128127elv 3482 . . . . . . 7 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴))
129 df-rex 3068 . . . . . . 7 (∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
130128, 129bitri 275 . . . . . 6 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
13111isnei 23126 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))))
132131anbi1d 631 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐵𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
133132exbidv 1918 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
134130, 133bitrid 283 . . . . 5 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
1359, 125, 134syl2anc 584 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
136124, 135bitrd 279 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
137114, 120, 1363bitr4d 311 . 2 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴)))
138137eqrdv 2732 1 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((nei‘(𝐽t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338   cuni 4911  cmpt 5230  ran crn 5689  cfv 6562  (class class class)co 7430  t crest 17466  Topctop 22914  neicnei 23120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-en 8984  df-fin 8987  df-fi 9448  df-rest 17468  df-topgen 17489  df-top 22915  df-topon 22932  df-bases 22968  df-nei 23121
This theorem is referenced by:  flfcntr  24066  cnextfres1  24091
  Copyright terms: Public domain W3C validator