Step | Hyp | Ref
| Expression |
1 | | dvfcn 25425 |
. . . 4
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
2 | | ssidd 4006 |
. . . . . . 7
β’ (π β β β
β) |
3 | | dvidlem.1 |
. . . . . . 7
β’ (π β πΉ:ββΆβ) |
4 | 2, 3, 2 | dvbss 25418 |
. . . . . 6
β’ (π β dom (β D πΉ) β
β) |
5 | | reldv 25387 |
. . . . . . 7
β’ Rel
(β D πΉ) |
6 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β π₯ β β) |
7 | | eqid 2733 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
8 | 7 | cnfldtop 24300 |
. . . . . . . . . 10
β’
(TopOpenββfld) β Top |
9 | | unicntop 24302 |
. . . . . . . . . . 11
β’ β =
βͺ
(TopOpenββfld) |
10 | 9 | ntrtop 22574 |
. . . . . . . . . 10
β’
((TopOpenββfld) β Top β
((intβ(TopOpenββfld))ββ) =
β) |
11 | 8, 10 | ax-mp 5 |
. . . . . . . . 9
β’
((intβ(TopOpenββfld))ββ) =
β |
12 | 6, 11 | eleqtrrdi 2845 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β π₯ β
((intβ(TopOpenββfld))ββ)) |
13 | | limcresi 25402 |
. . . . . . . . . 10
β’ ((π§ β β β¦ π΅) limβ π₯) β (((π§ β β β¦ π΅) βΎ (β β {π₯})) limβ π₯) |
14 | | dvidlem.3 |
. . . . . . . . . . . 12
β’ π΅ β β |
15 | | ssidd 4006 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β β β
β) |
16 | | cncfmptc 24428 |
. . . . . . . . . . . 12
β’ ((π΅ β β β§ β
β β β§ β β β) β (π§ β β β¦ π΅) β (ββcnββ)) |
17 | 14, 15, 15, 16 | mp3an2i 1467 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (π§ β β β¦ π΅) β (ββcnββ)) |
18 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π§ = π₯ β π΅ = π΅) |
19 | 17, 6, 18 | cnmptlimc 25407 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β π΅ β ((π§ β β β¦ π΅) limβ π₯)) |
20 | 13, 19 | sselid 3981 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β π΅ β (((π§ β β β¦ π΅) βΎ (β β {π₯})) limβ π₯)) |
21 | | eldifsn 4791 |
. . . . . . . . . . . . 13
β’ (π§ β (β β {π₯}) β (π§ β β β§ π§ β π₯)) |
22 | | dvidlem.2 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β β§ π§ β β β§ π§ β π₯)) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅) |
23 | 22 | 3exp2 1355 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β β β (π§ β β β (π§ β π₯ β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅)))) |
24 | 23 | imp43 429 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β) β§ (π§ β β β§ π§ β π₯)) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅) |
25 | 21, 24 | sylan2b 595 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π§ β (β β {π₯})) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅) |
26 | 25 | mpteq2dva 5249 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (π§ β (β β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β (β β {π₯}) β¦ π΅)) |
27 | | difss 4132 |
. . . . . . . . . . . 12
β’ (β
β {π₯}) β
β |
28 | | resmpt 6038 |
. . . . . . . . . . . 12
β’ ((β
β {π₯}) β
β β ((π§ β
β β¦ π΅) βΎ
(β β {π₯})) =
(π§ β (β β
{π₯}) β¦ π΅)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π§ β β β¦ π΅) βΎ (β β
{π₯})) = (π§ β (β β {π₯}) β¦ π΅) |
30 | 26, 29 | eqtr4di 2791 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (π§ β (β β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = ((π§ β β β¦ π΅) βΎ (β β {π₯}))) |
31 | 30 | oveq1d 7424 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((π§ β (β β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯) = (((π§ β β β¦ π΅) βΎ (β β {π₯})) limβ π₯)) |
32 | 20, 31 | eleqtrrd 2837 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β π΅ β ((π§ β (β β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
33 | 7 | cnfldtopon 24299 |
. . . . . . . . . 10
β’
(TopOpenββfld) β
(TopOnββ) |
34 | 33 | toponrestid 22423 |
. . . . . . . . 9
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
35 | | eqid 2733 |
. . . . . . . . 9
β’ (π§ β (β β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β (β β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
36 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β πΉ:ββΆβ) |
37 | 34, 7, 35, 15, 36, 15 | eldv 25415 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (π₯(β D πΉ)π΅ β (π₯ β
((intβ(TopOpenββfld))ββ) β§ π΅ β ((π§ β (β β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)))) |
38 | 12, 32, 37 | mpbir2and 712 |
. . . . . . 7
β’ ((π β§ π₯ β β) β π₯(β D πΉ)π΅) |
39 | | releldm 5944 |
. . . . . . 7
β’ ((Rel
(β D πΉ) β§ π₯(β D πΉ)π΅) β π₯ β dom (β D πΉ)) |
40 | 5, 38, 39 | sylancr 588 |
. . . . . 6
β’ ((π β§ π₯ β β) β π₯ β dom (β D πΉ)) |
41 | 4, 40 | eqelssd 4004 |
. . . . 5
β’ (π β dom (β D πΉ) = β) |
42 | 41 | feq2d 6704 |
. . . 4
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):ββΆβ)) |
43 | 1, 42 | mpbii 232 |
. . 3
β’ (π β (β D πΉ):ββΆβ) |
44 | 43 | ffnd 6719 |
. 2
β’ (π β (β D πΉ) Fn β) |
45 | | fnconstg 6780 |
. . 3
β’ (π΅ β β β (β
Γ {π΅}) Fn
β) |
46 | 14, 45 | mp1i 13 |
. 2
β’ (π β (β Γ {π΅}) Fn β) |
47 | | ffun 6721 |
. . . . . 6
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β Fun
(β D πΉ)) |
48 | 1, 47 | mp1i 13 |
. . . . 5
β’ ((π β§ π₯ β β) β Fun (β D πΉ)) |
49 | | funbrfvb 6947 |
. . . . 5
β’ ((Fun
(β D πΉ) β§ π₯ β dom (β D πΉ)) β (((β D πΉ)βπ₯) = π΅ β π₯(β D πΉ)π΅)) |
50 | 48, 40, 49 | syl2anc 585 |
. . . 4
β’ ((π β§ π₯ β β) β (((β D πΉ)βπ₯) = π΅ β π₯(β D πΉ)π΅)) |
51 | 38, 50 | mpbird 257 |
. . 3
β’ ((π β§ π₯ β β) β ((β D πΉ)βπ₯) = π΅) |
52 | 14 | a1i 11 |
. . . 4
β’ (π β π΅ β β) |
53 | | fvconst2g 7203 |
. . . 4
β’ ((π΅ β β β§ π₯ β β) β
((β Γ {π΅})βπ₯) = π΅) |
54 | 52, 53 | sylan 581 |
. . 3
β’ ((π β§ π₯ β β) β ((β Γ
{π΅})βπ₯) = π΅) |
55 | 51, 54 | eqtr4d 2776 |
. 2
β’ ((π β§ π₯ β β) β ((β D πΉ)βπ₯) = ((β Γ {π΅})βπ₯)) |
56 | 44, 46, 55 | eqfnfvd 7036 |
1
β’ (π β (β D πΉ) = (β Γ {π΅})) |