Step | Hyp | Ref
| Expression |
1 | | dvidlem.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
2 | | cnex 7934 |
. . . . . . 7
β’ β
β V |
3 | 2, 2 | fpm 6680 |
. . . . . 6
β’ (πΉ:ββΆβ β
πΉ β (β
βpm β)) |
4 | 1, 3 | syl 14 |
. . . . 5
β’ (π β πΉ β (β βpm
β)) |
5 | | dvfcnpm 14095 |
. . . . 5
β’ (πΉ β (β
βpm β) β (β D πΉ):dom (β D πΉ)βΆβ) |
6 | 4, 5 | syl 14 |
. . . 4
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
7 | | ssidd 3176 |
. . . . . . 7
β’ (π β β β
β) |
8 | 7, 1, 7 | dvbss 14090 |
. . . . . 6
β’ (π β dom (β D πΉ) β
β) |
9 | | reldvg 14084 |
. . . . . . . . 9
β’ ((β
β β β§ πΉ
β (β βpm β)) β Rel (β D
πΉ)) |
10 | 7, 4, 9 | syl2anc 411 |
. . . . . . . 8
β’ (π β Rel (β D πΉ)) |
11 | 10 | adantr 276 |
. . . . . . 7
β’ ((π β§ π₯ β β) β Rel (β D πΉ)) |
12 | | simpr 110 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β π₯ β β) |
13 | | eqid 2177 |
. . . . . . . . . . 11
β’
(MetOpenβ(abs β β )) = (MetOpenβ(abs β
β )) |
14 | 13 | cntoptop 13969 |
. . . . . . . . . 10
β’
(MetOpenβ(abs β β )) β Top |
15 | 13 | cntoptopon 13968 |
. . . . . . . . . . . 12
β’
(MetOpenβ(abs β β )) β
(TopOnββ) |
16 | 15 | toponunii 13453 |
. . . . . . . . . . 11
β’ β =
βͺ (MetOpenβ(abs β β
)) |
17 | 16 | ntrtop 13564 |
. . . . . . . . . 10
β’
((MetOpenβ(abs β β )) β Top β
((intβ(MetOpenβ(abs β β )))ββ) =
β) |
18 | 14, 17 | ax-mp 5 |
. . . . . . . . 9
β’
((intβ(MetOpenβ(abs β β )))ββ) =
β |
19 | 12, 18 | eleqtrrdi 2271 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β π₯ β ((intβ(MetOpenβ(abs
β β )))ββ)) |
20 | | limcresi 14071 |
. . . . . . . . . 10
β’ ((π§ β β β¦ π΅) limβ π₯) β (((π§ β β β¦ π΅) βΎ {π€ β β β£ π€ # π₯}) limβ π₯) |
21 | | dvidlem.3 |
. . . . . . . . . . . 12
β’ π΅ β β |
22 | | ssidd 3176 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β β β
β) |
23 | | cncfmptc 14018 |
. . . . . . . . . . . 12
β’ ((π΅ β β β§ β
β β β§ β β β) β (π§ β β β¦ π΅) β (ββcnββ)) |
24 | 21, 22, 22, 23 | mp3an2i 1342 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (π§ β β β¦ π΅) β (ββcnββ)) |
25 | | eqidd 2178 |
. . . . . . . . . . 11
β’ (π§ = π₯ β π΅ = π΅) |
26 | 24, 12, 25 | cnmptlimc 14079 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β π΅ β ((π§ β β β¦ π΅) limβ π₯)) |
27 | 20, 26 | sselid 3153 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β π΅ β (((π§ β β β¦ π΅) βΎ {π€ β β β£ π€ # π₯}) limβ π₯)) |
28 | | breq1 4006 |
. . . . . . . . . . . . . 14
β’ (π€ = π§ β (π€ # π₯ β π§ # π₯)) |
29 | 28 | elrab 2893 |
. . . . . . . . . . . . 13
β’ (π§ β {π€ β β β£ π€ # π₯} β (π§ β β β§ π§ # π₯)) |
30 | | dvidlemap.2 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β β§ π§ β β β§ π§ # π₯)) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅) |
31 | 30 | 3exp2 1225 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β β β (π§ β β β (π§ # π₯ β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅)))) |
32 | 31 | imp43 355 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β) β§ (π§ β β β§ π§ # π₯)) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅) |
33 | 29, 32 | sylan2b 287 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π§ β {π€ β β β£ π€ # π₯}) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅) |
34 | 33 | mpteq2dva 4093 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (π§ β {π€ β β β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β {π€ β β β£ π€ # π₯} β¦ π΅)) |
35 | | ssrab2 3240 |
. . . . . . . . . . . 12
β’ {π€ β β β£ π€ # π₯} β β |
36 | | resmpt 4955 |
. . . . . . . . . . . 12
β’ ({π€ β β β£ π€ # π₯} β β β ((π§ β β β¦ π΅) βΎ {π€ β β β£ π€ # π₯}) = (π§ β {π€ β β β£ π€ # π₯} β¦ π΅)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π§ β β β¦ π΅) βΎ {π€ β β β£ π€ # π₯}) = (π§ β {π€ β β β£ π€ # π₯} β¦ π΅) |
38 | 34, 37 | eqtr4di 2228 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (π§ β {π€ β β β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = ((π§ β β β¦ π΅) βΎ {π€ β β β£ π€ # π₯})) |
39 | 38 | oveq1d 5889 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((π§ β {π€ β β β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯) = (((π§ β β β¦ π΅) βΎ {π€ β β β£ π€ # π₯}) limβ π₯)) |
40 | 27, 39 | eleqtrrd 2257 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β π΅ β ((π§ β {π€ β β β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
41 | 15 | toponrestid 13457 |
. . . . . . . . 9
β’
(MetOpenβ(abs β β )) = ((MetOpenβ(abs β
β )) βΎt β) |
42 | | eqid 2177 |
. . . . . . . . 9
β’ (π§ β {π€ β β β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β {π€ β β β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
43 | 1 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β πΉ:ββΆβ) |
44 | 41, 13, 42, 22, 43, 22 | eldvap 14087 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (π₯(β D πΉ)π΅ β (π₯ β ((intβ(MetOpenβ(abs
β β )))ββ) β§ π΅ β ((π§ β {π€ β β β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)))) |
45 | 19, 40, 44 | mpbir2and 944 |
. . . . . . 7
β’ ((π β§ π₯ β β) β π₯(β D πΉ)π΅) |
46 | | releldm 4862 |
. . . . . . 7
β’ ((Rel
(β D πΉ) β§ π₯(β D πΉ)π΅) β π₯ β dom (β D πΉ)) |
47 | 11, 45, 46 | syl2anc 411 |
. . . . . 6
β’ ((π β§ π₯ β β) β π₯ β dom (β D πΉ)) |
48 | 8, 47 | eqelssd 3174 |
. . . . 5
β’ (π β dom (β D πΉ) = β) |
49 | 48 | feq2d 5353 |
. . . 4
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):ββΆβ)) |
50 | 6, 49 | mpbid 147 |
. . 3
β’ (π β (β D πΉ):ββΆβ) |
51 | 50 | ffnd 5366 |
. 2
β’ (π β (β D πΉ) Fn β) |
52 | | fnconstg 5413 |
. . 3
β’ (π΅ β β β (β
Γ {π΅}) Fn
β) |
53 | 21, 52 | mp1i 10 |
. 2
β’ (π β (β Γ {π΅}) Fn β) |
54 | 6 | adantr 276 |
. . . . . 6
β’ ((π β§ π₯ β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
55 | 54 | ffund 5369 |
. . . . 5
β’ ((π β§ π₯ β β) β Fun (β D πΉ)) |
56 | | funbrfvb 5558 |
. . . . 5
β’ ((Fun
(β D πΉ) β§ π₯ β dom (β D πΉ)) β (((β D πΉ)βπ₯) = π΅ β π₯(β D πΉ)π΅)) |
57 | 55, 47, 56 | syl2anc 411 |
. . . 4
β’ ((π β§ π₯ β β) β (((β D πΉ)βπ₯) = π΅ β π₯(β D πΉ)π΅)) |
58 | 45, 57 | mpbird 167 |
. . 3
β’ ((π β§ π₯ β β) β ((β D πΉ)βπ₯) = π΅) |
59 | 21 | a1i 9 |
. . . 4
β’ (π β π΅ β β) |
60 | | fvconst2g 5730 |
. . . 4
β’ ((π΅ β β β§ π₯ β β) β
((β Γ {π΅})βπ₯) = π΅) |
61 | 59, 60 | sylan 283 |
. . 3
β’ ((π β§ π₯ β β) β ((β Γ
{π΅})βπ₯) = π΅) |
62 | 58, 61 | eqtr4d 2213 |
. 2
β’ ((π β§ π₯ β β) β ((β D πΉ)βπ₯) = ((β Γ {π΅})βπ₯)) |
63 | 51, 53, 62 | eqfnfvd 5616 |
1
β’ (π β (β D πΉ) = (β Γ {π΅})) |