Step | Hyp | Ref
| Expression |
1 | | df-rab 3434 |
. 2
β’ {π‘ β (β
βm β) β£ βπ₯ β β βπ¦ β β+ βπ§ β β+
βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦)} = {π‘ β£ (π‘ β (β βm β)
β§ βπ₯ β
β βπ¦ β
β+ βπ§ β β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))} |
2 | | df-cnfn 31100 |
. 2
β’ ContFn =
{π‘ β (β
βm β) β£ βπ₯ β β βπ¦ β β+ βπ§ β β+
βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦)} |
3 | | hhcn.1 |
. . . . . . . . . . . . . 14
β’ π· = (normβ
β ββ ) |
4 | 3 | hilmetdval 30449 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π€ β β) β (π₯π·π€) = (normββ(π₯ ββ
π€))) |
5 | | normsub 30396 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π€ β β) β
(normββ(π₯ ββ π€)) =
(normββ(π€ ββ π₯))) |
6 | 4, 5 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π€ β β) β (π₯π·π€) = (normββ(π€ ββ
π₯))) |
7 | 6 | adantll 713 |
. . . . . . . . . . 11
β’ (((π‘: ββΆβ β§
π₯ β β) β§
π€ β β) β
(π₯π·π€) = (normββ(π€ ββ
π₯))) |
8 | 7 | breq1d 5159 |
. . . . . . . . . 10
β’ (((π‘: ββΆβ β§
π₯ β β) β§
π€ β β) β
((π₯π·π€) < π§ β (normββ(π€ ββ
π₯)) < π§)) |
9 | | ffvelcdm 7084 |
. . . . . . . . . . . . . 14
β’ ((π‘: ββΆβ β§
π₯ β β) β
(π‘βπ₯) β β) |
10 | | ffvelcdm 7084 |
. . . . . . . . . . . . . 14
β’ ((π‘: ββΆβ β§
π€ β β) β
(π‘βπ€) β β) |
11 | 9, 10 | anim12dan 620 |
. . . . . . . . . . . . 13
β’ ((π‘: ββΆβ β§
(π₯ β β β§
π€ β β)) β
((π‘βπ₯) β β β§ (π‘βπ€) β β)) |
12 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (abs
β β ) = (abs β β ) |
13 | 12 | cnmetdval 24287 |
. . . . . . . . . . . . . 14
β’ (((π‘βπ₯) β β β§ (π‘βπ€) β β) β ((π‘βπ₯)(abs β β )(π‘βπ€)) = (absβ((π‘βπ₯) β (π‘βπ€)))) |
14 | | abssub 15273 |
. . . . . . . . . . . . . 14
β’ (((π‘βπ₯) β β β§ (π‘βπ€) β β) β (absβ((π‘βπ₯) β (π‘βπ€))) = (absβ((π‘βπ€) β (π‘βπ₯)))) |
15 | 13, 14 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π‘βπ₯) β β β§ (π‘βπ€) β β) β ((π‘βπ₯)(abs β β )(π‘βπ€)) = (absβ((π‘βπ€) β (π‘βπ₯)))) |
16 | 11, 15 | syl 17 |
. . . . . . . . . . . 12
β’ ((π‘: ββΆβ β§
(π₯ β β β§
π€ β β)) β
((π‘βπ₯)(abs β β )(π‘βπ€)) = (absβ((π‘βπ€) β (π‘βπ₯)))) |
17 | 16 | anassrs 469 |
. . . . . . . . . . 11
β’ (((π‘: ββΆβ β§
π₯ β β) β§
π€ β β) β
((π‘βπ₯)(abs β β )(π‘βπ€)) = (absβ((π‘βπ€) β (π‘βπ₯)))) |
18 | 17 | breq1d 5159 |
. . . . . . . . . 10
β’ (((π‘: ββΆβ β§
π₯ β β) β§
π€ β β) β
(((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦)) |
19 | 8, 18 | imbi12d 345 |
. . . . . . . . 9
β’ (((π‘: ββΆβ β§
π₯ β β) β§
π€ β β) β
(((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦) β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
20 | 19 | ralbidva 3176 |
. . . . . . . 8
β’ ((π‘: ββΆβ β§
π₯ β β) β
(βπ€ β β
((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦) β βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
21 | 20 | rexbidv 3179 |
. . . . . . 7
β’ ((π‘: ββΆβ β§
π₯ β β) β
(βπ§ β
β+ βπ€ β β ((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦) β βπ§ β β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
22 | 21 | ralbidv 3178 |
. . . . . 6
β’ ((π‘: ββΆβ β§
π₯ β β) β
(βπ¦ β
β+ βπ§ β β+ βπ€ β β ((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦) β βπ¦ β β+ βπ§ β β+
βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
23 | 22 | ralbidva 3176 |
. . . . 5
β’ (π‘: ββΆβ β
(βπ₯ β β
βπ¦ β
β+ βπ§ β β+ βπ€ β β ((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦) β βπ₯ β β βπ¦ β β+ βπ§ β β+
βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
24 | 23 | pm5.32i 576 |
. . . 4
β’ ((π‘: ββΆβ β§
βπ₯ β β
βπ¦ β
β+ βπ§ β β+ βπ€ β β ((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦)) β (π‘: ββΆβ β§ βπ₯ β β βπ¦ β β+
βπ§ β
β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
25 | 3 | hilxmet 30448 |
. . . . 5
β’ π· β (βMetβ
β) |
26 | | cnxmet 24289 |
. . . . 5
β’ (abs
β β ) β (βMetββ) |
27 | | hhcn.2 |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
28 | | hhcn.4 |
. . . . . . 7
β’ πΎ =
(TopOpenββfld) |
29 | 28 | cnfldtopn 24298 |
. . . . . 6
β’ πΎ = (MetOpenβ(abs β
β )) |
30 | 27, 29 | metcn 24052 |
. . . . 5
β’ ((π· β (βMetβ
β) β§ (abs β β ) β (βMetββ)) β
(π‘ β (π½ Cn πΎ) β (π‘: ββΆβ β§ βπ₯ β β βπ¦ β β+
βπ§ β
β+ βπ€ β β ((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦)))) |
31 | 25, 26, 30 | mp2an 691 |
. . . 4
β’ (π‘ β (π½ Cn πΎ) β (π‘: ββΆβ β§ βπ₯ β β βπ¦ β β+
βπ§ β
β+ βπ€ β β ((π₯π·π€) < π§ β ((π‘βπ₯)(abs β β )(π‘βπ€)) < π¦))) |
32 | | cnex 11191 |
. . . . . 6
β’ β
β V |
33 | | ax-hilex 30252 |
. . . . . 6
β’ β
β V |
34 | 32, 33 | elmap 8865 |
. . . . 5
β’ (π‘ β (β
βm β) β π‘: ββΆβ) |
35 | 34 | anbi1i 625 |
. . . 4
β’ ((π‘ β (β
βm β) β§ βπ₯ β β βπ¦ β β+ βπ§ β β+
βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦)) β (π‘: ββΆβ β§ βπ₯ β β βπ¦ β β+
βπ§ β
β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
36 | 24, 31, 35 | 3bitr4i 303 |
. . 3
β’ (π‘ β (π½ Cn πΎ) β (π‘ β (β βm β)
β§ βπ₯ β
β βπ¦ β
β+ βπ§ β β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))) |
37 | 36 | eqabi 2870 |
. 2
β’ (π½ Cn πΎ) = {π‘ β£ (π‘ β (β βm β)
β§ βπ₯ β
β βπ¦ β
β+ βπ§ β β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((π‘βπ€) β (π‘βπ₯))) < π¦))} |
38 | 1, 2, 37 | 3eqtr4i 2771 |
1
β’ ContFn =
(π½ Cn πΎ) |