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 ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
dvres.t ⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
dvres.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
dvres.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
dvres.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
dvres.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )
dvres.y ⊢ ( 𝜑 → 𝑦 ∈ ℂ )
Assertion dvreslem ( 𝜑 → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 dvres.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2 dvres.t ⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
3 dvres.g ⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
4 dvres.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
5 dvres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
6 dvres.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
7 dvres.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )
8 dvres.y ⊢ ( 𝜑 → 𝑦 ∈ ℂ )
9 difss ⊢ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ ( 𝐴 ∩ 𝐵 )
10 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
11 9 10 sstri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ 𝐵
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) → 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) )
13 11 12 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) → 𝑧 ∈ 𝐵 )
14 13 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
15 1 cnfldtop ⊢ 𝐾 ∈ Top
16 cnex ⊢ ℂ ∈ V
17 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
18 4 16 17 sylancl ⊢ ( 𝜑 → 𝑆 ∈ V )
19 resttop ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐾 ↾t 𝑆 ) ∈ Top )
20 15 18 19 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ Top )
21 2 20 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ Top )
22 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
23 22 6 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑆 )
24 1 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
25 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
26 24 4 25 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
27 2 26 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ( TopOn ‘ 𝑆 ) )
28 toponuni ⊢ ( 𝑇 ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ 𝑇 )
29 27 28 syl ⊢ ( 𝜑 → 𝑆 = ∪ 𝑇 )
30 23 29 sseqtrd ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝑇 )
31 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
32 31 ntrss2 ⊢ ( ( 𝑇 ∈ Top ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝑇 ) → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
33 21 30 32 syl2anc ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
34 33 10 sstrdi ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐵 )
35 34 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝑥 ∈ 𝐵 )
36 35 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
38 14 37 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) )
39 38 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) → ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
40 39 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) )
41 3 reseq1i ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) )
42 ssdif ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ ( 𝐴 ∖ { 𝑥 } ) )
43 resmpt ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ ( 𝐴 ∖ { 𝑥 } ) → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) )
44 22 42 43 mp2b ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
45 41 44 eqtri ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
46 40 45 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) )
47 46 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) = ( ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) limℂ 𝑥 ) )
48 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐹 : 𝐴 ⟶ ℂ )
49 6 4 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐴 ⊆ ℂ )
51 33 22 sstrdi ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐴 )
52 51 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝑥 ∈ 𝐴 )
53 48 50 52 dvlem ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ∈ ℂ )
54 53 3 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐺 : ( 𝐴 ∖ { 𝑥 } ) ⟶ ℂ )
55 22 42 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ⊆ ( 𝐴 ∖ { 𝑥 } ) )
56 difss ⊢ ( 𝐴 ∖ { 𝑥 } ) ⊆ 𝐴
57 56 50 sstrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐴 ∖ { 𝑥 } ) ⊆ ℂ )
58 eqid ⊢ ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) )
59 difssd ⊢ ( 𝜑 → ( ∪ 𝑇 ∖ 𝐴 ) ⊆ ∪ 𝑇 )
60 30 59 unssd ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ⊆ ∪ 𝑇 )
61 ssun1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) )
62 61 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) )
63 31 ntrss ⊢ ( ( 𝑇 ∈ Top ∧ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ⊆ ∪ 𝑇 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ) → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ) )
64 21 60 62 63 syl3anc ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ) )
65 64 51 ssind ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ) ∩ 𝐴 ) )
66 6 29 sseqtrd ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝑇 )
67 22 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 )
68 eqid ⊢ ( 𝑇 ↾t 𝐴 ) = ( 𝑇 ↾t 𝐴 )
69 31 68 restntr ⊢ ( ( 𝑇 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑇 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( ( int ‘ ( 𝑇 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ) ∩ 𝐴 ) )
70 21 66 67 69 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝑇 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ) ∩ 𝐴 ) )
71 2 oveq1i ⊢ ( 𝑇 ↾t 𝐴 ) = ( ( 𝐾 ↾t 𝑆 ) ↾t 𝐴 )
72 15 a1i ⊢ ( 𝜑 → 𝐾 ∈ Top )
73 restabs ⊢ ( ( 𝐾 ∈ Top ∧ 𝐴 ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( 𝐾 ↾t 𝑆 ) ↾t 𝐴 ) = ( 𝐾 ↾t 𝐴 ) )
74 72 6 18 73 syl3anc ⊢ ( 𝜑 → ( ( 𝐾 ↾t 𝑆 ) ↾t 𝐴 ) = ( 𝐾 ↾t 𝐴 ) )
75 71 74 syl5eq ⊢ ( 𝜑 → ( 𝑇 ↾t 𝐴 ) = ( 𝐾 ↾t 𝐴 ) )
76 75 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝑇 ↾t 𝐴 ) ) = ( int ‘ ( 𝐾 ↾t 𝐴 ) ) )
77 76 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( 𝑇 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( int ‘ ( 𝐾 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
78 70 77 eqtr3d ⊢ ( 𝜑 → ( ( ( int ‘ 𝑇 ) ‘ ( ( 𝐴 ∩ 𝐵 ) ∪ ( ∪ 𝑇 ∖ 𝐴 ) ) ) ∩ 𝐴 ) = ( ( int ‘ ( 𝐾 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
79 65 78 sseqtrd ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ ( 𝐾 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
80 79 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
81 undif1 ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝐴 ∪ { 𝑥 } )
82 33 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
83 82 snssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → { 𝑥 } ⊆ ( 𝐴 ∩ 𝐵 ) )
84 83 22 sstrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → { 𝑥 } ⊆ 𝐴 )
85 ssequn2 ⊢ ( { 𝑥 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 𝑥 } ) = 𝐴 )
86 84 85 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐴 ∪ { 𝑥 } ) = 𝐴 )
87 81 86 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = 𝐴 )
88 87 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( 𝐾 ↾t 𝐴 ) )
89 88 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( int ‘ ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) ) = ( int ‘ ( 𝐾 ↾t 𝐴 ) ) )
90 undif1 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( ( 𝐴 ∩ 𝐵 ) ∪ { 𝑥 } )
91 ssequn2 ⊢ ( { 𝑥 } ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∪ { 𝑥 } ) = ( 𝐴 ∩ 𝐵 ) )
92 83 91 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐴 ∩ 𝐵 ) ∪ { 𝑥 } ) = ( 𝐴 ∩ 𝐵 ) )
93 90 92 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝐴 ∩ 𝐵 ) )
94 89 93 fveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( int ‘ ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) ) ‘ ( ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) = ( ( int ‘ ( 𝐾 ↾t 𝐴 ) ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
95 80 94 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → 𝑥 ∈ ( ( int ‘ ( 𝐾 ↾t ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) ) ‘ ( ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ∪ { 𝑥 } ) ) )
96 54 55 57 1 58 95 limcres ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ) limℂ 𝑥 ) = ( 𝐺 limℂ 𝑥 ) )
97 47 96 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) = ( 𝐺 limℂ 𝑥 ) )
98 97 eleq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝑦 ∈ ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ↔ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) )
99 98 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ) )
100 7 29 sseqtrd ⊢ ( 𝜑 → 𝐵 ⊆ ∪ 𝑇 )
101 31 ntrin ⊢ ( ( 𝑇 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑇 ∧ 𝐵 ⊆ ∪ 𝑇 ) → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) )
102 21 66 100 101 syl3anc ⊢ ( 𝜑 → ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) )
103 102 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ↔ 𝑥 ∈ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
104 elin ⊢ ( 𝑥 ∈ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) )
105 103 104 bitrdi ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
106 105 anbi1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ↔ ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ) )
107 99 106 bitrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ↔ ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ) )
108 an32 ⊢ ( ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ↔ ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) )
109 107 108 bitrdi ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ↔ ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
110 eqid ⊢ ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
111 fresin ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
112 5 111 syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : ( 𝐴 ∩ 𝐵 ) ⟶ ℂ )
113 2 1 110 4 112 23 eldv ⊢ ( 𝜑 → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( ( 𝐴 ∩ 𝐵 ) ∖ { 𝑥 } ) ↦ ( ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑧 ) − ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ) )
114 2 1 3 4 5 6 eldv ⊢ ( 𝜑 → ( 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ) )
115 114 anbi1cd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ↔ ( ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( 𝐺 limℂ 𝑥 ) ) ∧ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ) ) )
116 109 113 115 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ( 𝑆 D ( 𝐹 ↾ 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐵 ) ∧ 𝑥 ( 𝑆 D 𝐹 ) 𝑦 ) ) )