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

Theorem neitr 21186
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 1992 . . . . . 6 𝑑(𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴)
2 nfv 1992 . . . . . . 7 𝑑 𝑐 (𝐽t 𝐴)
3 nfre1 3143 . . . . . . 7 𝑑𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)
42, 3nfan 1977 . . . . . 6 𝑑(𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
51, 4nfan 1977 . . . . 5 𝑑((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
6 simpl 474 . . . . . . 7 ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) → 𝑐 (𝐽t 𝐴))
76anim2i 594 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)))
8 simp-5r 831 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 (𝐽t 𝐴))
9 simp1 1131 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ Top)
10 simp2 1132 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴𝑋)
11 neitr.1 . . . . . . . . . . . . . 14 𝑋 = 𝐽
1211restuni 21168 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝐴𝑋) → 𝐴 = (𝐽t 𝐴))
139, 10, 12syl2anc 696 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 = (𝐽t 𝐴))
1413ad5antr 775 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴 = (𝐽t 𝐴))
158, 14sseqtr4d 3783 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝐴)
1610ad5antr 775 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐴𝑋)
1715, 16sstrd 3754 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐𝑋)
189ad5antr 775 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐽 ∈ Top)
19 simplr 809 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝐽)
2011eltopss 20914 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑒𝐽) → 𝑒𝑋)
2118, 19, 20syl2anc 696 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒𝑋)
2221ssdifssd 3891 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑋)
2317, 22unssd 3932 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋)
24 simpr1l 1291 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝐵𝑑)
25243anassrs 1454 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑑)
26 simpr 479 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑 = (𝑒𝐴))
2725, 26sseqtrd 3782 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵 ⊆ (𝑒𝐴))
28 inss1 3976 . . . . . . . . . 10 (𝑒𝐴) ⊆ 𝑒
2927, 28syl6ss 3756 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝐵𝑒)
30 inundif 4190 . . . . . . . . . 10 ((𝑒𝐴) ∪ (𝑒𝐴)) = 𝑒
31 simpr1r 1293 . . . . . . . . . . . . 13 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ ((𝐵𝑑𝑑𝑐) ∧ 𝑒𝐽𝑑 = (𝑒𝐴))) → 𝑑𝑐)
32313anassrs 1454 . . . . . . . . . . . 12 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑑𝑐)
3326, 32eqsstr3d 3781 . . . . . . . . . . 11 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → (𝑒𝐴) ⊆ 𝑐)
34 unss1 3925 . . . . . . . . . . 11 ((𝑒𝐴) ⊆ 𝑐 → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3533, 34syl 17 . . . . . . . . . 10 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ((𝑒𝐴) ∪ (𝑒𝐴)) ⊆ (𝑐 ∪ (𝑒𝐴)))
3630, 35syl5eqssr 3791 . . . . . . . . 9 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))
37 sseq2 3768 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝐵𝑏𝐵𝑒))
38 sseq1 3767 . . . . . . . . . . 11 (𝑏 = 𝑒 → (𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)) ↔ 𝑒 ⊆ (𝑐 ∪ (𝑒𝐴))))
3937, 38anbi12d 749 . . . . . . . . . 10 (𝑏 = 𝑒 → ((𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))) ↔ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))))
4039rspcev 3449 . . . . . . . . 9 ((𝑒𝐽 ∧ (𝐵𝑒𝑒 ⊆ (𝑐 ∪ (𝑒𝐴)))) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
4119, 29, 36, 40syl12anc 1475 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
42 indir 4018 . . . . . . . . . . 11 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴))
43 incom 3948 . . . . . . . . . . . . 13 (𝐴 ∩ (𝑒𝐴)) = ((𝑒𝐴) ∩ 𝐴)
44 disjdif 4184 . . . . . . . . . . . . 13 (𝐴 ∩ (𝑒𝐴)) = ∅
4543, 44eqtr3i 2784 . . . . . . . . . . . 12 ((𝑒𝐴) ∩ 𝐴) = ∅
4645uneq2i 3907 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ((𝑒𝐴) ∩ 𝐴)) = ((𝑐𝐴) ∪ ∅)
47 un0 4110 . . . . . . . . . . 11 ((𝑐𝐴) ∪ ∅) = (𝑐𝐴)
4842, 46, 473eqtri 2786 . . . . . . . . . 10 ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴) = (𝑐𝐴)
49 df-ss 3729 . . . . . . . . . . 11 (𝑐𝐴 ↔ (𝑐𝐴) = 𝑐)
5049biimpi 206 . . . . . . . . . 10 (𝑐𝐴 → (𝑐𝐴) = 𝑐)
5148, 50syl5req 2807 . . . . . . . . 9 (𝑐𝐴𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
5215, 51syl 17 . . . . . . . 8 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
53 vex 3343 . . . . . . . . . 10 𝑐 ∈ V
54 vex 3343 . . . . . . . . . . 11 𝑒 ∈ V
55 difexg 4960 . . . . . . . . . . 11 (𝑒 ∈ V → (𝑒𝐴) ∈ V)
5654, 55ax-mp 5 . . . . . . . . . 10 (𝑒𝐴) ∈ V
5753, 56unex 7121 . . . . . . . . 9 (𝑐 ∪ (𝑒𝐴)) ∈ V
58 sseq1 3767 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝑋 ↔ (𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋))
59 sseq2 3768 . . . . . . . . . . . . 13 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑏𝑎𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))
6059anbi2d 742 . . . . . . . . . . . 12 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝐵𝑏𝑏𝑎) ↔ (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
6160rexbidv 3190 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) ↔ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))))
6258, 61anbi12d 749 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ↔ ((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴))))))
63 ineq1 3950 . . . . . . . . . . 11 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑎𝐴) = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))
6463eqeq2d 2770 . . . . . . . . . 10 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (𝑐 = (𝑎𝐴) ↔ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)))
6562, 64anbi12d 749 . . . . . . . . 9 (𝑎 = (𝑐 ∪ (𝑒𝐴)) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) ↔ (((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴))))
6657, 65spcev 3440 . . . . . . . 8 ((((𝑐 ∪ (𝑒𝐴)) ⊆ 𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏 ⊆ (𝑐 ∪ (𝑒𝐴)))) ∧ 𝑐 = ((𝑐 ∪ (𝑒𝐴)) ∩ 𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
6723, 41, 52, 66syl21anc 1476 . . . . . . 7 (((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) ∧ 𝑒𝐽) ∧ 𝑑 = (𝑒𝐴)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
689ad3antrrr 768 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐽 ∈ Top)
69 uniexg 7120 . . . . . . . . . . . 12 (𝐽 ∈ Top → 𝐽 ∈ V)
709, 69syl 17 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐽 ∈ V)
7111, 70syl5eqel 2843 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝑋 ∈ V)
7271, 10ssexd 4957 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐴 ∈ V)
7372ad3antrrr 768 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝐴 ∈ V)
74 simplr 809 . . . . . . . 8 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → 𝑑 ∈ (𝐽t 𝐴))
75 elrest 16290 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝑑 ∈ (𝐽t 𝐴) ↔ ∃𝑒𝐽 𝑑 = (𝑒𝐴)))
7675biimpa 502 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐴 ∈ V) ∧ 𝑑 ∈ (𝐽t 𝐴)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7768, 73, 74, 76syl21anc 1476 . . . . . . 7 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑒𝐽 𝑑 = (𝑒𝐴))
7867, 77r19.29a 3216 . . . . . 6 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 (𝐽t 𝐴)) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
797, 78sylanl1 685 . . . . 5 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) ∧ 𝑑 ∈ (𝐽t 𝐴)) ∧ (𝐵𝑑𝑑𝑐)) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
80 simprr 813 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
815, 79, 80r19.29af 3214 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))) → ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)))
82 inss2 3977 . . . . . . . . . 10 (𝑎𝐴) ⊆ 𝐴
83 sseq1 3767 . . . . . . . . . 10 (𝑐 = (𝑎𝐴) → (𝑐𝐴 ↔ (𝑎𝐴) ⊆ 𝐴))
8482, 83mpbiri 248 . . . . . . . . 9 (𝑐 = (𝑎𝐴) → 𝑐𝐴)
8584adantl 473 . . . . . . . 8 (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8685exlimiv 2007 . . . . . . 7 (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → 𝑐𝐴)
8786adantl 473 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐𝐴)
8813adantr 472 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝐴 = (𝐽t 𝐴))
8987, 88sseqtrd 3782 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → 𝑐 (𝐽t 𝐴))
909ad4antr 771 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐽 ∈ Top)
9172ad4antr 771 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐴 ∈ V)
92 simplr 809 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝐽)
93 elrestr 16291 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝑏𝐽) → (𝑏𝐴) ∈ (𝐽t 𝐴))
9490, 91, 92, 93syl3anc 1477 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ∈ (𝐽t 𝐴))
95 simprl 811 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝑏)
96 simp3 1133 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝐴)
9796ad4antr 771 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵𝐴)
9895, 97ssind 3980 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝐵 ⊆ (𝑏𝐴))
99 simprr 813 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑏𝑎)
100 ssrin 3981 . . . . . . . . . . . . . . . 16 (𝑏𝑎 → (𝑏𝐴) ⊆ (𝑎𝐴))
10199, 100syl 17 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ (𝑎𝐴))
102 simp-4r 827 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → 𝑐 = (𝑎𝐴))
103101, 102sseqtr4d 3783 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → (𝑏𝐴) ⊆ 𝑐)
10494, 98, 103jca32 559 . . . . . . . . . . . . 13 ((((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) ∧ (𝐵𝑏𝑏𝑎)) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
105104ex 449 . . . . . . . . . . . 12 (((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) ∧ 𝑏𝐽) → ((𝐵𝑏𝑏𝑎) → ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
106105reximdva 3155 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ 𝑎𝑋) → (∃𝑏𝐽 (𝐵𝑏𝑏𝑎) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
107106impr 650 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ 𝑐 = (𝑎𝐴)) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
108107an32s 881 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
109108expl 649 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
110109exlimdv 2010 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴)) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐))))
111110imp 444 . . . . . 6 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
112 sseq2 3768 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝐵𝑑𝐵 ⊆ (𝑏𝐴)))
113 sseq1 3767 . . . . . . . . 9 (𝑑 = (𝑏𝐴) → (𝑑𝑐 ↔ (𝑏𝐴) ⊆ 𝑐))
114112, 113anbi12d 749 . . . . . . . 8 (𝑑 = (𝑏𝐴) → ((𝐵𝑑𝑑𝑐) ↔ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)))
115114rspcev 3449 . . . . . . 7 (((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
116115rexlimivw 3167 . . . . . 6 (∃𝑏𝐽 ((𝑏𝐴) ∈ (𝐽t 𝐴) ∧ (𝐵 ⊆ (𝑏𝐴) ∧ (𝑏𝐴) ⊆ 𝑐)) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
117111, 116syl 17 . . . . 5 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))
11889, 117jca 555 . . . 4 (((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) ∧ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))) → (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)))
11981, 118impbida 913 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
120 resttop 21166 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽t 𝐴) ∈ Top)
1219, 72, 120syl2anc 696 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝐽t 𝐴) ∈ Top)
12296, 13sseqtrd 3782 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵 (𝐽t 𝐴))
123 eqid 2760 . . . . 5 (𝐽t 𝐴) = (𝐽t 𝐴)
124123isnei 21109 . . . 4 (((𝐽t 𝐴) ∈ Top ∧ 𝐵 (𝐽t 𝐴)) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
125121, 122, 124syl2anc 696 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ (𝑐 (𝐽t 𝐴) ∧ ∃𝑑 ∈ (𝐽t 𝐴)(𝐵𝑑𝑑𝑐))))
126 fvex 6362 . . . . . 6 ((nei‘𝐽)‘𝐵) ∈ V
127 restval 16289 . . . . . 6 ((((nei‘𝐽)‘𝐵) ∈ V ∧ 𝐴 ∈ V) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
128126, 72, 127sylancr 698 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (((nei‘𝐽)‘𝐵) ↾t 𝐴) = ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)))
129128eleq2d 2825 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ 𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))))
13096, 10sstrd 3754 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → 𝐵𝑋)
131 eqid 2760 . . . . . . . . 9 (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) = (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴))
132131elrnmpt 5527 . . . . . . . 8 (𝑐 ∈ V → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴)))
13353, 132ax-mp 5 . . . . . . 7 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴))
134 df-rex 3056 . . . . . . 7 (∃𝑎 ∈ ((nei‘𝐽)‘𝐵)𝑐 = (𝑎𝐴) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
135133, 134bitri 264 . . . . . 6 (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)))
13611isnei 21109 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↔ (𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎))))
137136anbi1d 743 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐵𝑋) → ((𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
138137exbidv 1999 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (∃𝑎(𝑎 ∈ ((nei‘𝐽)‘𝐵) ∧ 𝑐 = (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
139135, 138syl5bb 272 . . . . 5 ((𝐽 ∈ Top ∧ 𝐵𝑋) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
1409, 130, 139syl2anc 696 . . . 4 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ran (𝑎 ∈ ((nei‘𝐽)‘𝐵) ↦ (𝑎𝐴)) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
141129, 140bitrd 268 . . 3 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴) ↔ ∃𝑎((𝑎𝑋 ∧ ∃𝑏𝐽 (𝐵𝑏𝑏𝑎)) ∧ 𝑐 = (𝑎𝐴))))
142119, 125, 1413bitr4d 300 . 2 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → (𝑐 ∈ ((nei‘(𝐽t 𝐴))‘𝐵) ↔ 𝑐 ∈ (((nei‘𝐽)‘𝐵) ↾t 𝐴)))
143142eqrdv 2758 1 ((𝐽 ∈ Top ∧ 𝐴𝑋𝐵𝐴) → ((nei‘(𝐽t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  wrex 3051  Vcvv 3340  cdif 3712  cun 3713  cin 3714  wss 3715  c0 4058   cuni 4588  cmpt 4881  ran crn 5267  cfv 6049  (class class class)co 6813  t crest 16283  Topctop 20900  neicnei 21103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-oadd 7733  df-er 7911  df-en 8122  df-fin 8125  df-fi 8482  df-rest 16285  df-topgen 16306  df-top 20901  df-topon 20918  df-bases 20952  df-nei 21104
This theorem is referenced by:  flfcntr  22048  cnextfres1  22073
  Copyright terms: Public domain W3C validator