# Metamath Proof Explorer

## Theorem dvreslem

Description: Lemma for dvres . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Commute the consequent and shorten proof. (Revised by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypotheses dvres.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
dvres.t ${⊢}{T}={K}{↾}_{𝑡}{S}$
dvres.g ${⊢}{G}=\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)$
dvres.s ${⊢}{\phi }\to {S}\subseteq ℂ$
dvres.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
dvres.a ${⊢}{\phi }\to {A}\subseteq {S}$
dvres.b ${⊢}{\phi }\to {B}\subseteq {S}$
dvres.y ${⊢}{\phi }\to {y}\in ℂ$
Assertion dvreslem ${⊢}{\phi }\to \left({x}{\left({{F}↾}_{{B}}\right)}_{{S}}^{\prime }{y}↔\left({x}\in \mathrm{int}\left({T}\right)\left({B}\right)\wedge {x}{{F}}_{{S}}^{\prime }{y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dvres.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 dvres.t ${⊢}{T}={K}{↾}_{𝑡}{S}$
3 dvres.g ${⊢}{G}=\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)$
4 dvres.s ${⊢}{\phi }\to {S}\subseteq ℂ$
5 dvres.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
6 dvres.a ${⊢}{\phi }\to {A}\subseteq {S}$
7 dvres.b ${⊢}{\phi }\to {B}\subseteq {S}$
8 dvres.y ${⊢}{\phi }\to {y}\in ℂ$
9 difss ${⊢}\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\subseteq {A}\cap {B}$
10 inss2 ${⊢}{A}\cap {B}\subseteq {B}$
11 9 10 sstri ${⊢}\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\subseteq {B}$
12 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\wedge {z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\right)\to {z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)$
13 11 12 sseldi ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\wedge {z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\right)\to {z}\in {B}$
14 13 fvresd ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\wedge {z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\right)\to \left({{F}↾}_{{B}}\right)\left({z}\right)={F}\left({z}\right)$
15 1 cnfldtop ${⊢}{K}\in \mathrm{Top}$
16 cnex ${⊢}ℂ\in \mathrm{V}$
17 ssexg ${⊢}\left({S}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to {S}\in \mathrm{V}$
18 4 16 17 sylancl ${⊢}{\phi }\to {S}\in \mathrm{V}$
19 resttop ${⊢}\left({K}\in \mathrm{Top}\wedge {S}\in \mathrm{V}\right)\to {K}{↾}_{𝑡}{S}\in \mathrm{Top}$
20 15 18 19 sylancr ${⊢}{\phi }\to {K}{↾}_{𝑡}{S}\in \mathrm{Top}$
21 2 20 eqeltrid ${⊢}{\phi }\to {T}\in \mathrm{Top}$
22 inss1 ${⊢}{A}\cap {B}\subseteq {A}$
23 22 6 sstrid ${⊢}{\phi }\to {A}\cap {B}\subseteq {S}$
24 1 cnfldtopon ${⊢}{K}\in \mathrm{TopOn}\left(ℂ\right)$
25 resttopon ${⊢}\left({K}\in \mathrm{TopOn}\left(ℂ\right)\wedge {S}\subseteq ℂ\right)\to {K}{↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
26 24 4 25 sylancr ${⊢}{\phi }\to {K}{↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
27 2 26 eqeltrid ${⊢}{\phi }\to {T}\in \mathrm{TopOn}\left({S}\right)$
28 toponuni ${⊢}{T}\in \mathrm{TopOn}\left({S}\right)\to {S}=\bigcup {T}$
29 27 28 syl ${⊢}{\phi }\to {S}=\bigcup {T}$
30 23 29 sseqtrd ${⊢}{\phi }\to {A}\cap {B}\subseteq \bigcup {T}$
31 eqid ${⊢}\bigcup {T}=\bigcup {T}$
32 31 ntrss2 ${⊢}\left({T}\in \mathrm{Top}\wedge {A}\cap {B}\subseteq \bigcup {T}\right)\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq {A}\cap {B}$
33 21 30 32 syl2anc ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq {A}\cap {B}$
34 33 10 sstrdi ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq {B}$
35 34 sselda ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {x}\in {B}$
36 35 fvresd ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({{F}↾}_{{B}}\right)\left({x}\right)={F}\left({x}\right)$
37 36 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\wedge {z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\right)\to \left({{F}↾}_{{B}}\right)\left({x}\right)={F}\left({x}\right)$
38 14 37 oveq12d ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\wedge {z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\right)\to \left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)={F}\left({z}\right)-{F}\left({x}\right)$
39 38 oveq1d ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\wedge {z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\right)\to \frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}=\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}$
40 39 mpteq2dva ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right)=\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)$
41 3 reseq1i ${⊢}{{G}↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}={\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}$
42 ssdif ${⊢}{A}\cap {B}\subseteq {A}\to \left({A}\cap {B}\right)\setminus \left\{{x}\right\}\subseteq {A}\setminus \left\{{x}\right\}$
43 resmpt ${⊢}\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\subseteq {A}\setminus \left\{{x}\right\}\to {\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}=\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)$
44 22 42 43 mp2b ${⊢}{\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}=\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)$
45 41 44 eqtri ${⊢}{{G}↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}=\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)$
46 40 45 syl6eqr ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right)={{G}↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}$
47 46 oveq1d ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}=\left({{G}↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}\right){lim}_{ℂ}{x}$
48 5 adantr ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {F}:{A}⟶ℂ$
49 6 4 sstrd ${⊢}{\phi }\to {A}\subseteq ℂ$
50 49 adantr ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {A}\subseteq ℂ$
51 33 22 sstrdi ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq {A}$
52 51 sselda ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {x}\in {A}$
53 48 50 52 dvlem ${⊢}\left(\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\wedge {z}\in \left({A}\setminus \left\{{x}\right\}\right)\right)\to \frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\in ℂ$
54 53 3 fmptd ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {G}:{A}\setminus \left\{{x}\right\}⟶ℂ$
55 22 42 mp1i ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({A}\cap {B}\right)\setminus \left\{{x}\right\}\subseteq {A}\setminus \left\{{x}\right\}$
56 difss ${⊢}{A}\setminus \left\{{x}\right\}\subseteq {A}$
57 56 50 sstrid ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {A}\setminus \left\{{x}\right\}\subseteq ℂ$
58 eqid ${⊢}{K}{↾}_{𝑡}\left(\left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)={K}{↾}_{𝑡}\left(\left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)$
59 difssd ${⊢}{\phi }\to \bigcup {T}\setminus {A}\subseteq \bigcup {T}$
60 30 59 unssd ${⊢}{\phi }\to \left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\subseteq \bigcup {T}$
61 ssun1 ${⊢}{A}\cap {B}\subseteq \left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)$
62 61 a1i ${⊢}{\phi }\to {A}\cap {B}\subseteq \left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)$
63 31 ntrss ${⊢}\left({T}\in \mathrm{Top}\wedge \left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\subseteq \bigcup {T}\wedge {A}\cap {B}\subseteq \left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\right)\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq \mathrm{int}\left({T}\right)\left(\left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\right)$
64 21 60 62 63 syl3anc ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq \mathrm{int}\left({T}\right)\left(\left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\right)$
65 64 51 ssind ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq \mathrm{int}\left({T}\right)\left(\left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\right)\cap {A}$
66 6 29 sseqtrd ${⊢}{\phi }\to {A}\subseteq \bigcup {T}$
67 22 a1i ${⊢}{\phi }\to {A}\cap {B}\subseteq {A}$
68 eqid ${⊢}{T}{↾}_{𝑡}{A}={T}{↾}_{𝑡}{A}$
69 31 68 restntr ${⊢}\left({T}\in \mathrm{Top}\wedge {A}\subseteq \bigcup {T}\wedge {A}\cap {B}\subseteq {A}\right)\to \mathrm{int}\left({T}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)=\mathrm{int}\left({T}\right)\left(\left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\right)\cap {A}$
70 21 66 67 69 syl3anc ${⊢}{\phi }\to \mathrm{int}\left({T}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)=\mathrm{int}\left({T}\right)\left(\left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\right)\cap {A}$
71 2 oveq1i ${⊢}{T}{↾}_{𝑡}{A}=\left({K}{↾}_{𝑡}{S}\right){↾}_{𝑡}{A}$
72 15 a1i ${⊢}{\phi }\to {K}\in \mathrm{Top}$
73 restabs ${⊢}\left({K}\in \mathrm{Top}\wedge {A}\subseteq {S}\wedge {S}\in \mathrm{V}\right)\to \left({K}{↾}_{𝑡}{S}\right){↾}_{𝑡}{A}={K}{↾}_{𝑡}{A}$
74 72 6 18 73 syl3anc ${⊢}{\phi }\to \left({K}{↾}_{𝑡}{S}\right){↾}_{𝑡}{A}={K}{↾}_{𝑡}{A}$
75 71 74 syl5eq ${⊢}{\phi }\to {T}{↾}_{𝑡}{A}={K}{↾}_{𝑡}{A}$
76 75 fveq2d ${⊢}{\phi }\to \mathrm{int}\left({T}{↾}_{𝑡}{A}\right)=\mathrm{int}\left({K}{↾}_{𝑡}{A}\right)$
77 76 fveq1d ${⊢}{\phi }\to \mathrm{int}\left({T}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)=\mathrm{int}\left({K}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)$
78 70 77 eqtr3d ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left(\left({A}\cap {B}\right)\cup \left(\bigcup {T}\setminus {A}\right)\right)\cap {A}=\mathrm{int}\left({K}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)$
79 65 78 sseqtrd ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\subseteq \mathrm{int}\left({K}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)$
80 79 sselda ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {x}\in \mathrm{int}\left({K}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)$
81 undif1 ${⊢}\left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}={A}\cup \left\{{x}\right\}$
82 33 sselda ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {x}\in \left({A}\cap {B}\right)$
83 82 snssd ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left\{{x}\right\}\subseteq {A}\cap {B}$
84 83 22 sstrdi ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left\{{x}\right\}\subseteq {A}$
85 ssequn2 ${⊢}\left\{{x}\right\}\subseteq {A}↔{A}\cup \left\{{x}\right\}={A}$
86 84 85 sylib ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {A}\cup \left\{{x}\right\}={A}$
87 81 86 syl5eq ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}={A}$
88 87 oveq2d ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {K}{↾}_{𝑡}\left(\left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)={K}{↾}_{𝑡}{A}$
89 88 fveq2d ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \mathrm{int}\left({K}{↾}_{𝑡}\left(\left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)\right)=\mathrm{int}\left({K}{↾}_{𝑡}{A}\right)$
90 undif1 ${⊢}\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}=\left({A}\cap {B}\right)\cup \left\{{x}\right\}$
91 ssequn2 ${⊢}\left\{{x}\right\}\subseteq {A}\cap {B}↔\left({A}\cap {B}\right)\cup \left\{{x}\right\}={A}\cap {B}$
92 83 91 sylib ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({A}\cap {B}\right)\cup \left\{{x}\right\}={A}\cap {B}$
93 90 92 syl5eq ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}={A}\cap {B}$
94 89 93 fveq12d ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \mathrm{int}\left({K}{↾}_{𝑡}\left(\left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)\right)\left(\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)=\mathrm{int}\left({K}{↾}_{𝑡}{A}\right)\left({A}\cap {B}\right)$
95 80 94 eleqtrrd ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to {x}\in \mathrm{int}\left({K}{↾}_{𝑡}\left(\left({A}\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)\right)\left(\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)\cup \left\{{x}\right\}\right)$
96 54 55 57 1 58 95 limcres ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({{G}↾}_{\left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)}\right){lim}_{ℂ}{x}={G}{lim}_{ℂ}{x}$
97 47 96 eqtrd ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}={G}{lim}_{ℂ}{x}$
98 97 eleq2d ${⊢}\left({\phi }\wedge {x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\right)\to \left({y}\in \left(\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)↔{y}\in \left({G}{lim}_{ℂ}{x}\right)\right)$
99 98 pm5.32da ${⊢}{\phi }\to \left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\wedge {y}\in \left(\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)↔\left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)\right)$
100 7 29 sseqtrd ${⊢}{\phi }\to {B}\subseteq \bigcup {T}$
101 31 ntrin ${⊢}\left({T}\in \mathrm{Top}\wedge {A}\subseteq \bigcup {T}\wedge {B}\subseteq \bigcup {T}\right)\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)=\mathrm{int}\left({T}\right)\left({A}\right)\cap \mathrm{int}\left({T}\right)\left({B}\right)$
102 21 66 100 101 syl3anc ${⊢}{\phi }\to \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)=\mathrm{int}\left({T}\right)\left({A}\right)\cap \mathrm{int}\left({T}\right)\left({B}\right)$
103 102 eleq2d ${⊢}{\phi }\to \left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)↔{x}\in \left(\mathrm{int}\left({T}\right)\left({A}\right)\cap \mathrm{int}\left({T}\right)\left({B}\right)\right)\right)$
104 elin ${⊢}{x}\in \left(\mathrm{int}\left({T}\right)\left({A}\right)\cap \mathrm{int}\left({T}\right)\left({B}\right)\right)↔\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)$
105 103 104 syl6bb ${⊢}{\phi }\to \left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)↔\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)\right)$
106 105 anbi1d ${⊢}{\phi }\to \left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)↔\left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)\right)$
107 99 106 bitrd ${⊢}{\phi }\to \left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\wedge {y}\in \left(\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)↔\left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)\right)$
108 an32 ${⊢}\left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)↔\left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)$
109 107 108 syl6bb ${⊢}{\phi }\to \left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\wedge {y}\in \left(\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)↔\left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)\right)$
110 eqid ${⊢}\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right)=\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right)$
111 fresin ${⊢}{F}:{A}⟶ℂ\to \left({{F}↾}_{{B}}\right):{A}\cap {B}⟶ℂ$
112 5 111 syl ${⊢}{\phi }\to \left({{F}↾}_{{B}}\right):{A}\cap {B}⟶ℂ$
113 2 1 110 4 112 23 eldv ${⊢}{\phi }\to \left({x}{\left({{F}↾}_{{B}}\right)}_{{S}}^{\prime }{y}↔\left({x}\in \mathrm{int}\left({T}\right)\left({A}\cap {B}\right)\wedge {y}\in \left(\left({z}\in \left(\left({A}\cap {B}\right)\setminus \left\{{x}\right\}\right)⟼\frac{\left({{F}↾}_{{B}}\right)\left({z}\right)-\left({{F}↾}_{{B}}\right)\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)\right)$
114 2 1 3 4 5 6 eldv ${⊢}{\phi }\to \left({x}{{F}}_{{S}}^{\prime }{y}↔\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)\right)$
115 114 anbi1cd ${⊢}{\phi }\to \left(\left({x}\in \mathrm{int}\left({T}\right)\left({B}\right)\wedge {x}{{F}}_{{S}}^{\prime }{y}\right)↔\left(\left({x}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {y}\in \left({G}{lim}_{ℂ}{x}\right)\right)\wedge {x}\in \mathrm{int}\left({T}\right)\left({B}\right)\right)\right)$
116 109 113 115 3bitr4d ${⊢}{\phi }\to \left({x}{\left({{F}↾}_{{B}}\right)}_{{S}}^{\prime }{y}↔\left({x}\in \mathrm{int}\left({T}\right)\left({B}\right)\wedge {x}{{F}}_{{S}}^{\prime }{y}\right)\right)$