Step | Hyp | Ref
| Expression |
1 | | simpll1 1213 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β π· β (βMetβπ)) |
2 | | simprl 770 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β π§ β π½) |
3 | | simprr 772 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β π΄ β π§) |
4 | | metdscn.j |
. . . . . . . 8
β’ π½ = (MetOpenβπ·) |
5 | 4 | mopni2 23771 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π§ β π½ β§ π΄ β π§) β βπ β β+ (π΄(ballβπ·)π) β π§) |
6 | 1, 2, 3, 5 | syl3anc 1372 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β βπ β β+ (π΄(ballβπ·)π) β π§) |
7 | | simprr 772 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (π΄(ballβπ·)π) β π§) |
8 | 7 | ssrind 4194 |
. . . . . . 7
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β ((π΄(ballβπ·)π) β© π) β (π§ β© π)) |
9 | | rpgt0 12856 |
. . . . . . . . . 10
β’ (π β β+
β 0 < π) |
10 | | 0re 11091 |
. . . . . . . . . . 11
β’ 0 β
β |
11 | | rpre 12852 |
. . . . . . . . . . 11
β’ (π β β+
β π β
β) |
12 | | ltnle 11168 |
. . . . . . . . . . 11
β’ ((0
β β β§ π
β β) β (0 < π β Β¬ π β€ 0)) |
13 | 10, 11, 12 | sylancr 588 |
. . . . . . . . . 10
β’ (π β β+
β (0 < π β
Β¬ π β€
0)) |
14 | 9, 13 | mpbid 231 |
. . . . . . . . 9
β’ (π β β+
β Β¬ π β€
0) |
15 | 14 | ad2antrl 727 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β Β¬ π β€ 0) |
16 | | simpllr 775 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (πΉβπ΄) = 0) |
17 | 16 | breq2d 5116 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (π β€ (πΉβπ΄) β π β€ 0)) |
18 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β π· β (βMetβπ)) |
19 | | simpl2 1193 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π β π) |
20 | 19 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β π β π) |
21 | | simpl3 1194 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π΄ β π) |
22 | 21 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β π΄ β π) |
23 | | rpxr 12853 |
. . . . . . . . . . . . 13
β’ (π β β+
β π β
β*) |
24 | 23 | ad2antrl 727 |
. . . . . . . . . . . 12
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β π β β*) |
25 | | metdscn.f |
. . . . . . . . . . . . 13
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
26 | 25 | metdsge 24134 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π β β*) β (π β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)π)) = β
)) |
27 | 18, 20, 22, 24, 26 | syl31anc 1374 |
. . . . . . . . . . 11
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (π β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)π)) = β
)) |
28 | 17, 27 | bitr3d 281 |
. . . . . . . . . 10
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (π β€ 0 β (π β© (π΄(ballβπ·)π)) = β
)) |
29 | | incom 4160 |
. . . . . . . . . . 11
β’ (π β© (π΄(ballβπ·)π)) = ((π΄(ballβπ·)π) β© π) |
30 | 29 | eqeq1i 2743 |
. . . . . . . . . 10
β’ ((π β© (π΄(ballβπ·)π)) = β
β ((π΄(ballβπ·)π) β© π) = β
) |
31 | 28, 30 | bitrdi 287 |
. . . . . . . . 9
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (π β€ 0 β ((π΄(ballβπ·)π) β© π) = β
)) |
32 | 31 | necon3bbid 2980 |
. . . . . . . 8
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (Β¬ π β€ 0 β ((π΄(ballβπ·)π) β© π) β β
)) |
33 | 15, 32 | mpbid 231 |
. . . . . . 7
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β ((π΄(ballβπ·)π) β© π) β β
) |
34 | | ssn0 4359 |
. . . . . . 7
β’ ((((π΄(ballβπ·)π) β© π) β (π§ β© π) β§ ((π΄(ballβπ·)π) β© π) β β
) β (π§ β© π) β β
) |
35 | 8, 33, 34 | syl2anc 585 |
. . . . . 6
β’
(((((π· β
(βMetβπ) β§
π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β§ (π β β+ β§ (π΄(ballβπ·)π) β π§)) β (π§ β© π) β β
) |
36 | 6, 35 | rexlimddv 3157 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ (π§ β π½ β§ π΄ β π§)) β (π§ β© π) β β
) |
37 | 36 | expr 458 |
. . . 4
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β§ π§ β π½) β (π΄ β π§ β (π§ β© π) β β
)) |
38 | 37 | ralrimiva 3142 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β βπ§ β π½ (π΄ β π§ β (π§ β© π) β β
)) |
39 | 4 | mopntopon 23714 |
. . . . . . 7
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
40 | 39 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β π½ β (TopOnβπ)) |
41 | 40 | adantr 482 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π½ β (TopOnβπ)) |
42 | | topontop 22184 |
. . . . 5
β’ (π½ β (TopOnβπ) β π½ β Top) |
43 | 41, 42 | syl 17 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π½ β Top) |
44 | | toponuni 22185 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
45 | 41, 44 | syl 17 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π = βͺ π½) |
46 | 19, 45 | sseqtrd 3983 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π β βͺ π½) |
47 | 21, 45 | eleqtrd 2841 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π΄ β βͺ π½) |
48 | | eqid 2738 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
49 | 48 | elcls 22346 |
. . . 4
β’ ((π½ β Top β§ π β βͺ π½
β§ π΄ β βͺ π½)
β (π΄ β
((clsβπ½)βπ) β βπ§ β π½ (π΄ β π§ β (π§ β© π) β β
))) |
50 | 43, 46, 47, 49 | syl3anc 1372 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β (π΄ β ((clsβπ½)βπ) β βπ§ β π½ (π΄ β π§ β (π§ β© π) β β
))) |
51 | 38, 50 | mpbird 257 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) = 0) β π΄ β ((clsβπ½)βπ)) |
52 | | incom 4160 |
. . . . . . 7
β’ ((π΄(ballβπ·)(πΉβπ΄)) β© π) = (π β© (π΄(ballβπ·)(πΉβπ΄))) |
53 | 25 | metdsf 24133 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
54 | 53 | ffvelcdmda 7030 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π β π) β§ π΄ β π) β (πΉβπ΄) β (0[,]+β)) |
55 | 54 | 3impa 1111 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) β (0[,]+β)) |
56 | | eliccxr 13281 |
. . . . . . . . . 10
β’ ((πΉβπ΄) β (0[,]+β) β (πΉβπ΄) β
β*) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) β
β*) |
58 | 57 | xrleidd 13000 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) β€ (πΉβπ΄)) |
59 | 25 | metdsge 24134 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) β β*) β ((πΉβπ΄) β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)(πΉβπ΄))) = β
)) |
60 | 57, 59 | mpdan 686 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β ((πΉβπ΄) β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)(πΉβπ΄))) = β
)) |
61 | 58, 60 | mpbid 231 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (π β© (π΄(ballβπ·)(πΉβπ΄))) = β
) |
62 | 52, 61 | eqtrid 2790 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β ((π΄(ballβπ·)(πΉβπ΄)) β© π) = β
) |
63 | 62 | adantr 482 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β ((π΄(ballβπ·)(πΉβπ΄)) β© π) = β
) |
64 | 40 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π½ β (TopOnβπ)) |
65 | 64, 42 | syl 17 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π½ β Top) |
66 | | simpll2 1214 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π β π) |
67 | 64, 44 | syl 17 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π = βͺ π½) |
68 | 66, 67 | sseqtrd 3983 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π β βͺ π½) |
69 | | simplr 768 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π΄ β ((clsβπ½)βπ)) |
70 | | simpll1 1213 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π· β (βMetβπ)) |
71 | | simpll3 1215 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π΄ β π) |
72 | 57 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β (πΉβπ΄) β
β*) |
73 | 4 | blopn 23778 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π΄ β π β§ (πΉβπ΄) β β*) β (π΄(ballβπ·)(πΉβπ΄)) β π½) |
74 | 70, 71, 72, 73 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β (π΄(ballβπ·)(πΉβπ΄)) β π½) |
75 | | simpr 486 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β 0 < (πΉβπ΄)) |
76 | | xblcntr 23686 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π΄ β π β§ ((πΉβπ΄) β β* β§ 0 <
(πΉβπ΄))) β π΄ β (π΄(ballβπ·)(πΉβπ΄))) |
77 | 70, 71, 72, 75, 76 | syl112anc 1375 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β π΄ β (π΄(ballβπ·)(πΉβπ΄))) |
78 | 48 | clsndisj 22348 |
. . . . . . . 8
β’ (((π½ β Top β§ π β βͺ π½
β§ π΄ β
((clsβπ½)βπ)) β§ ((π΄(ballβπ·)(πΉβπ΄)) β π½ β§ π΄ β (π΄(ballβπ·)(πΉβπ΄)))) β ((π΄(ballβπ·)(πΉβπ΄)) β© π) β β
) |
79 | 65, 68, 69, 74, 77, 78 | syl32anc 1379 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β§ 0 < (πΉβπ΄)) β ((π΄(ballβπ·)(πΉβπ΄)) β© π) β β
) |
80 | 79 | ex 414 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β (0 < (πΉβπ΄) β ((π΄(ballβπ·)(πΉβπ΄)) β© π) β β
)) |
81 | 80 | necon2bd 2958 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β (((π΄(ballβπ·)(πΉβπ΄)) β© π) = β
β Β¬ 0 < (πΉβπ΄))) |
82 | 63, 81 | mpd 15 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β Β¬ 0 < (πΉβπ΄)) |
83 | | elxrge0 13303 |
. . . . . . . . 9
β’ ((πΉβπ΄) β (0[,]+β) β ((πΉβπ΄) β β* β§ 0 β€
(πΉβπ΄))) |
84 | 83 | simprbi 498 |
. . . . . . . 8
β’ ((πΉβπ΄) β (0[,]+β) β 0 β€ (πΉβπ΄)) |
85 | 55, 84 | syl 17 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β 0 β€ (πΉβπ΄)) |
86 | | 0xr 11136 |
. . . . . . . 8
β’ 0 β
β* |
87 | | xrleloe 12992 |
. . . . . . . 8
β’ ((0
β β* β§ (πΉβπ΄) β β*) β (0 β€
(πΉβπ΄) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄)))) |
88 | 86, 57, 87 | sylancr 588 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (0 β€ (πΉβπ΄) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄)))) |
89 | 85, 88 | mpbid 231 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄))) |
90 | 89 | adantr 482 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄))) |
91 | 90 | ord 863 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β (Β¬ 0 < (πΉβπ΄) β 0 = (πΉβπ΄))) |
92 | 82, 91 | mpd 15 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β 0 = (πΉβπ΄)) |
93 | 92 | eqcomd 2744 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ π΄ β ((clsβπ½)βπ)) β (πΉβπ΄) = 0) |
94 | 51, 93 | impbida 800 |
1
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β ((πΉβπ΄) = 0 β π΄ β ((clsβπ½)βπ))) |