Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. 2
β’
(TopOpenββfld) =
(TopOpenββfld) |
2 | 1 | tgioo2 24539 |
. 2
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
3 | | reelprrecn 11204 |
. . 3
β’ β
β {β, β} |
4 | 3 | a1i 11 |
. 2
β’ (π β β β {β,
β}) |
5 | | retop 24498 |
. . . . 5
β’
(topGenβran (,)) β Top |
6 | | dvcnvre.1 |
. . . . . . 7
β’ (π β πΉ:πβ1-1-ontoβπ) |
7 | | f1ofo 6840 |
. . . . . . 7
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβontoβπ) |
8 | | forn 6808 |
. . . . . . 7
β’ (πΉ:πβontoβπ β ran πΉ = π) |
9 | 6, 7, 8 | 3syl 18 |
. . . . . 6
β’ (π β ran πΉ = π) |
10 | | dvcnvre.f |
. . . . . . 7
β’ (π β πΉ β (πβcnββ)) |
11 | | cncff 24633 |
. . . . . . 7
β’ (πΉ β (πβcnββ) β πΉ:πβΆβ) |
12 | | frn 6724 |
. . . . . . 7
β’ (πΉ:πβΆβ β ran πΉ β β) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . 6
β’ (π β ran πΉ β β) |
14 | 9, 13 | eqsstrrd 4021 |
. . . . 5
β’ (π β π β β) |
15 | | uniretop 24499 |
. . . . . 6
β’ β =
βͺ (topGenβran (,)) |
16 | 15 | ntrss2 22781 |
. . . . 5
β’
(((topGenβran (,)) β Top β§ π β β) β
((intβ(topGenβran (,)))βπ) β π) |
17 | 5, 14, 16 | sylancr 587 |
. . . 4
β’ (π β
((intβ(topGenβran (,)))βπ) β π) |
18 | | f1ocnvfv2 7277 |
. . . . . 6
β’ ((πΉ:πβ1-1-ontoβπ β§ π₯ β π) β (πΉβ(β‘πΉβπ₯)) = π₯) |
19 | 6, 18 | sylan 580 |
. . . . 5
β’ ((π β§ π₯ β π) β (πΉβ(β‘πΉβπ₯)) = π₯) |
20 | | eqid 2732 |
. . . . . . . . 9
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
21 | 20 | rexmet 24527 |
. . . . . . . 8
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
22 | | dvcnvre.d |
. . . . . . . . . . . 12
β’ (π β dom (β D πΉ) = π) |
23 | | dvbsss 25643 |
. . . . . . . . . . . . 13
β’ dom
(β D πΉ) β
β |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β dom (β D πΉ) β
β) |
25 | 22, 24 | eqsstrrd 4021 |
. . . . . . . . . . 11
β’ (π β π β β) |
26 | 15 | ntrss2 22781 |
. . . . . . . . . . 11
β’
(((topGenβran (,)) β Top β§ π β β) β
((intβ(topGenβran (,)))βπ) β π) |
27 | 5, 25, 26 | sylancr 587 |
. . . . . . . . . 10
β’ (π β
((intβ(topGenβran (,)))βπ) β π) |
28 | | ax-resscn 11169 |
. . . . . . . . . . . . 13
β’ β
β β |
29 | 28 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
β) |
30 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆβ) |
31 | | fss 6734 |
. . . . . . . . . . . . 13
β’ ((πΉ:πβΆβ β§ β β
β) β πΉ:πβΆβ) |
32 | 30, 28, 31 | sylancl 586 |
. . . . . . . . . . . 12
β’ (π β πΉ:πβΆβ) |
33 | 29, 32, 25, 2, 1 | dvbssntr 25641 |
. . . . . . . . . . 11
β’ (π β dom (β D πΉ) β
((intβ(topGenβran (,)))βπ)) |
34 | 22, 33 | eqsstrrd 4021 |
. . . . . . . . . 10
β’ (π β π β ((intβ(topGenβran
(,)))βπ)) |
35 | 27, 34 | eqssd 3999 |
. . . . . . . . 9
β’ (π β
((intβ(topGenβran (,)))βπ) = π) |
36 | 15 | isopn3 22790 |
. . . . . . . . . 10
β’
(((topGenβran (,)) β Top β§ π β β) β (π β (topGenβran (,)) β
((intβ(topGenβran (,)))βπ) = π)) |
37 | 5, 25, 36 | sylancr 587 |
. . . . . . . . 9
β’ (π β (π β (topGenβran (,)) β
((intβ(topGenβran (,)))βπ) = π)) |
38 | 35, 37 | mpbird 256 |
. . . . . . . 8
β’ (π β π β (topGenβran
(,))) |
39 | | f1ocnv 6845 |
. . . . . . . . . 10
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
40 | | f1of 6833 |
. . . . . . . . . 10
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
41 | 6, 39, 40 | 3syl 18 |
. . . . . . . . 9
β’ (π β β‘πΉ:πβΆπ) |
42 | 41 | ffvelcdmda 7086 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (β‘πΉβπ₯) β π) |
43 | | eqid 2732 |
. . . . . . . . . 10
β’
(MetOpenβ((abs β β ) βΎ (β Γ
β))) = (MetOpenβ((abs β β ) βΎ (β Γ
β))) |
44 | 20, 43 | tgioo 24532 |
. . . . . . . . 9
β’
(topGenβran (,)) = (MetOpenβ((abs β β ) βΎ
(β Γ β))) |
45 | 44 | mopni2 24222 |
. . . . . . . 8
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§ π β (topGenβran (,)) β§ (β‘πΉβπ₯) β π) β βπ β β+ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π) |
46 | 21, 38, 42, 45 | mp3an2ani 1468 |
. . . . . . 7
β’ ((π β§ π₯ β π) β βπ β β+ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π) |
47 | 10 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β πΉ β (πβcnββ)) |
48 | 22 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β dom (β D πΉ) = π) |
49 | | dvcnvre.z |
. . . . . . . . 9
β’ (π β Β¬ 0 β ran
(β D πΉ)) |
50 | 49 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β Β¬ 0 β ran (β D
πΉ)) |
51 | 6 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β πΉ:πβ1-1-ontoβπ) |
52 | 42 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (β‘πΉβπ₯) β π) |
53 | | rphalfcl 13005 |
. . . . . . . . 9
β’ (π β β+
β (π / 2) β
β+) |
54 | 53 | ad2antrl 726 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (π / 2) β
β+) |
55 | 25 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β π β β) |
56 | 55, 52 | sseldd 3983 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (β‘πΉβπ₯) β β) |
57 | 54 | rpred 13020 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (π / 2) β β) |
58 | 56, 57 | resubcld 11646 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β ((β‘πΉβπ₯) β (π / 2)) β β) |
59 | 56, 57 | readdcld 11247 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β ((β‘πΉβπ₯) + (π / 2)) β β) |
60 | | elicc2 13393 |
. . . . . . . . . . . . . . . 16
β’ ((((β‘πΉβπ₯) β (π / 2)) β β β§ ((β‘πΉβπ₯) + (π / 2)) β β) β (π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2))) β (π¦ β β β§ ((β‘πΉβπ₯) β (π / 2)) β€ π¦ β§ π¦ β€ ((β‘πΉβπ₯) + (π / 2))))) |
61 | 58, 59, 60 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2))) β (π¦ β β β§ ((β‘πΉβπ₯) β (π / 2)) β€ π¦ β§ π¦ β€ ((β‘πΉβπ₯) + (π / 2))))) |
62 | 61 | biimpa 477 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β (π¦ β β β§ ((β‘πΉβπ₯) β (π / 2)) β€ π¦ β§ π¦ β€ ((β‘πΉβπ₯) + (π / 2)))) |
63 | 62 | simp1d 1142 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β π¦ β β) |
64 | 56 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β (β‘πΉβπ₯) β β) |
65 | | simplrl 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β π β β+) |
66 | 65 | rpred 13020 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β π β β) |
67 | 64, 66 | resubcld 11646 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) β π) β β) |
68 | 58 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) β (π / 2)) β β) |
69 | 65, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β (π / 2) β
β+) |
70 | 69 | rpred 13020 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β (π / 2) β β) |
71 | | rphalflt 13007 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β (π / 2) < π) |
72 | 65, 71 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β (π / 2) < π) |
73 | 70, 66, 64, 72 | ltsub2dd 11831 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) β π) < ((β‘πΉβπ₯) β (π / 2))) |
74 | 62 | simp2d 1143 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) β (π / 2)) β€ π¦) |
75 | 67, 68, 63, 73, 74 | ltletrd 11378 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) β π) < π¦) |
76 | 59 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) + (π / 2)) β β) |
77 | 64, 66 | readdcld 11247 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) + π) β β) |
78 | 62 | simp3d 1144 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β π¦ β€ ((β‘πΉβπ₯) + (π / 2))) |
79 | 70, 66, 64, 72 | ltadd2dd 11377 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) + (π / 2)) < ((β‘πΉβπ₯) + π)) |
80 | 63, 76, 77, 78, 79 | lelttrd 11376 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β π¦ < ((β‘πΉβπ₯) + π)) |
81 | 67 | rexrd 11268 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) β π) β
β*) |
82 | 77 | rexrd 11268 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β ((β‘πΉβπ₯) + π) β
β*) |
83 | | elioo2 13369 |
. . . . . . . . . . . . . 14
β’ ((((β‘πΉβπ₯) β π) β β* β§ ((β‘πΉβπ₯) + π) β β*) β (π¦ β (((β‘πΉβπ₯) β π)(,)((β‘πΉβπ₯) + π)) β (π¦ β β β§ ((β‘πΉβπ₯) β π) < π¦ β§ π¦ < ((β‘πΉβπ₯) + π)))) |
84 | 81, 82, 83 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β (π¦ β (((β‘πΉβπ₯) β π)(,)((β‘πΉβπ₯) + π)) β (π¦ β β β§ ((β‘πΉβπ₯) β π) < π¦ β§ π¦ < ((β‘πΉβπ₯) + π)))) |
85 | 63, 75, 80, 84 | mpbir3and 1342 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β§ π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2)))) β π¦ β (((β‘πΉβπ₯) β π)(,)((β‘πΉβπ₯) + π))) |
86 | 85 | ex 413 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (π¦ β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2))) β π¦ β (((β‘πΉβπ₯) β π)(,)((β‘πΉβπ₯) + π)))) |
87 | 86 | ssrdv 3988 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2))) β (((β‘πΉβπ₯) β π)(,)((β‘πΉβπ₯) + π))) |
88 | | rpre 12986 |
. . . . . . . . . . . 12
β’ (π β β+
β π β
β) |
89 | 88 | ad2antrl 726 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β π β β) |
90 | 20 | bl2ioo 24528 |
. . . . . . . . . . 11
β’ (((β‘πΉβπ₯) β β β§ π β β) β ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) = (((β‘πΉβπ₯) β π)(,)((β‘πΉβπ₯) + π))) |
91 | 56, 89, 90 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) = (((β‘πΉβπ₯) β π)(,)((β‘πΉβπ₯) + π))) |
92 | 87, 91 | sseqtrrd 4023 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2))) β ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π)) |
93 | | simprr 771 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π) |
94 | 92, 93 | sstrd 3992 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β (((β‘πΉβπ₯) β (π / 2))[,]((β‘πΉβπ₯) + (π / 2))) β π) |
95 | | eqid 2732 |
. . . . . . . 8
β’
(topGenβran (,)) = (topGenβran (,)) |
96 | | eqid 2732 |
. . . . . . . 8
β’
((TopOpenββfld) βΎt π) =
((TopOpenββfld) βΎt π) |
97 | | eqid 2732 |
. . . . . . . 8
β’
((TopOpenββfld) βΎt π) =
((TopOpenββfld) βΎt π) |
98 | 47, 48, 50, 51, 52, 54, 94, 95, 1, 96, 97 | dvcnvrelem2 25759 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ (π β β+ β§ ((β‘πΉβπ₯)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π)) β ((πΉβ(β‘πΉβπ₯)) β ((intβ(topGenβran
(,)))βπ) β§ β‘πΉ β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))β(πΉβ(β‘πΉβπ₯))))) |
99 | 46, 98 | rexlimddv 3161 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((πΉβ(β‘πΉβπ₯)) β ((intβ(topGenβran
(,)))βπ) β§ β‘πΉ β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))β(πΉβ(β‘πΉβπ₯))))) |
100 | 99 | simpld 495 |
. . . . 5
β’ ((π β§ π₯ β π) β (πΉβ(β‘πΉβπ₯)) β ((intβ(topGenβran
(,)))βπ)) |
101 | 19, 100 | eqeltrrd 2834 |
. . . 4
β’ ((π β§ π₯ β π) β π₯ β ((intβ(topGenβran
(,)))βπ)) |
102 | 17, 101 | eqelssd 4003 |
. . 3
β’ (π β
((intβ(topGenβran (,)))βπ) = π) |
103 | 15 | isopn3 22790 |
. . . 4
β’
(((topGenβran (,)) β Top β§ π β β) β (π β (topGenβran (,)) β
((intβ(topGenβran (,)))βπ) = π)) |
104 | 5, 14, 103 | sylancr 587 |
. . 3
β’ (π β (π β (topGenβran (,)) β
((intβ(topGenβran (,)))βπ) = π)) |
105 | 102, 104 | mpbird 256 |
. 2
β’ (π β π β (topGenβran
(,))) |
106 | 99 | simprd 496 |
. . . . . 6
β’ ((π β§ π₯ β π) β β‘πΉ β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))β(πΉβ(β‘πΉβπ₯)))) |
107 | 19 | fveq2d 6895 |
. . . . . 6
β’ ((π β§ π₯ β π) β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))β(πΉβ(β‘πΉβπ₯))) =
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))βπ₯)) |
108 | 106, 107 | eleqtrd 2835 |
. . . . 5
β’ ((π β§ π₯ β π) β β‘πΉ β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))βπ₯)) |
109 | 108 | ralrimiva 3146 |
. . . 4
β’ (π β βπ₯ β π β‘πΉ β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))βπ₯)) |
110 | 1 | cnfldtopon 24519 |
. . . . . 6
β’
(TopOpenββfld) β
(TopOnββ) |
111 | 14, 28 | sstrdi 3994 |
. . . . . 6
β’ (π β π β β) |
112 | | resttopon 22885 |
. . . . . 6
β’
(((TopOpenββfld) β (TopOnββ)
β§ π β β)
β ((TopOpenββfld) βΎt π) β (TopOnβπ)) |
113 | 110, 111,
112 | sylancr 587 |
. . . . 5
β’ (π β
((TopOpenββfld) βΎt π) β (TopOnβπ)) |
114 | 25, 28 | sstrdi 3994 |
. . . . . 6
β’ (π β π β β) |
115 | | resttopon 22885 |
. . . . . 6
β’
(((TopOpenββfld) β (TopOnββ)
β§ π β β)
β ((TopOpenββfld) βΎt π) β (TopOnβπ)) |
116 | 110, 114,
115 | sylancr 587 |
. . . . 5
β’ (π β
((TopOpenββfld) βΎt π) β (TopOnβπ)) |
117 | | cncnp 23004 |
. . . . 5
β’
((((TopOpenββfld) βΎt π) β (TopOnβπ) β§
((TopOpenββfld) βΎt π) β (TopOnβπ)) β (β‘πΉ β
(((TopOpenββfld) βΎt π) Cn ((TopOpenββfld)
βΎt π))
β (β‘πΉ:πβΆπ β§ βπ₯ β π β‘πΉ β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))βπ₯)))) |
118 | 113, 116,
117 | syl2anc 584 |
. . . 4
β’ (π β (β‘πΉ β
(((TopOpenββfld) βΎt π) Cn ((TopOpenββfld)
βΎt π))
β (β‘πΉ:πβΆπ β§ βπ₯ β π β‘πΉ β
((((TopOpenββfld) βΎt π) CnP ((TopOpenββfld)
βΎt π))βπ₯)))) |
119 | 41, 109, 118 | mpbir2and 711 |
. . 3
β’ (π β β‘πΉ β
(((TopOpenββfld) βΎt π) Cn ((TopOpenββfld)
βΎt π))) |
120 | 1, 97, 96 | cncfcn 24650 |
. . . 4
β’ ((π β β β§ π β β) β (πβcnβπ) = (((TopOpenββfld)
βΎt π) Cn
((TopOpenββfld) βΎt π))) |
121 | 111, 114,
120 | syl2anc 584 |
. . 3
β’ (π β (πβcnβπ) = (((TopOpenββfld)
βΎt π) Cn
((TopOpenββfld) βΎt π))) |
122 | 119, 121 | eleqtrrd 2836 |
. 2
β’ (π β β‘πΉ β (πβcnβπ)) |
123 | 1, 2, 4, 105, 6, 122, 22, 49 | dvcnv 25718 |
1
β’ (π β (β D β‘πΉ) = (π₯ β π β¦ (1 / ((β D πΉ)β(β‘πΉβπ₯))))) |