Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β (Filβπ)) β§ π β β+) β π β
β+) |
2 | | equivcau.3 |
. . . . . . . . 9
β’ (π β π
β
β+) |
3 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (Filβπ)) β§ π β β+) β π
β
β+) |
4 | 1, 3 | rpdivcld 12982 |
. . . . . . 7
β’ (((π β§ π β (Filβπ)) β§ π β β+) β (π / π
) β
β+) |
5 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = (π / π
) β (π₯(ballβπ·)π ) = (π₯(ballβπ·)(π / π
))) |
6 | 5 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = (π / π
) β ((π₯(ballβπ·)π ) β π β (π₯(ballβπ·)(π / π
)) β π)) |
7 | 6 | rexbidv 3172 |
. . . . . . . 8
β’ (π = (π / π
) β (βπ₯ β π (π₯(ballβπ·)π ) β π β βπ₯ β π (π₯(ballβπ·)(π / π
)) β π)) |
8 | 7 | rspcv 3579 |
. . . . . . 7
β’ ((π / π
) β β+ β
(βπ β
β+ βπ₯ β π (π₯(ballβπ·)π ) β π β βπ₯ β π (π₯(ballβπ·)(π / π
)) β π)) |
9 | 4, 8 | syl 17 |
. . . . . 6
β’ (((π β§ π β (Filβπ)) β§ π β β+) β
(βπ β
β+ βπ₯ β π (π₯(ballβπ·)π ) β π β βπ₯ β π (π₯(ballβπ·)(π / π
)) β π)) |
10 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β π β (Filβπ)) |
11 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(MetOpenβπΆ) =
(MetOpenβπΆ) |
12 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
13 | | equivcau.1 |
. . . . . . . . . . . 12
β’ (π β πΆ β (Metβπ)) |
14 | | equivcau.2 |
. . . . . . . . . . . 12
β’ (π β π· β (Metβπ)) |
15 | | equivcau.4 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π
Β· (π₯π·π¦))) |
16 | 11, 12, 13, 14, 2, 15 | metss2lem 23890 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π β β+)) β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) |
17 | 16 | ancom2s 649 |
. . . . . . . . . 10
β’ ((π β§ (π β β+ β§ π₯ β π)) β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) |
18 | 17 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β (Filβπ)) β§ (π β β+ β§ π₯ β π)) β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) |
19 | 18 | anassrs 469 |
. . . . . . . 8
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) |
20 | 13 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β πΆ β (Metβπ)) |
21 | | metxmet 23710 |
. . . . . . . . . 10
β’ (πΆ β (Metβπ) β πΆ β (βMetβπ)) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β πΆ β (βMetβπ)) |
23 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β π₯ β π) |
24 | | rpxr 12932 |
. . . . . . . . . 10
β’ (π β β+
β π β
β*) |
25 | 24 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β π β β*) |
26 | | blssm 23794 |
. . . . . . . . 9
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π β β*) β (π₯(ballβπΆ)π) β π) |
27 | 22, 23, 25, 26 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β (π₯(ballβπΆ)π) β π) |
28 | | filss 23227 |
. . . . . . . . . 10
β’ ((π β (Filβπ) β§ ((π₯(ballβπ·)(π / π
)) β π β§ (π₯(ballβπΆ)π) β π β§ (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π))) β (π₯(ballβπΆ)π) β π) |
29 | 28 | 3exp2 1355 |
. . . . . . . . 9
β’ (π β (Filβπ) β ((π₯(ballβπ·)(π / π
)) β π β ((π₯(ballβπΆ)π) β π β ((π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π) β (π₯(ballβπΆ)π) β π)))) |
30 | 29 | com24 95 |
. . . . . . . 8
β’ (π β (Filβπ) β ((π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π) β ((π₯(ballβπΆ)π) β π β ((π₯(ballβπ·)(π / π
)) β π β (π₯(ballβπΆ)π) β π)))) |
31 | 10, 19, 27, 30 | syl3c 66 |
. . . . . . 7
β’ ((((π β§ π β (Filβπ)) β§ π β β+) β§ π₯ β π) β ((π₯(ballβπ·)(π / π
)) β π β (π₯(ballβπΆ)π) β π)) |
32 | 31 | reximdva 3162 |
. . . . . 6
β’ (((π β§ π β (Filβπ)) β§ π β β+) β
(βπ₯ β π (π₯(ballβπ·)(π / π
)) β π β βπ₯ β π (π₯(ballβπΆ)π) β π)) |
33 | 9, 32 | syld 47 |
. . . . 5
β’ (((π β§ π β (Filβπ)) β§ π β β+) β
(βπ β
β+ βπ₯ β π (π₯(ballβπ·)π ) β π β βπ₯ β π (π₯(ballβπΆ)π) β π)) |
34 | 33 | ralrimdva 3148 |
. . . 4
β’ ((π β§ π β (Filβπ)) β (βπ β β+ βπ₯ β π (π₯(ballβπ·)π ) β π β βπ β β+ βπ₯ β π (π₯(ballβπΆ)π) β π)) |
35 | 34 | imdistanda 573 |
. . 3
β’ (π β ((π β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π ) β π) β (π β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπΆ)π) β π))) |
36 | | metxmet 23710 |
. . . 4
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
37 | | iscfil3 24660 |
. . . 4
β’ (π· β (βMetβπ) β (π β (CauFilβπ·) β (π β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π ) β π))) |
38 | 14, 36, 37 | 3syl 18 |
. . 3
β’ (π β (π β (CauFilβπ·) β (π β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π ) β π))) |
39 | | iscfil3 24660 |
. . . 4
β’ (πΆ β (βMetβπ) β (π β (CauFilβπΆ) β (π β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπΆ)π) β π))) |
40 | 13, 21, 39 | 3syl 18 |
. . 3
β’ (π β (π β (CauFilβπΆ) β (π β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπΆ)π) β π))) |
41 | 35, 38, 40 | 3imtr4d 294 |
. 2
β’ (π β (π β (CauFilβπ·) β π β (CauFilβπΆ))) |
42 | 41 | ssrdv 3954 |
1
β’ (π β (CauFilβπ·) β (CauFilβπΆ)) |