Step | Hyp | Ref
| Expression |
1 | | recnprss 14092 |
. . . . 5
β’ (π β {β, β}
β π β
β) |
2 | | reldvg 14084 |
. . . . 5
β’ ((π β β β§ πΉ β (β
βpm π)) β Rel (π D πΉ)) |
3 | 1, 2 | sylan 283 |
. . . 4
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β Rel (π D πΉ)) |
4 | | elpmi 6666 |
. . . . . . . . . . . . . 14
β’ (πΉ β (β
βpm π) β (πΉ:dom πΉβΆβ β§ dom πΉ β π)) |
5 | 4 | simpld 112 |
. . . . . . . . . . . . 13
β’ (πΉ β (β
βpm π) β πΉ:dom πΉβΆβ) |
6 | 5 | adantl 277 |
. . . . . . . . . . . 12
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β πΉ:dom πΉβΆβ) |
7 | 6 | adantr 276 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β πΉ:dom πΉβΆβ) |
8 | 4 | simprd 114 |
. . . . . . . . . . . . . 14
β’ (πΉ β (β
βpm π) β dom πΉ β π) |
9 | 8 | adantl 277 |
. . . . . . . . . . . . 13
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β dom πΉ β π) |
10 | 1 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β π β β) |
11 | 9, 10 | sstrd 3165 |
. . . . . . . . . . . 12
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β dom πΉ β β) |
12 | 11 | adantr 276 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β dom πΉ β β) |
13 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
β’
(MetOpenβ(abs β β )) = (MetOpenβ(abs β
β )) |
14 | 13 | cntoptopon 13968 |
. . . . . . . . . . . . . . . 16
β’
(MetOpenβ(abs β β )) β
(TopOnββ) |
15 | | resttopon 13607 |
. . . . . . . . . . . . . . . 16
β’
(((MetOpenβ(abs β β )) β (TopOnββ)
β§ π β β)
β ((MetOpenβ(abs β β )) βΎt π) β (TopOnβπ)) |
16 | 14, 15 | mpan 424 |
. . . . . . . . . . . . . . 15
β’ (π β β β
((MetOpenβ(abs β β )) βΎt π) β (TopOnβπ)) |
17 | | topontop 13450 |
. . . . . . . . . . . . . . 15
β’
(((MetOpenβ(abs β β )) βΎt π) β (TopOnβπ) β ((MetOpenβ(abs
β β )) βΎt π) β Top) |
18 | 16, 17 | syl 14 |
. . . . . . . . . . . . . 14
β’ (π β β β
((MetOpenβ(abs β β )) βΎt π) β Top) |
19 | 10, 18 | syl 14 |
. . . . . . . . . . . . 13
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β ((MetOpenβ(abs β
β )) βΎt π) β Top) |
20 | | toponuni 13451 |
. . . . . . . . . . . . . . . . 17
β’
(((MetOpenβ(abs β β )) βΎt π) β (TopOnβπ) β π = βͺ
((MetOpenβ(abs β β )) βΎt π)) |
21 | 16, 20 | syl 14 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π = βͺ
((MetOpenβ(abs β β )) βΎt π)) |
22 | 21 | sseq2d 3185 |
. . . . . . . . . . . . . . 15
β’ (π β β β (dom
πΉ β π β dom πΉ β βͺ
((MetOpenβ(abs β β )) βΎt π))) |
23 | 10, 22 | syl 14 |
. . . . . . . . . . . . . 14
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (dom πΉ β π β dom πΉ β βͺ
((MetOpenβ(abs β β )) βΎt π))) |
24 | 9, 23 | mpbid 147 |
. . . . . . . . . . . . 13
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β dom πΉ β βͺ
((MetOpenβ(abs β β )) βΎt π)) |
25 | | eqid 2177 |
. . . . . . . . . . . . . 14
β’ βͺ ((MetOpenβ(abs β β ))
βΎt π) =
βͺ ((MetOpenβ(abs β β ))
βΎt π) |
26 | 25 | ntrss2 13557 |
. . . . . . . . . . . . 13
β’
((((MetOpenβ(abs β β )) βΎt π) β Top β§ dom πΉ β βͺ ((MetOpenβ(abs β β ))
βΎt π))
β ((intβ((MetOpenβ(abs β β )) βΎt
π))βdom πΉ) β dom πΉ) |
27 | 19, 24, 26 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β dom πΉ) |
28 | 27 | sselda 3155 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β π₯ β dom πΉ) |
29 | 7, 12, 28 | dvlemap 14085 |
. . . . . . . . . 10
β’ ((((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β§ π§ β {π€ β dom πΉ β£ π€ # π₯}) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) β β) |
30 | 29 | fmpttd 5671 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β (π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))):{π€ β dom πΉ β£ π€ # π₯}βΆβ) |
31 | | ssrab2 3240 |
. . . . . . . . . 10
β’ {π€ β dom πΉ β£ π€ # π₯} β dom πΉ |
32 | 31, 12 | sstrid 3166 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β {π€ β dom πΉ β£ π€ # π₯} β β) |
33 | 12, 28 | sseldd 3156 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β π₯ β β) |
34 | | simpr 110 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) |
35 | 27, 9 | sstrd 3165 |
. . . . . . . . . 10
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β π) |
36 | 35 | sselda 3155 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β π₯ β π) |
37 | 19 | adantr 276 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β ((MetOpenβ(abs β
β )) βΎt π) β Top) |
38 | 24 | adantr 276 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β dom πΉ β βͺ
((MetOpenβ(abs β β )) βΎt π)) |
39 | 25 | ntropn 13553 |
. . . . . . . . . 10
β’
((((MetOpenβ(abs β β )) βΎt π) β Top β§ dom πΉ β βͺ ((MetOpenβ(abs β β ))
βΎt π))
β ((intβ((MetOpenβ(abs β β )) βΎt
π))βdom πΉ) β ((MetOpenβ(abs
β β )) βΎt π)) |
40 | 37, 38, 39 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β ((MetOpenβ(abs β
β )) βΎt π)) |
41 | | simpll 527 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β π β {β, β}) |
42 | | rabss2 3238 |
. . . . . . . . . . 11
β’
(((intβ((MetOpenβ(abs β β )) βΎt
π))βdom πΉ) β dom πΉ β {π€ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β£ π€ # π₯} β {π€ β dom πΉ β£ π€ # π₯}) |
43 | 27, 42 | syl 14 |
. . . . . . . . . 10
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β {π€ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β£ π€ # π₯} β {π€ β dom πΉ β£ π€ # π₯}) |
44 | 43 | adantr 276 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β {π€ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β£ π€ # π₯} β {π€ β dom πΉ β£ π€ # π₯}) |
45 | 30, 32, 33, 34, 36, 40, 41, 44, 13 | limcimo 14070 |
. . . . . . . 8
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)) β β*π¦ π¦ β ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
46 | 45 | ex 115 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β β*π¦ π¦ β ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
47 | | moanimv 2101 |
. . . . . . 7
β’
(β*π¦(π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ) β§ π¦ β ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β (π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β β*π¦ π¦ β ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
48 | 46, 47 | sylibr 134 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β β*π¦(π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β§ π¦ β ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
49 | | eqid 2177 |
. . . . . . . 8
β’
((MetOpenβ(abs β β )) βΎt π) = ((MetOpenβ(abs β
β )) βΎt π) |
50 | | eqid 2177 |
. . . . . . . 8
β’ (π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
51 | 49, 13, 50, 10, 6, 9 | eldvap 14087 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (π₯(π D πΉ)π¦ β (π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β§ π¦ β ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)))) |
52 | 51 | mobidv 2062 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (β*π¦ π₯(π D πΉ)π¦ β β*π¦(π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β§ π¦ β ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)))) |
53 | 48, 52 | mpbird 167 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β β*π¦ π₯(π D πΉ)π¦) |
54 | 53 | alrimiv 1874 |
. . . 4
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β βπ₯β*π¦ π₯(π D πΉ)π¦) |
55 | | dffun6 5230 |
. . . 4
β’ (Fun
(π D πΉ) β (Rel (π D πΉ) β§ βπ₯β*π¦ π₯(π D πΉ)π¦)) |
56 | 3, 54, 55 | sylanbrc 417 |
. . 3
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β Fun (π D πΉ)) |
57 | 56 | funfnd 5247 |
. 2
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (π D πΉ) Fn dom (π D πΉ)) |
58 | | vex 2740 |
. . . . 5
β’ π¦ β V |
59 | 58 | elrn 4870 |
. . . 4
β’ (π¦ β ran (π D πΉ) β βπ₯ π₯(π D πΉ)π¦) |
60 | 10, 6, 9 | dvcl 14088 |
. . . . . 6
β’ (((π β {β, β} β§
πΉ β (β
βpm π)) β§ π₯(π D πΉ)π¦) β π¦ β β) |
61 | 60 | ex 115 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (π₯(π D πΉ)π¦ β π¦ β β)) |
62 | 61 | exlimdv 1819 |
. . . 4
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (βπ₯ π₯(π D πΉ)π¦ β π¦ β β)) |
63 | 59, 62 | biimtrid 152 |
. . 3
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (π¦ β ran (π D πΉ) β π¦ β β)) |
64 | 63 | ssrdv 3161 |
. 2
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β ran (π D πΉ) β β) |
65 | | df-f 5220 |
. 2
β’ ((π D πΉ):dom (π D πΉ)βΆβ β ((π D πΉ) Fn dom (π D πΉ) β§ ran (π D πΉ) β β)) |
66 | 57, 64, 65 | sylanbrc 417 |
1
β’ ((π β {β, β} β§
πΉ β (β
βpm π)) β (π D πΉ):dom (π D πΉ)βΆβ) |