Step | Hyp | Ref
| Expression |
1 | | ax-resscn 7903 |
. . . . 5
β’ β
β β |
2 | 1 | a1i 9 |
. . . 4
β’ (π β β β
β) |
3 | | dvcj.f |
. . . 4
β’ (π β πΉ:πβΆβ) |
4 | | dvcj.x |
. . . 4
β’ (π β π β β) |
5 | | eqid 2177 |
. . . . 5
β’
(MetOpenβ(abs β β )) = (MetOpenβ(abs β
β )) |
6 | 5 | tgioo2cntop 14052 |
. . . 4
β’
(topGenβran (,)) = ((MetOpenβ(abs β β ))
βΎt β) |
7 | 2, 3, 4, 6, 5 | dvbssntrcntop 14156 |
. . 3
β’ (π β dom (β D πΉ) β
((intβ(topGenβran (,)))βπ)) |
8 | | dvcj.c |
. . 3
β’ (π β πΆ β dom (β D πΉ)) |
9 | 7, 8 | sseldd 3157 |
. 2
β’ (π β πΆ β ((intβ(topGenβran
(,)))βπ)) |
10 | 4, 1 | sstrdi 3168 |
. . . . . 6
β’ (π β π β β) |
11 | 1 | a1i 9 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π β β) β β β
β) |
12 | | simpl 109 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π β β) β πΉ:πβΆβ) |
13 | | simpr 110 |
. . . . . . . . 9
β’ ((πΉ:πβΆβ β§ π β β) β π β β) |
14 | 11, 12, 13 | dvbss 14157 |
. . . . . . . 8
β’ ((πΉ:πβΆβ β§ π β β) β dom (β D
πΉ) β π) |
15 | 3, 4, 14 | syl2anc 411 |
. . . . . . 7
β’ (π β dom (β D πΉ) β π) |
16 | 15, 8 | sseldd 3157 |
. . . . . 6
β’ (π β πΆ β π) |
17 | 3, 10, 16 | dvlemap 14152 |
. . . . 5
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)) β β) |
18 | 17 | fmpttd 5672 |
. . . 4
β’ (π β (π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))):{π€ β π β£ π€ # πΆ}βΆβ) |
19 | | ssidd 3177 |
. . . 4
β’ (π β β β
β) |
20 | 5 | cntoptopon 14035 |
. . . . 5
β’
(MetOpenβ(abs β β )) β
(TopOnββ) |
21 | 20 | toponrestid 13524 |
. . . 4
β’
(MetOpenβ(abs β β )) = ((MetOpenβ(abs β
β )) βΎt β) |
22 | 3 | fdmd 5373 |
. . . . . . . . . . . . 13
β’ (π β dom πΉ = π) |
23 | 22 | feq2d 5354 |
. . . . . . . . . . . 12
β’ (π β (πΉ:dom πΉβΆβ β πΉ:πβΆβ)) |
24 | 3, 23 | mpbird 167 |
. . . . . . . . . . 11
β’ (π β πΉ:dom πΉβΆβ) |
25 | 22, 4 | eqsstrd 3192 |
. . . . . . . . . . 11
β’ (π β dom πΉ β β) |
26 | | cnex 7935 |
. . . . . . . . . . . 12
β’ β
β V |
27 | | reex 7945 |
. . . . . . . . . . . 12
β’ β
β V |
28 | 26, 27 | elpm2 6680 |
. . . . . . . . . . 11
β’ (πΉ β (β
βpm β) β (πΉ:dom πΉβΆβ β§ dom πΉ β β)) |
29 | 24, 25, 28 | sylanbrc 417 |
. . . . . . . . . 10
β’ (π β πΉ β (β βpm
β)) |
30 | | dvfpm 14161 |
. . . . . . . . . 10
β’ (πΉ β (β
βpm β) β (β D πΉ):dom (β D πΉ)βΆβ) |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
β’ (π β (β D πΉ):dom (β D πΉ)βΆβ) |
32 | 31 | ffund 5370 |
. . . . . . . 8
β’ (π β Fun (β D πΉ)) |
33 | | funfvbrb 5630 |
. . . . . . . 8
β’ (Fun
(β D πΉ) β (πΆ β dom (β D πΉ) β πΆ(β D πΉ)((β D πΉ)βπΆ))) |
34 | 32, 33 | syl 14 |
. . . . . . 7
β’ (π β (πΆ β dom (β D πΉ) β πΆ(β D πΉ)((β D πΉ)βπΆ))) |
35 | 8, 34 | mpbid 147 |
. . . . . 6
β’ (π β πΆ(β D πΉ)((β D πΉ)βπΆ)) |
36 | | eqid 2177 |
. . . . . . 7
β’ (π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) = (π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) |
37 | 6, 5, 36, 2, 3, 4 | eldvap 14154 |
. . . . . 6
β’ (π β (πΆ(β D πΉ)((β D πΉ)βπΆ) β (πΆ β ((intβ(topGenβran
(,)))βπ) β§
((β D πΉ)βπΆ) β ((π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) limβ πΆ)))) |
38 | 35, 37 | mpbid 147 |
. . . . 5
β’ (π β (πΆ β ((intβ(topGenβran
(,)))βπ) β§
((β D πΉ)βπΆ) β ((π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) limβ πΆ))) |
39 | 38 | simprd 114 |
. . . 4
β’ (π β ((β D πΉ)βπΆ) β ((π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) limβ πΆ)) |
40 | | cjcncf 14078 |
. . . . . 6
β’ β
β (ββcnββ) |
41 | 5 | cncfcn1cntop 14084 |
. . . . . 6
β’
(ββcnββ) =
((MetOpenβ(abs β β )) Cn (MetOpenβ(abs β β
))) |
42 | 40, 41 | eleqtri 2252 |
. . . . 5
β’ β
β ((MetOpenβ(abs β β )) Cn (MetOpenβ(abs β
β ))) |
43 | 31, 8 | ffvelcdmd 5653 |
. . . . 5
β’ (π β ((β D πΉ)βπΆ) β β) |
44 | | unicntopcntop 14039 |
. . . . . 6
β’ β =
βͺ (MetOpenβ(abs β β
)) |
45 | 44 | cncnpi 13731 |
. . . . 5
β’
((β β ((MetOpenβ(abs β β )) Cn
(MetOpenβ(abs β β ))) β§ ((β D πΉ)βπΆ) β β) β β β
(((MetOpenβ(abs β β )) CnP (MetOpenβ(abs β
β )))β((β D πΉ)βπΆ))) |
46 | 42, 43, 45 | sylancr 414 |
. . . 4
β’ (π β β β
(((MetOpenβ(abs β β )) CnP (MetOpenβ(abs β
β )))β((β D πΉ)βπΆ))) |
47 | 18, 19, 5, 21, 39, 46 | limccnpcntop 14147 |
. . 3
β’ (π β (ββ((β
D πΉ)βπΆ)) β ((β β
(π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) limβ πΆ)) |
48 | | cjf 10856 |
. . . . . . 7
β’
β:ββΆβ |
49 | 48 | a1i 9 |
. . . . . 6
β’ (π β
β:ββΆβ) |
50 | 49, 17 | cofmpt 5686 |
. . . . 5
β’ (π β (β β (π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) = (π₯ β {π€ β π β£ π€ # πΆ} β¦ (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))))) |
51 | 3 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β πΉ:πβΆβ) |
52 | | elrabi 2891 |
. . . . . . . . . . 11
β’ (π₯ β {π€ β π β£ π€ # πΆ} β π₯ β π) |
53 | 52 | adantl 277 |
. . . . . . . . . 10
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β π₯ β π) |
54 | 51, 53 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (πΉβπ₯) β β) |
55 | 3, 16 | ffvelcdmd 5653 |
. . . . . . . . . 10
β’ (π β (πΉβπΆ) β β) |
56 | 55 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (πΉβπΆ) β β) |
57 | 54, 56 | subcld 8268 |
. . . . . . . 8
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β ((πΉβπ₯) β (πΉβπΆ)) β β) |
58 | 4 | sselda 3156 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β π₯ β β) |
59 | 52, 58 | sylan2 286 |
. . . . . . . . . 10
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β π₯ β β) |
60 | 4, 16 | sseldd 3157 |
. . . . . . . . . . 11
β’ (π β πΆ β β) |
61 | 60 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β πΆ β β) |
62 | 59, 61 | resubcld 8338 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (π₯ β πΆ) β β) |
63 | 62 | recnd 7986 |
. . . . . . . 8
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (π₯ β πΆ) β β) |
64 | 59 | recnd 7986 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β π₯ β β) |
65 | 61 | recnd 7986 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β πΆ β β) |
66 | | breq1 4007 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β (π€ # πΆ β π₯ # πΆ)) |
67 | 66 | elrab 2894 |
. . . . . . . . . . 11
β’ (π₯ β {π€ β π β£ π€ # πΆ} β (π₯ β π β§ π₯ # πΆ)) |
68 | 67 | simprbi 275 |
. . . . . . . . . 10
β’ (π₯ β {π€ β π β£ π€ # πΆ} β π₯ # πΆ) |
69 | 68 | adantl 277 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β π₯ # πΆ) |
70 | 64, 65, 69 | subap0d 8601 |
. . . . . . . 8
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (π₯ β πΆ) # 0) |
71 | 57, 63, 70 | cjdivapd 10977 |
. . . . . . 7
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) = ((ββ((πΉβπ₯) β (πΉβπΆ))) / (ββ(π₯ β πΆ)))) |
72 | | cjsub 10901 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β β β§ (πΉβπΆ) β β) β
(ββ((πΉβπ₯) β (πΉβπΆ))) = ((ββ(πΉβπ₯)) β (ββ(πΉβπΆ)))) |
73 | 54, 56, 72 | syl2anc 411 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (ββ((πΉβπ₯) β (πΉβπΆ))) = ((ββ(πΉβπ₯)) β (ββ(πΉβπΆ)))) |
74 | | fvco3 5588 |
. . . . . . . . . . 11
β’ ((πΉ:πβΆβ β§ π₯ β π) β ((β β πΉ)βπ₯) = (ββ(πΉβπ₯))) |
75 | 3, 52, 74 | syl2an 289 |
. . . . . . . . . 10
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β ((β β πΉ)βπ₯) = (ββ(πΉβπ₯))) |
76 | | fvco3 5588 |
. . . . . . . . . . . 12
β’ ((πΉ:πβΆβ β§ πΆ β π) β ((β β πΉ)βπΆ) = (ββ(πΉβπΆ))) |
77 | 3, 16, 76 | syl2anc 411 |
. . . . . . . . . . 11
β’ (π β ((β β πΉ)βπΆ) = (ββ(πΉβπΆ))) |
78 | 77 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β ((β β πΉ)βπΆ) = (ββ(πΉβπΆ))) |
79 | 75, 78 | oveq12d 5893 |
. . . . . . . . 9
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) = ((ββ(πΉβπ₯)) β (ββ(πΉβπΆ)))) |
80 | 73, 79 | eqtr4d 2213 |
. . . . . . . 8
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (ββ((πΉβπ₯) β (πΉβπΆ))) = (((β β πΉ)βπ₯) β ((β β πΉ)βπΆ))) |
81 | 62 | cjred 10980 |
. . . . . . . 8
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (ββ(π₯ β πΆ)) = (π₯ β πΆ)) |
82 | 80, 81 | oveq12d 5893 |
. . . . . . 7
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β ((ββ((πΉβπ₯) β (πΉβπΆ))) / (ββ(π₯ β πΆ))) = ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) |
83 | 71, 82 | eqtrd 2210 |
. . . . . 6
β’ ((π β§ π₯ β {π€ β π β£ π€ # πΆ}) β (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ))) = ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) |
84 | 83 | mpteq2dva 4094 |
. . . . 5
β’ (π β (π₯ β {π€ β π β£ π€ # πΆ} β¦ (ββ(((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) = (π₯ β {π€ β π β£ π€ # πΆ} β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ)))) |
85 | 50, 84 | eqtrd 2210 |
. . . 4
β’ (π β (β β (π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) = (π₯ β {π€ β π β£ π€ # πΆ} β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ)))) |
86 | 85 | oveq1d 5890 |
. . 3
β’ (π β ((β β (π₯ β {π€ β π β£ π€ # πΆ} β¦ (((πΉβπ₯) β (πΉβπΆ)) / (π₯ β πΆ)))) limβ πΆ) = ((π₯ β {π€ β π β£ π€ # πΆ} β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) limβ πΆ)) |
87 | 47, 86 | eleqtrd 2256 |
. 2
β’ (π β (ββ((β
D πΉ)βπΆ)) β ((π₯ β {π€ β π β£ π€ # πΆ} β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) limβ πΆ)) |
88 | | eqid 2177 |
. . 3
β’ (π₯ β {π€ β π β£ π€ # πΆ} β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) = (π₯ β {π€ β π β£ π€ # πΆ} β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) |
89 | | fco 5382 |
. . . 4
β’
((β:ββΆβ β§ πΉ:πβΆβ) β (β β
πΉ):πβΆβ) |
90 | 48, 3, 89 | sylancr 414 |
. . 3
β’ (π β (β β πΉ):πβΆβ) |
91 | 6, 5, 88, 2, 90, 4 | eldvap 14154 |
. 2
β’ (π β (πΆ(β D (β β πΉ))(ββ((β D
πΉ)βπΆ)) β (πΆ β ((intβ(topGenβran
(,)))βπ) β§
(ββ((β D πΉ)βπΆ)) β ((π₯ β {π€ β π β£ π€ # πΆ} β¦ ((((β β πΉ)βπ₯) β ((β β πΉ)βπΆ)) / (π₯ β πΆ))) limβ πΆ)))) |
92 | 9, 87, 91 | mpbir2and 944 |
1
β’ (π β πΆ(β D (β β πΉ))(ββ((β D
πΉ)βπΆ))) |