Step | Hyp | Ref
| Expression |
1 | | metnrmlem.u |
. . 3
β’ π = βͺ π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) |
2 | | metnrmlem.1 |
. . . . 5
β’ (π β π· β (βMetβπ)) |
3 | | metdscn.j |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
4 | 3 | mopntop 23809 |
. . . . 5
β’ (π· β (βMetβπ) β π½ β Top) |
5 | 2, 4 | syl 17 |
. . . 4
β’ (π β π½ β Top) |
6 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β π) β π· β (βMetβπ)) |
7 | | metnrmlem.3 |
. . . . . . . . 9
β’ (π β π β (Clsdβπ½)) |
8 | | eqid 2737 |
. . . . . . . . . 10
β’ βͺ π½ =
βͺ π½ |
9 | 8 | cldss 22396 |
. . . . . . . . 9
β’ (π β (Clsdβπ½) β π β βͺ π½) |
10 | 7, 9 | syl 17 |
. . . . . . . 8
β’ (π β π β βͺ π½) |
11 | 3 | mopnuni 23810 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β π = βͺ π½) |
12 | 2, 11 | syl 17 |
. . . . . . . 8
β’ (π β π = βͺ π½) |
13 | 10, 12 | sseqtrrd 3990 |
. . . . . . 7
β’ (π β π β π) |
14 | 13 | sselda 3949 |
. . . . . 6
β’ ((π β§ π‘ β π) β π‘ β π) |
15 | | metdscn.f |
. . . . . . . . . 10
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
16 | | metnrmlem.2 |
. . . . . . . . . 10
β’ (π β π β (Clsdβπ½)) |
17 | | metnrmlem.4 |
. . . . . . . . . 10
β’ (π β (π β© π) = β
) |
18 | 15, 3, 2, 16, 7, 17 | metnrmlem1a 24237 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (0 < (πΉβπ‘) β§ if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β
β+)) |
19 | 18 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) β
β+) |
20 | 19 | rphalfcld 12976 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β
β+) |
21 | 20 | rpxrd 12965 |
. . . . . 6
β’ ((π β§ π‘ β π) β (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β
β*) |
22 | 3 | blopn 23872 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π‘ β π β§ (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β β*) β
(π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β π½) |
23 | 6, 14, 21, 22 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π‘ β π) β (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β π½) |
24 | 23 | ralrimiva 3144 |
. . . 4
β’ (π β βπ‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β π½) |
25 | | iunopn 22263 |
. . . 4
β’ ((π½ β Top β§ βπ‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β π½) β βͺ
π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β π½) |
26 | 5, 24, 25 | syl2anc 585 |
. . 3
β’ (π β βͺ π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β π½) |
27 | 1, 26 | eqeltrid 2842 |
. 2
β’ (π β π β π½) |
28 | | blcntr 23782 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π‘ β π β§ (if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2) β β+) β
π‘ β (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
29 | 6, 14, 20, 28 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π‘ β π) β π‘ β (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
30 | 29 | snssd 4774 |
. . . . 5
β’ ((π β§ π‘ β π) β {π‘} β (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
31 | 30 | ralrimiva 3144 |
. . . 4
β’ (π β βπ‘ β π {π‘} β (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
32 | | ss2iun 4977 |
. . . 4
β’
(βπ‘ β
π {π‘} β (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2)) β βͺ π‘ β π {π‘} β βͺ
π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
33 | 31, 32 | syl 17 |
. . 3
β’ (π β βͺ π‘ β π {π‘} β βͺ
π‘ β π (π‘(ballβπ·)(if(1 β€ (πΉβπ‘), 1, (πΉβπ‘)) / 2))) |
34 | | iunid 5025 |
. . . 4
β’ βͺ π‘ β π {π‘} = π |
35 | 34 | eqcomi 2746 |
. . 3
β’ π = βͺ π‘ β π {π‘} |
36 | 33, 35, 1 | 3sstr4g 3994 |
. 2
β’ (π β π β π) |
37 | 27, 36 | jca 513 |
1
β’ (π β (π β π½ β§ π β π)) |