Step |
Hyp |
Ref |
Expression |
0 |
|
cana |
⊢ Ana |
1 |
|
vs |
⊢ 𝑠 |
2 |
|
cr |
⊢ ℝ |
3 |
|
cc |
⊢ ℂ |
4 |
2 3
|
cpr |
⊢ { ℝ , ℂ } |
5 |
|
vf |
⊢ 𝑓 |
6 |
|
cpm |
⊢ ↑pm |
7 |
1
|
cv |
⊢ 𝑠 |
8 |
3 7 6
|
co |
⊢ ( ℂ ↑pm 𝑠 ) |
9 |
|
vx |
⊢ 𝑥 |
10 |
5
|
cv |
⊢ 𝑓 |
11 |
10
|
cdm |
⊢ dom 𝑓 |
12 |
9
|
cv |
⊢ 𝑥 |
13 |
|
cnt |
⊢ int |
14 |
|
ctopn |
⊢ TopOpen |
15 |
|
ccnfld |
⊢ ℂfld |
16 |
15 14
|
cfv |
⊢ ( TopOpen ‘ ℂfld ) |
17 |
|
crest |
⊢ ↾t |
18 |
16 7 17
|
co |
⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) |
19 |
18 13
|
cfv |
⊢ ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) |
20 |
|
cpnf |
⊢ +∞ |
21 |
|
ctayl |
⊢ Tayl |
22 |
7 10 21
|
co |
⊢ ( 𝑠 Tayl 𝑓 ) |
23 |
20 12 22
|
co |
⊢ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) |
24 |
10 23
|
cin |
⊢ ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) |
25 |
24
|
cdm |
⊢ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) |
26 |
25 19
|
cfv |
⊢ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) |
27 |
12 26
|
wcel |
⊢ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) |
28 |
27 9 11
|
wral |
⊢ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) |
29 |
28 5 8
|
crab |
⊢ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) } |
30 |
1 4 29
|
cmpt |
⊢ ( 𝑠 ∈ { ℝ , ℂ } ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) } ) |
31 |
0 30
|
wceq |
⊢ Ana = ( 𝑠 ∈ { ℝ , ℂ } ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) } ) |