Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β (π βpm β)) β§ π β β+)
β π β
β+) |
2 | | equivcau.3 |
. . . . . . . 8
β’ (π β π
β
β+) |
3 | 2 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (π βpm β)) β§ π β β+)
β π
β
β+) |
4 | 1, 3 | rpdivcld 12975 |
. . . . . 6
β’ (((π β§ π β (π βpm β)) β§ π β β+)
β (π / π
) β
β+) |
5 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = (π / π
) β ((πβπ)(ballβπ·)π ) = ((πβπ)(ballβπ·)(π / π
))) |
6 | 5 | feq3d 6656 |
. . . . . . . 8
β’ (π = (π / π
) β ((π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π ) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) |
7 | 6 | rexbidv 3176 |
. . . . . . 7
β’ (π = (π / π
) β (βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π ) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) |
8 | 7 | rspcv 3578 |
. . . . . 6
β’ ((π / π
) β β+ β
(βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π ) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) |
9 | 4, 8 | syl 17 |
. . . . 5
β’ (((π β§ π β (π βpm β)) β§ π β β+)
β (βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π ) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) |
10 | | simprr 772 |
. . . . . . . 8
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
))) |
11 | | elpmi 8785 |
. . . . . . . . . . . 12
β’ (π β (π βpm β) β (π:dom πβΆπ β§ dom π β β)) |
12 | 11 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (π βpm β) β π:dom πβΆπ) |
13 | 12 | ad3antlr 730 |
. . . . . . . . . 10
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β π:dom πβΆπ) |
14 | | resss 5963 |
. . . . . . . . . . . 12
β’ (π βΎ
(β€β₯βπ)) β π |
15 | | dmss 5859 |
. . . . . . . . . . . 12
β’ ((π βΎ
(β€β₯βπ)) β π β dom (π βΎ (β€β₯βπ)) β dom π) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . 11
β’ dom
(π βΎ
(β€β₯βπ)) β dom π |
17 | | uzid 12779 |
. . . . . . . . . . . . 13
β’ (π β β€ β π β
(β€β₯βπ)) |
18 | 17 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β π β (β€β₯βπ)) |
19 | | fdm 6678 |
. . . . . . . . . . . . 13
β’ ((π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)) β dom (π βΎ (β€β₯βπ)) =
(β€β₯βπ)) |
20 | 19 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β dom (π βΎ (β€β₯βπ)) =
(β€β₯βπ)) |
21 | 18, 20 | eleqtrrd 2841 |
. . . . . . . . . . 11
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β π β dom (π βΎ (β€β₯βπ))) |
22 | 16, 21 | sselid 3943 |
. . . . . . . . . 10
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β π β dom π) |
23 | 13, 22 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β (πβπ) β π) |
24 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(MetOpenβπΆ) =
(MetOpenβπΆ) |
25 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
26 | | equivcau.1 |
. . . . . . . . . . . . 13
β’ (π β πΆ β (Metβπ)) |
27 | | equivcau.2 |
. . . . . . . . . . . . 13
β’ (π β π· β (Metβπ)) |
28 | | equivcau.4 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π
Β· (π₯π·π¦))) |
29 | 24, 25, 26, 27, 2, 28 | metss2lem 23870 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π β β+)) β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) |
30 | 29 | expr 458 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β (π β β+ β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π))) |
31 | 30 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ₯ β π (π β β+ β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π))) |
32 | 31 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β βπ₯ β π (π β β+ β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π))) |
33 | | simplr 768 |
. . . . . . . . 9
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β π β β+) |
34 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = (πβπ) β (π₯(ballβπ·)(π / π
)) = ((πβπ)(ballβπ·)(π / π
))) |
35 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = (πβπ) β (π₯(ballβπΆ)π) = ((πβπ)(ballβπΆ)π)) |
36 | 34, 35 | sseq12d 3978 |
. . . . . . . . . . 11
β’ (π₯ = (πβπ) β ((π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π) β ((πβπ)(ballβπ·)(π / π
)) β ((πβπ)(ballβπΆ)π))) |
37 | 36 | imbi2d 341 |
. . . . . . . . . 10
β’ (π₯ = (πβπ) β ((π β β+ β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) β (π β β+ β ((πβπ)(ballβπ·)(π / π
)) β ((πβπ)(ballβπΆ)π)))) |
38 | 37 | rspcv 3578 |
. . . . . . . . 9
β’ ((πβπ) β π β (βπ₯ β π (π β β+ β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) β (π β β+ β ((πβπ)(ballβπ·)(π / π
)) β ((πβπ)(ballβπΆ)π)))) |
39 | 23, 32, 33, 38 | syl3c 66 |
. . . . . . . 8
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β ((πβπ)(ballβπ·)(π / π
)) β ((πβπ)(ballβπΆ)π)) |
40 | 10, 39 | fssd 6687 |
. . . . . . 7
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ (π β β€
β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)))) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π)) |
41 | 40 | expr 458 |
. . . . . 6
β’ ((((π β§ π β (π βpm β)) β§ π β β+)
β§ π β β€)
β ((π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π))) |
42 | 41 | reximdva 3166 |
. . . . 5
β’ (((π β§ π β (π βpm β)) β§ π β β+)
β (βπ β
β€ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)(π / π
)) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π))) |
43 | 9, 42 | syld 47 |
. . . 4
β’ (((π β§ π β (π βpm β)) β§ π β β+)
β (βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π ) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π))) |
44 | 43 | ralrimdva 3152 |
. . 3
β’ ((π β§ π β (π βpm β)) β
(βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π ) β βπ β β+ βπ β β€ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π))) |
45 | 44 | ss2rabdv 4034 |
. 2
β’ (π β {π β (π βpm β) β£
βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π )} β {π β (π βpm β) β£
βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π)}) |
46 | | metxmet 23690 |
. . 3
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
47 | | caufval 24642 |
. . 3
β’ (π· β (βMetβπ) β (Cauβπ·) = {π β (π βpm β) β£
βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π )}) |
48 | 27, 46, 47 | 3syl 18 |
. 2
β’ (π β (Cauβπ·) = {π β (π βpm β) β£
βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π )}) |
49 | | metxmet 23690 |
. . 3
β’ (πΆ β (Metβπ) β πΆ β (βMetβπ)) |
50 | | caufval 24642 |
. . 3
β’ (πΆ β (βMetβπ) β (CauβπΆ) = {π β (π βpm β) β£
βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π)}) |
51 | 26, 49, 50 | 3syl 18 |
. 2
β’ (π β (CauβπΆ) = {π β (π βpm β) β£
βπ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπΆ)π)}) |
52 | 45, 48, 51 | 3sstr4d 3992 |
1
β’ (π β (Cauβπ·) β (CauβπΆ)) |