Step | Hyp | Ref
| Expression |
1 | | cana 25729 |
. 2
class
Ana |
2 | | vs |
. . 3
setvar π |
3 | | cr 11057 |
. . . 4
class
β |
4 | | cc 11056 |
. . . 4
class
β |
5 | 3, 4 | cpr 4593 |
. . 3
class {β,
β} |
6 | | vx |
. . . . . . 7
setvar π₯ |
7 | 6 | cv 1541 |
. . . . . 6
class π₯ |
8 | | vf |
. . . . . . . . . 10
setvar π |
9 | 8 | cv 1541 |
. . . . . . . . 9
class π |
10 | | cpnf 11193 |
. . . . . . . . . 10
class
+β |
11 | 2 | cv 1541 |
. . . . . . . . . . 11
class π |
12 | | ctayl 25728 |
. . . . . . . . . . 11
class
Tayl |
13 | 11, 9, 12 | co 7362 |
. . . . . . . . . 10
class (π Tayl π) |
14 | 10, 7, 13 | co 7362 |
. . . . . . . . 9
class
(+β(π Tayl
π)π₯) |
15 | 9, 14 | cin 3914 |
. . . . . . . 8
class (π β© (+β(π Tayl π)π₯)) |
16 | 15 | cdm 5638 |
. . . . . . 7
class dom
(π β© (+β(π Tayl π)π₯)) |
17 | | ccnfld 20812 |
. . . . . . . . . 10
class
βfld |
18 | | ctopn 17310 |
. . . . . . . . . 10
class
TopOpen |
19 | 17, 18 | cfv 6501 |
. . . . . . . . 9
class
(TopOpenββfld) |
20 | | crest 17309 |
. . . . . . . . 9
class
βΎt |
21 | 19, 11, 20 | co 7362 |
. . . . . . . 8
class
((TopOpenββfld) βΎt π ) |
22 | | cnt 22384 |
. . . . . . . 8
class
int |
23 | 21, 22 | cfv 6501 |
. . . . . . 7
class
(intβ((TopOpenββfld) βΎt
π )) |
24 | 16, 23 | cfv 6501 |
. . . . . 6
class
((intβ((TopOpenββfld) βΎt
π ))βdom (π β© (+β(π Tayl π)π₯))) |
25 | 7, 24 | wcel 2107 |
. . . . 5
wff π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom (π β© (+β(π Tayl π)π₯))) |
26 | 9 | cdm 5638 |
. . . . 5
class dom π |
27 | 25, 6, 26 | wral 3065 |
. . . 4
wff
βπ₯ β dom
π π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom (π β© (+β(π Tayl π)π₯))) |
28 | | cpm 8773 |
. . . . 5
class
βpm |
29 | 4, 11, 28 | co 7362 |
. . . 4
class (β
βpm π ) |
30 | 27, 8, 29 | crab 3410 |
. . 3
class {π β (β
βpm π )
β£ βπ₯ β
dom π π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom (π β© (+β(π Tayl π)π₯)))} |
31 | 2, 5, 30 | cmpt 5193 |
. 2
class (π β {β, β}
β¦ {π β (β
βpm π )
β£ βπ₯ β
dom π π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom (π β© (+β(π Tayl π)π₯)))}) |
32 | 1, 31 | wceq 1542 |
1
wff Ana =
(π β {β,
β} β¦ {π β
(β βpm π ) β£ βπ₯ β dom π π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom (π β© (+β(π Tayl π)π₯)))}) |