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

Theorem neitr 22676
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 1918 . . . . . 6 𝑑(𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴)
2 nfv 1918 . . . . . . 7 𝑑 𝑐 (𝐽t 𝐴)
3 nfre1 3283 . . . . . . 7 𝑑𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)
42, 3nfan 1903 . . . . . 6 𝑑(𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
51, 4nfan 1903 . . . . 5 𝑑((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
6 simpl 484 . . . . . . 7 ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) → 𝑐 (𝐽t 𝐴))
76anim2i 618 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)))
8 simp-5r 785 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 (𝐽t 𝐴))
9 simp1 1137 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ Top)
10 simp2 1138 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴𝑋)
11 neitr.1 . . . . . . . . . . . . . 14 𝑋 = 𝐽
1211restuni 22658 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 = (𝐽t 𝐴))
139, 10, 12syl2anc 585 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 = (𝐽t 𝐴))
1413ad5antr 733 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴 = (𝐽t 𝐴))
158, 14sseqtrrd 4023 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝐴)
1610ad5antr 733 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴𝑋)
1715, 16sstrd 3992 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝑋)
189ad5antr 733 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐽 ∈ Top)
19 simplr 768 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝐽)
2011eltopss 22401 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑒𝐽) → 𝑒𝑋)
2118, 19, 20syl2anc 585 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝑋)
2221ssdifssd 4142 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑋)
2317, 22unssd 4186 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋)
24 simpr1l 1231 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝐵𝑑)
25243anassrs 1361 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑑)
26 simpr 486 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑 = (𝑒𝐴))
2725, 26sseqtrd 4022 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵 ⊆ (𝑒𝐴))
28 inss1 4228 . . . . . . . . . 10 (𝑒𝐴) ⊆ 𝑒
2927, 28sstrdi 3994 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑒)
30 inundif 4478 . . . . . . . . . 10 ((𝑒𝐴) ∪ (𝑒𝐴)) = 𝑒
31 simpr1r 1232 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝑑𝑐)
32313anassrs 1361 . . . . . . . . . . . 12 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑𝑐)
3326, 32eqsstrrd 4021 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑐)
34 unss1 4179 . . . . . . . . . . 11 ((𝑒𝐴) ⊆ 𝑐 → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3533, 34syl 17 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3630, 35eqsstrrid 4031 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))
37 sseq2 4008 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝐵𝑏𝐵𝑒))
38 sseq1 4007 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴))))
3937, 38anbi12d 632 . . . . . . . . . 10 (𝑏 = 𝑒 → ((𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))) ↔ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))))
4039rspcev 3613 . . . . . . . . 9 ((𝑒𝐽 ∧ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
4119, 29, 36, 40syl12anc 836 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
42 indir 4275 . . . . . . . . . . 11 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴))
43 disjdifr 4472 . . . . . . . . . . . 12 ((𝑒𝐴) ∩ 𝐴) = ∅
4443uneq2i 4160 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴)) = ((𝑐𝐴) ∪ ∅)
45 un0 4390 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ∅) = (𝑐𝐴)
4642, 44, 453eqtri 2765 . . . . . . . . . 10 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = (𝑐𝐴)
47 df-ss 3965 . . . . . . . . . . 11 (𝑐𝐴 ↔ (𝑐𝐴) = 𝑐)
4847biimpi 215 . . . . . . . . . 10 (𝑐𝐴 → (𝑐𝐴) = 𝑐)
4946, 48eqtr2id 2786 . . . . . . . . 9 (𝑐𝐴𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
5015, 49syl 17 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
51 vex 3479 . . . . . . . . . 10 𝑐 ∈ V
52 vex 3479 . . . . . . . . . . 11 𝑒 ∈ V
5352difexi 5328 . . . . . . . . . 10 (𝑒𝐴) ∈ V
5451, 53unex 7730 . . . . . . . . 9 (𝑐 ∪ (𝑒𝐴)) ∈ V
55 sseq1 4007 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝑋 ↔ (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋))
56 sseq2 4008 . . . . . . . . . . . . 13 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑏𝑎𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
5756anbi2d 630 . . . . . . . . . . . 12 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝐵𝑏𝑏𝑎) ↔ (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
5857rexbidv 3179 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) ↔ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
5955, 58anbi12d 632 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ↔ ((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))))
60 ineq1 4205 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝐴) = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
6160eqeq2d 2744 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑐 = (𝑎𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)))
6259, 61anbi12d 632 . . . . . . . . 9 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) ↔ (((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))))
6354, 62spcev 3597 . . . . . . . 8 ((((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
6423, 41, 50, 63syl21anc 837 . . . . . . 7 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
659ad3antrrr 729 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐽 ∈ Top)
669uniexd 7729 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ V)
6711, 66eqeltrid 2838 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝑋 ∈ V)
6867, 10ssexd 5324 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 ∈ V)
6968ad3antrrr 729 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐴 ∈ V)
70 simplr 768 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝑑 ∈ (𝐽t 𝐴))
71 elrest 17370 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽t 𝐴) ↔ ∃𝑒𝐽 𝑑 = (𝑒𝐴)))
7271biimpa 478 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽t 𝐴)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7365, 69, 70, 72syl21anc 837 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7464, 73r19.29a 3163 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
757, 74sylanl1 679 . . . . 5 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
76 simprr 772 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
775, 75, 76r19.29af 3266 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
78 inss2 4229 . . . . . . . . . 10 (𝑎𝐴) ⊆ 𝐴
79 sseq1 4007 . . . . . . . . . 10 (𝑐 = (𝑎𝐴) → (𝑐𝐴 ↔ (𝑎𝐴) ⊆ 𝐴))
8078, 79mpbiri 258 . . . . . . . . 9 (𝑐 = (𝑎𝐴) → 𝑐𝐴)
8180adantl 483 . . . . . . . 8 (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8281exlimiv 1934 . . . . . . 7 (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8382adantl 483 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐𝐴)
8413adantr 482 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝐴 = (𝐽t 𝐴))
8583, 84sseqtrd 4022 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐 (𝐽t 𝐴))
869ad4antr 731 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐽 ∈ Top)
8768ad4antr 731 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐴 ∈ V)
88 simplr 768 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝐽)
89 elrestr 17371 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏𝐽) → (𝑏𝐴) ∈ (𝐽t 𝐴))
9086, 87, 88, 89syl3anc 1372 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ∈ (𝐽t 𝐴))
91 simprl 770 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝑏)
92 simp3 1139 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝐴)
9392ad4antr 731 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝐴)
9491, 93ssind 4232 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵 ⊆ (𝑏𝐴))
95 simprr 772 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝑎)
9695ssrind 4235 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ (𝑎𝐴))
97 simp-4r 783 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑐 = (𝑎𝐴))
9896, 97sseqtrrd 4023 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ 𝑐)
9990, 94, 98jca32 517 . . . . . . . . . . . . 13 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
10099ex 414 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) → ((𝐵𝑏𝑏𝑎) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
101100reximdva 3169 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
102101impr 456 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
103102an32s 651 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
104103expl 459 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
105104exlimdv 1937 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
106105imp 408 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
107 sseq2 4008 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝐵𝑑𝐵 ⊆ (𝑏𝐴)))
108 sseq1 4007 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝑑𝑐 ↔ (𝑏𝐴) ⊆ 𝑐))
109107, 108anbi12d 632 . . . . . . . 8 (𝑑 = (𝑏𝐴) → ((𝐵𝑑𝑑𝑐) ↔ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
110109rspcev 3613 . . . . . . 7 (((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
111110rexlimivw 3152 . . . . . 6 (∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
112106, 111syl 17 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
11385, 112jca 513 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
11477, 113impbida 800 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
115 resttop 22656 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽t 𝐴) ∈ Top)
1169, 68, 115syl2anc 585 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝐽t 𝐴) ∈ Top)
11792, 13sseqtrd 4022 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵 (𝐽t 𝐴))
118 eqid 2733 . . . . 5 (𝐽t 𝐴) = (𝐽t 𝐴)
119118isnei 22599 . . . 4 (((𝐽t 𝐴) ∈ Top ∧ 𝐵 (𝐽t 𝐴)) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
120116, 117, 119syl2anc 585 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
121 fvex 6902 . . . . . 6 ((nei‘𝐽)‘𝐵) ∈ V
122 restval 17369 . . . . . 6 ((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
123121, 68, 122sylancr 588 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
124123eleq2d 2820 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))))
12592, 10sstrd 3992 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝑋)
126 eqid 2733 . . . . . . . . 9 (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))
127126elrnmpt 5954 . . . . . . . 8 (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴)))
128127elv 3481 . . . . . . 7 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴))
129 df-rex 3072 . . . . . . 7 (∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
130128, 129bitri 275 . . . . . 6 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
13111isnei 22599 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))))
132131anbi1d 631 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐵𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
133132exbidv 1925 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
134130, 133bitrid 283 . . . . 5 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
1359, 125, 134syl2anc 585 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
136124, 135bitrd 279 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
137114, 120, 1363bitr4d 311 . 2 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴)))
138137eqrdv 2731 1 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((nei‘(𝐽t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  wrex 3071  Vcvv 3475  cdif 3945  cun 3946  cin 3947  wss 3948  c0 4322   cuni 4908  cmpt 5231  ran crn 5677  cfv 6541  (class class class)co 7406  t crest 17363  Topctop 22387  neicnei 22593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-en 8937  df-fin 8940  df-fi 9403  df-rest 17365  df-topgen 17386  df-top 22388  df-topon 22405  df-bases 22441  df-nei 22594
This theorem is referenced by:  flfcntr  23539  cnextfres1  23564
  Copyright terms: Public domain W3C validator