| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvfcn 25944 | . . . . . . 7
⊢ (ℂ
D exp):dom (ℂ D exp)⟶ℂ | 
| 2 |  | dvbsss 25938 | . . . . . . . . 9
⊢ dom
(ℂ D exp) ⊆ ℂ | 
| 3 |  | subcl 11508 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) | 
| 4 | 3 | ancoms 458 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 − 𝑥) ∈ ℂ) | 
| 5 |  | efadd 16131 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ (𝑧 − 𝑥) ∈ ℂ) → (exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) | 
| 6 | 4, 5 | syldan 591 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = ((exp‘𝑥) · (exp‘(𝑧 − 𝑥)))) | 
| 7 |  | pncan3 11517 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 + (𝑧 − 𝑥)) = 𝑧) | 
| 8 | 7 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑥 + (𝑧 − 𝑥))) = (exp‘𝑧)) | 
| 9 | 6, 8 | eqtr3d 2778 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥))) = (exp‘𝑧)) | 
| 10 | 9 | mpteq2dva 5241 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
((exp‘𝑥) ·
(exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ (exp‘𝑧))) | 
| 11 |  | cnex 11237 | . . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V | 
| 12 | 11 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ℂ
∈ V) | 
| 13 |  | fvexd 6920 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘𝑥) ∈
V) | 
| 14 |  | fvexd 6920 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈ V) | 
| 15 |  | fconstmpt 5746 | . . . . . . . . . . . . . . . 16
⊢ (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥)) | 
| 16 | 15 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}) =
(𝑧 ∈ ℂ ↦
(exp‘𝑥))) | 
| 17 |  | eqidd 2737 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) | 
| 18 | 12, 13, 14, 16, 17 | offval2 7718 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = (𝑧 ∈ ℂ ↦ ((exp‘𝑥) · (exp‘(𝑧 − 𝑥))))) | 
| 19 |  | eff 16118 | . . . . . . . . . . . . . . . 16
⊢
exp:ℂ⟶ℂ | 
| 20 | 19 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
exp:ℂ⟶ℂ) | 
| 21 | 20 | feqmptd 6976 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → exp =
(𝑧 ∈ ℂ ↦
(exp‘𝑧))) | 
| 22 | 10, 18, 21 | 3eqtr4d 2786 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) = exp) | 
| 23 | 22 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → (ℂ
D ((ℂ × {(exp‘𝑥)}) ∘f · (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) = (ℂ D
exp)) | 
| 24 |  | efcl 16119 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
(exp‘𝑥) ∈
ℂ) | 
| 25 |  | fconstg 6794 | . . . . . . . . . . . . . . . 16
⊢
((exp‘𝑥)
∈ ℂ → (ℂ × {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) | 
| 26 | 24, 25 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶{(exp‘𝑥)}) | 
| 27 | 24 | snssd 4808 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
{(exp‘𝑥)} ⊆
ℂ) | 
| 28 | 26, 27 | fssd 6752 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (ℂ
× {(exp‘𝑥)}):ℂ⟶ℂ) | 
| 29 |  | ssidd 4006 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ℂ
⊆ ℂ) | 
| 30 |  | efcl 16119 | . . . . . . . . . . . . . . . 16
⊢ ((𝑧 − 𝑥) ∈ ℂ → (exp‘(𝑧 − 𝑥)) ∈ ℂ) | 
| 31 | 4, 30 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑧 − 𝑥)) ∈
ℂ) | 
| 32 | 31 | fmpttd 7134 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))):ℂ⟶ℂ) | 
| 33 |  | c0ex 11256 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V | 
| 34 | 33 | snid 4661 | . . . . . . . . . . . . . . . . 17
⊢ 0 ∈
{0} | 
| 35 |  | opelxpi 5721 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
{0}) → 〈𝑥,
0〉 ∈ (ℂ × {0})) | 
| 36 | 34, 35 | mpan2 691 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ × {0})) | 
| 37 |  | dvconst 25953 | . . . . . . . . . . . . . . . . 17
⊢
((exp‘𝑥)
∈ ℂ → (ℂ D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) | 
| 38 | 24, 37 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (ℂ
D (ℂ × {(exp‘𝑥)})) = (ℂ ×
{0})) | 
| 39 | 36, 38 | eleqtrrd 2843 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ →
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) | 
| 40 |  | df-br 5143 | . . . . . . . . . . . . . . 15
⊢ (𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0 ↔
〈𝑥, 0〉 ∈
(ℂ D (ℂ × {(exp‘𝑥)}))) | 
| 41 | 39, 40 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (ℂ ×
{(exp‘𝑥)}))0) | 
| 42 | 20, 4 | cofmpt 7151 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (exp
∘ (𝑧 ∈ ℂ
↦ (𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))) | 
| 43 | 42 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (ℂ
D (exp ∘ (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) = (ℂ D (𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥))))) | 
| 44 | 4 | fmpttd 7134 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)):ℂ⟶ℂ) | 
| 45 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 − 𝑥) = (𝑥 − 𝑥)) | 
| 46 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) = (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)) | 
| 47 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 − 𝑥) ∈ V | 
| 48 | 45, 46, 47 | fvmpt 7015 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = (𝑥 − 𝑥)) | 
| 49 |  | subid 11529 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (𝑥 − 𝑥) = 0) | 
| 50 | 48, 49 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥) = 0) | 
| 51 |  | dveflem 26018 | . . . . . . . . . . . . . . . . . 18
⊢ 0(ℂ
D exp)1 | 
| 52 | 50, 51 | eqbrtrdi 5181 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))‘𝑥)(ℂ D exp)1) | 
| 53 |  | 1ex 11258 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
V | 
| 54 | 53 | snid 4661 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
{1} | 
| 55 |  | opelxpi 5721 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
{1}) → 〈𝑥,
1〉 ∈ (ℂ × {1})) | 
| 56 | 54, 55 | mpan2 691 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ × {1})) | 
| 57 |  | cnelprrecn 11249 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ℂ
∈ {ℝ, ℂ} | 
| 58 | 57 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → ℂ
∈ {ℝ, ℂ}) | 
| 59 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑧 ∈
ℂ) | 
| 60 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) | 
| 61 | 58 | dvmptid 25996 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑧)) = (𝑧 ∈ ℂ ↦ 1)) | 
| 62 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 𝑥 ∈
ℂ) | 
| 63 |  | 0cnd 11255 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → 0 ∈
ℂ) | 
| 64 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) | 
| 65 | 58, 64 | dvmptc 25997 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
𝑥)) = (𝑧 ∈ ℂ ↦ 0)) | 
| 66 | 58, 59, 60, 61, 62, 63, 65 | dvmptsub 26006 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (𝑧 ∈ ℂ ↦ (1 −
0))) | 
| 67 |  | 1m0e1 12388 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 0) = 1 | 
| 68 | 67 | mpteq2i 5246 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (𝑧 ∈
ℂ ↦ 1) | 
| 69 |  | fconstmpt 5746 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) | 
| 70 | 68, 69 | eqtr4i 2767 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℂ ↦ (1
− 0)) = (ℂ × {1}) | 
| 71 | 66, 70 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℂ → (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧 − 𝑥))) = (ℂ ×
{1})) | 
| 72 | 56, 71 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
〈𝑥, 1〉 ∈
(ℂ D (𝑧 ∈
ℂ ↦ (𝑧 −
𝑥)))) | 
| 73 |  | df-br 5143 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1 ↔ 〈𝑥, 1〉 ∈ (ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))) | 
| 74 | 72, 73 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥)))1) | 
| 75 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 76 | 20, 29, 44, 29, 29, 29, 52, 74, 75 | dvcobr 25984 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))(1 · 1)) | 
| 77 |  | 1t1e1 12429 | . . . . . . . . . . . . . . . 16
⊢ (1
· 1) = 1 | 
| 78 | 76, 77 | breqtrdi 5183 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (exp ∘ (𝑧 ∈ ℂ ↦ (𝑧 − 𝑥))))1) | 
| 79 | 43, 78 | breqdi 5157 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥))))1) | 
| 80 | 28, 29, 32, 29, 29, 41, 79, 75 | dvmulbr 25976 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))((0 · ((𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))‘𝑥)) + (1 · ((ℂ ×
{(exp‘𝑥)})‘𝑥)))) | 
| 81 | 32, 64 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → ((𝑧 ∈ ℂ ↦
(exp‘(𝑧 − 𝑥)))‘𝑥) ∈ ℂ) | 
| 82 | 81 | mul02d 11460 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) = 0) | 
| 83 |  | fvex 6918 | . . . . . . . . . . . . . . . . . 18
⊢
(exp‘𝑥) ∈
V | 
| 84 | 83 | fvconst2 7225 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → ((ℂ
× {(exp‘𝑥)})‘𝑥) = (exp‘𝑥)) | 
| 85 | 84 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (1 · (exp‘𝑥))) | 
| 86 | 24 | mullidd 11280 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (1
· (exp‘𝑥)) =
(exp‘𝑥)) | 
| 87 | 85, 86 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → (1
· ((ℂ × {(exp‘𝑥)})‘𝑥)) = (exp‘𝑥)) | 
| 88 | 82, 87 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (0 + (exp‘𝑥))) | 
| 89 | 24 | addlidd 11463 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ → (0 +
(exp‘𝑥)) =
(exp‘𝑥)) | 
| 90 | 88, 89 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → ((0
· ((𝑧 ∈ ℂ
↦ (exp‘(𝑧
− 𝑥)))‘𝑥)) + (1 · ((ℂ
× {(exp‘𝑥)})‘𝑥))) = (exp‘𝑥)) | 
| 91 | 80, 90 | breqtrd 5168 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D ((ℂ ×
{(exp‘𝑥)})
∘f · (𝑧 ∈ ℂ ↦ (exp‘(𝑧 − 𝑥)))))(exp‘𝑥)) | 
| 92 | 23, 91 | breqdi 5157 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℂ → 𝑥(ℂ D exp)(exp‘𝑥)) | 
| 93 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑥 ∈ V | 
| 94 | 93, 83 | breldm 5918 | . . . . . . . . . . 11
⊢ (𝑥(ℂ D exp)(exp‘𝑥) → 𝑥 ∈ dom (ℂ D exp)) | 
| 95 | 92, 94 | syl 17 | . . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → 𝑥 ∈ dom (ℂ D
exp)) | 
| 96 | 95 | ssriv 3986 | . . . . . . . . 9
⊢ ℂ
⊆ dom (ℂ D exp) | 
| 97 | 2, 96 | eqssi 3999 | . . . . . . . 8
⊢ dom
(ℂ D exp) = ℂ | 
| 98 | 97 | feq2i 6727 | . . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ ↔ (ℂ D
exp):ℂ⟶ℂ) | 
| 99 | 1, 98 | mpbi 230 | . . . . . 6
⊢ (ℂ
D exp):ℂ⟶ℂ | 
| 100 | 99 | a1i 11 | . . . . 5
⊢ (⊤
→ (ℂ D exp):ℂ⟶ℂ) | 
| 101 | 100 | feqmptd 6976 | . . . 4
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ ((ℂ D exp)‘𝑥))) | 
| 102 |  | ffun 6738 | . . . . . . 7
⊢ ((ℂ
D exp):dom (ℂ D exp)⟶ℂ → Fun (ℂ D
exp)) | 
| 103 | 1, 102 | ax-mp 5 | . . . . . 6
⊢ Fun
(ℂ D exp) | 
| 104 |  | funbrfv 6956 | . . . . . 6
⊢ (Fun
(ℂ D exp) → (𝑥(ℂ D exp)(exp‘𝑥) → ((ℂ D exp)‘𝑥) = (exp‘𝑥))) | 
| 105 | 103, 92, 104 | mpsyl 68 | . . . . 5
⊢ (𝑥 ∈ ℂ → ((ℂ
D exp)‘𝑥) =
(exp‘𝑥)) | 
| 106 | 105 | mpteq2ia 5244 | . . . 4
⊢ (𝑥 ∈ ℂ ↦
((ℂ D exp)‘𝑥))
= (𝑥 ∈ ℂ ↦
(exp‘𝑥)) | 
| 107 | 101, 106 | eqtrdi 2792 | . . 3
⊢ (⊤
→ (ℂ D exp) = (𝑥
∈ ℂ ↦ (exp‘𝑥))) | 
| 108 | 19 | a1i 11 | . . . 4
⊢ (⊤
→ exp:ℂ⟶ℂ) | 
| 109 | 108 | feqmptd 6976 | . . 3
⊢ (⊤
→ exp = (𝑥 ∈
ℂ ↦ (exp‘𝑥))) | 
| 110 | 107, 109 | eqtr4d 2779 | . 2
⊢ (⊤
→ (ℂ D exp) = exp) | 
| 111 | 110 | mptru 1546 | 1
⊢ (ℂ
D exp) = exp |