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

Theorem neitr 21032
 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 1883 . . . . . 6 𝑑(𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴)
2 nfv 1883 . . . . . . 7 𝑑 𝑐 (𝐽t 𝐴)
3 nfre1 3034 . . . . . . 7 𝑑𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)
42, 3nfan 1868 . . . . . 6 𝑑(𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
51, 4nfan 1868 . . . . 5 𝑑((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
6 simpl 472 . . . . . . 7 ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) → 𝑐 (𝐽t 𝐴))
76anim2i 592 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)))
8 simp-5r 826 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 (𝐽t 𝐴))
9 simp1 1081 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ Top)
10 simp2 1082 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴𝑋)
11 neitr.1 . . . . . . . . . . . . . 14 𝑋 = 𝐽
1211restuni 21014 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 = (𝐽t 𝐴))
139, 10, 12syl2anc 694 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 = (𝐽t 𝐴))
1413ad5antr 773 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴 = (𝐽t 𝐴))
158, 14sseqtr4d 3675 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝐴)
1610ad5antr 773 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴𝑋)
1715, 16sstrd 3646 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝑋)
189ad5antr 773 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐽 ∈ Top)
19 simplr 807 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝐽)
2011eltopss 20760 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑒𝐽) → 𝑒𝑋)
2118, 19, 20syl2anc 694 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝑋)
2221ssdifssd 3781 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑋)
2317, 22unssd 3822 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋)
24 simpr1l 1138 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝐵𝑑)
25243anassrs 1313 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑑)
26 simpr 476 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑 = (𝑒𝐴))
2725, 26sseqtrd 3674 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵 ⊆ (𝑒𝐴))
28 inss1 3866 . . . . . . . . . 10 (𝑒𝐴) ⊆ 𝑒
2927, 28syl6ss 3648 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑒)
30 inundif 4079 . . . . . . . . . 10 ((𝑒𝐴) ∪ (𝑒𝐴)) = 𝑒
31 simpr1r 1139 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝑑𝑐)
32313anassrs 1313 . . . . . . . . . . . 12 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑𝑐)
3326, 32eqsstr3d 3673 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑐)
34 unss1 3815 . . . . . . . . . . 11 ((𝑒𝐴) ⊆ 𝑐 → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3533, 34syl 17 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3630, 35syl5eqssr 3683 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))
37 sseq2 3660 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝐵𝑏𝐵𝑒))
38 sseq1 3659 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴))))
3937, 38anbi12d 747 . . . . . . . . . 10 (𝑏 = 𝑒 → ((𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))) ↔ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))))
4039rspcev 3340 . . . . . . . . 9 ((𝑒𝐽 ∧ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
4119, 29, 36, 40syl12anc 1364 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
42 indir 3908 . . . . . . . . . . 11 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴))
43 incom 3838 . . . . . . . . . . . . 13 (𝐴 ∩ (𝑒𝐴)) = ((𝑒𝐴) ∩ 𝐴)
44 disjdif 4073 . . . . . . . . . . . . 13 (𝐴 ∩ (𝑒𝐴)) = ∅
4543, 44eqtr3i 2675 . . . . . . . . . . . 12 ((𝑒𝐴) ∩ 𝐴) = ∅
4645uneq2i 3797 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴)) = ((𝑐𝐴) ∪ ∅)
47 un0 4000 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ∅) = (𝑐𝐴)
4842, 46, 473eqtri 2677 . . . . . . . . . 10 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = (𝑐𝐴)
49 df-ss 3621 . . . . . . . . . . 11 (𝑐𝐴 ↔ (𝑐𝐴) = 𝑐)
5049biimpi 206 . . . . . . . . . 10 (𝑐𝐴 → (𝑐𝐴) = 𝑐)
5148, 50syl5req 2698 . . . . . . . . 9 (𝑐𝐴𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
5215, 51syl 17 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
53 vex 3234 . . . . . . . . . 10 𝑐 ∈ V
54 vex 3234 . . . . . . . . . . 11 𝑒 ∈ V
55 difexg 4841 . . . . . . . . . . 11 (𝑒 ∈ V → (𝑒𝐴) ∈ V)
5654, 55ax-mp 5 . . . . . . . . . 10 (𝑒𝐴) ∈ V
5753, 56unex 6998 . . . . . . . . 9 (𝑐 ∪ (𝑒𝐴)) ∈ V
58 sseq1 3659 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝑋 ↔ (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋))
59 sseq2 3660 . . . . . . . . . . . . 13 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑏𝑎𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
6059anbi2d 740 . . . . . . . . . . . 12 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝐵𝑏𝑏𝑎) ↔ (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
6160rexbidv 3081 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) ↔ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
6258, 61anbi12d 747 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ↔ ((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))))
63 ineq1 3840 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝐴) = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
6463eqeq2d 2661 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑐 = (𝑎𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)))
6562, 64anbi12d 747 . . . . . . . . 9 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) ↔ (((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))))
6657, 65spcev 3331 . . . . . . . 8 ((((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
6723, 41, 52, 66syl21anc 1365 . . . . . . 7 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
689ad3antrrr 766 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐽 ∈ Top)
69 uniexg 6997 . . . . . . . . . . . 12 (𝐽 ∈ Top → 𝐽 ∈ V)
709, 69syl 17 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ V)
7111, 70syl5eqel 2734 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝑋 ∈ V)
7271, 10ssexd 4838 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 ∈ V)
7372ad3antrrr 766 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐴 ∈ V)
74 simplr 807 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝑑 ∈ (𝐽t 𝐴))
75 elrest 16135 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽t 𝐴) ↔ ∃𝑒𝐽 𝑑 = (𝑒𝐴)))
7675biimpa 500 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽t 𝐴)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7768, 73, 74, 76syl21anc 1365 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7867, 77r19.29a 3107 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
797, 78sylanl1 683 . . . . 5 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
80 simprr 811 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
815, 79, 80r19.29af 3105 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
82 inss2 3867 . . . . . . . . . 10 (𝑎𝐴) ⊆ 𝐴
83 sseq1 3659 . . . . . . . . . 10 (𝑐 = (𝑎𝐴) → (𝑐𝐴 ↔ (𝑎𝐴) ⊆ 𝐴))
8482, 83mpbiri 248 . . . . . . . . 9 (𝑐 = (𝑎𝐴) → 𝑐𝐴)
8584adantl 481 . . . . . . . 8 (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8685exlimiv 1898 . . . . . . 7 (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8786adantl 481 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐𝐴)
8813adantr 480 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝐴 = (𝐽t 𝐴))
8987, 88sseqtrd 3674 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐 (𝐽t 𝐴))
909ad4antr 769 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐽 ∈ Top)
9172ad4antr 769 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐴 ∈ V)
92 simplr 807 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝐽)
93 elrestr 16136 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏𝐽) → (𝑏𝐴) ∈ (𝐽t 𝐴))
9490, 91, 92, 93syl3anc 1366 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ∈ (𝐽t 𝐴))
95 simprl 809 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝑏)
96 simp3 1083 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝐴)
9796ad4antr 769 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝐴)
9895, 97ssind 3870 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵 ⊆ (𝑏𝐴))
99 simprr 811 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝑎)
100 ssrin 3871 . . . . . . . . . . . . . . . 16 (𝑏𝑎 → (𝑏𝐴) ⊆ (𝑎𝐴))
10199, 100syl 17 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ (𝑎𝐴))
102 simp-4r 824 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑐 = (𝑎𝐴))
103101, 102sseqtr4d 3675 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ 𝑐)
10494, 98, 103jca32 557 . . . . . . . . . . . . 13 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
105104ex 449 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) → ((𝐵𝑏𝑏𝑎) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
106105reximdva 3046 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
107106impr 648 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
108107an32s 863 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
109108expl 647 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
110109exlimdv 1901 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
111110imp 444 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
112 sseq2 3660 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝐵𝑑𝐵 ⊆ (𝑏𝐴)))
113 sseq1 3659 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝑑𝑐 ↔ (𝑏𝐴) ⊆ 𝑐))
114112, 113anbi12d 747 . . . . . . . 8 (𝑑 = (𝑏𝐴) → ((𝐵𝑑𝑑𝑐) ↔ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
115114rspcev 3340 . . . . . . 7 (((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
116115rexlimivw 3058 . . . . . 6 (∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
117111, 116syl 17 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
11889, 117jca 553 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
11981, 118impbida 895 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
120 resttop 21012 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽t 𝐴) ∈ Top)
1219, 72, 120syl2anc 694 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝐽t 𝐴) ∈ Top)
12296, 13sseqtrd 3674 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵 (𝐽t 𝐴))
123 eqid 2651 . . . . 5 (𝐽t 𝐴) = (𝐽t 𝐴)
124123isnei 20955 . . . 4 (((𝐽t 𝐴) ∈ Top ∧ 𝐵 (𝐽t 𝐴)) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
125121, 122, 124syl2anc 694 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
126 fvex 6239 . . . . . 6 ((nei‘𝐽)‘𝐵) ∈ V
127 restval 16134 . . . . . 6 ((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
128126, 72, 127sylancr 696 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
129128eleq2d 2716 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))))
13096, 10sstrd 3646 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝑋)
131 eqid 2651 . . . . . . . . 9 (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))
132131elrnmpt 5404 . . . . . . . 8 (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴)))
13353, 132ax-mp 5 . . . . . . 7 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴))
134 df-rex 2947 . . . . . . 7 (∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
135133, 134bitri 264 . . . . . 6 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
13611isnei 20955 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))))
137136anbi1d 741 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐵𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
138137exbidv 1890 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
139135, 138syl5bb 272 . . . . 5 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
1409, 130, 139syl2anc 694 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
141129, 140bitrd 268 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
142119, 125, 1413bitr4d 300 . 2 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴)))
143142eqrdv 2649 1 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((nei‘(𝐽t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523  ∃wex 1744   ∈ wcel 2030  ∃wrex 2942  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ∪ cuni 4468   ↦ cmpt 4762  ran crn 5144  ‘cfv 5926  (class class class)co 6690   ↾t crest 16128  Topctop 20746  neicnei 20949 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-oadd 7609  df-er 7787  df-en 7998  df-fin 8001  df-fi 8358  df-rest 16130  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-nei 20950 This theorem is referenced by:  flfcntr  21894  cnextfres1  21919
 Copyright terms: Public domain W3C validator