Step | Hyp | Ref
| Expression |
1 | | mopni.1 |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
2 | 1 | mopnuni 23810 |
. . . . 5
β’ (π· β (βMetβπ) β π = βͺ π½) |
3 | 2 | 3ad2ant1 1134 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β π = βͺ
π½) |
4 | 3 | difeq1d 4082 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π β π) = (βͺ π½ β π)) |
5 | | difssd 4093 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π β π) β π) |
6 | | simpl3 1194 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β π
β
β*) |
7 | | simpl1 1192 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β π· β (βMetβπ)) |
8 | | simpl2 1193 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β π β π) |
9 | | eldifi 4087 |
. . . . . . . . 9
β’ (π¦ β (π β π) β π¦ β π) |
10 | 9 | adantl 483 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β π¦ β π) |
11 | | xmetcl 23700 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π¦ β π) β (ππ·π¦) β
β*) |
12 | 7, 8, 10, 11 | syl3anc 1372 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β (ππ·π¦) β
β*) |
13 | | eldif 3921 |
. . . . . . . . . 10
β’ (π¦ β (π β π) β (π¦ β π β§ Β¬ π¦ β π)) |
14 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π§ = π¦ β (ππ·π§) = (ππ·π¦)) |
15 | 14 | breq1d 5116 |
. . . . . . . . . . . . 13
β’ (π§ = π¦ β ((ππ·π§) β€ π
β (ππ·π¦) β€ π
)) |
16 | | blcld.3 |
. . . . . . . . . . . . 13
β’ π = {π§ β π β£ (ππ·π§) β€ π
} |
17 | 15, 16 | elrab2 3649 |
. . . . . . . . . . . 12
β’ (π¦ β π β (π¦ β π β§ (ππ·π¦) β€ π
)) |
18 | 17 | simplbi2 502 |
. . . . . . . . . . 11
β’ (π¦ β π β ((ππ·π¦) β€ π
β π¦ β π)) |
19 | 18 | con3dimp 410 |
. . . . . . . . . 10
β’ ((π¦ β π β§ Β¬ π¦ β π) β Β¬ (ππ·π¦) β€ π
) |
20 | 13, 19 | sylbi 216 |
. . . . . . . . 9
β’ (π¦ β (π β π) β Β¬ (ππ·π¦) β€ π
) |
21 | 20 | adantl 483 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β Β¬ (ππ·π¦) β€ π
) |
22 | | xrltnle 11227 |
. . . . . . . . 9
β’ ((π
β β*
β§ (ππ·π¦) β β*) β (π
< (ππ·π¦) β Β¬ (ππ·π¦) β€ π
)) |
23 | 6, 12, 22 | syl2anc 585 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β (π
< (ππ·π¦) β Β¬ (ππ·π¦) β€ π
)) |
24 | 21, 23 | mpbird 257 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β π
< (ππ·π¦)) |
25 | | qbtwnxr 13125 |
. . . . . . 7
β’ ((π
β β*
β§ (ππ·π¦) β β* β§ π
< (ππ·π¦)) β βπ₯ β β (π
< π₯ β§ π₯ < (ππ·π¦))) |
26 | 6, 12, 24, 25 | syl3anc 1372 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β βπ₯ β β (π
< π₯ β§ π₯ < (ππ·π¦))) |
27 | | qre 12883 |
. . . . . . . 8
β’ (π₯ β β β π₯ β
β) |
28 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π· β (βMetβπ)) |
29 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π¦ β π) |
30 | 12 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (ππ·π¦) β
β*) |
31 | | rexr 11206 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β π₯ β
β*) |
32 | 31 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π₯ β β*) |
33 | 32 | xnegcld 13225 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β -ππ₯ β
β*) |
34 | 30, 33 | xaddcld 13226 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β ((ππ·π¦) +π
-ππ₯)
β β*) |
35 | | blelrn 23786 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π¦ β π β§ ((ππ·π¦) +π
-ππ₯)
β β*) β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β ran (ballβπ·)) |
36 | 28, 29, 34, 35 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β ran (ballβπ·)) |
37 | | simprrr 781 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π₯ < (ππ·π¦)) |
38 | | xposdif 13187 |
. . . . . . . . . . . . 13
β’ ((π₯ β β*
β§ (ππ·π¦) β β*) β (π₯ < (ππ·π¦) β 0 < ((ππ·π¦) +π
-ππ₯))) |
39 | 32, 30, 38 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π₯ < (ππ·π¦) β 0 < ((ππ·π¦) +π
-ππ₯))) |
40 | 37, 39 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β 0 < ((ππ·π¦) +π
-ππ₯)) |
41 | | xblcntr 23780 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π¦ β π β§ (((ππ·π¦) +π
-ππ₯)
β β* β§ 0 < ((ππ·π¦) +π
-ππ₯)))
β π¦ β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))) |
42 | 28, 29, 34, 40, 41 | syl112anc 1375 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π¦ β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))) |
43 | | incom 4162 |
. . . . . . . . . . . . 13
β’ ((π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β© (π(ballβπ·)π₯)) = ((π(ballβπ·)π₯) β© (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))) |
44 | 8 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π β π) |
45 | | xaddcom 13165 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β*
β§ ((ππ·π¦) +π
-ππ₯)
β β*) β (π₯ +π ((ππ·π¦) +π
-ππ₯)) =
(((ππ·π¦) +π
-ππ₯)
+π π₯)) |
46 | 32, 34, 45 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π₯ +π ((ππ·π¦) +π
-ππ₯)) =
(((ππ·π¦) +π
-ππ₯)
+π π₯)) |
47 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π₯ β β) |
48 | | xnpcan 13177 |
. . . . . . . . . . . . . . . . 17
β’ (((ππ·π¦) β β* β§ π₯ β β) β (((ππ·π¦) +π
-ππ₯)
+π π₯) =
(ππ·π¦)) |
49 | 30, 47, 48 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (((ππ·π¦) +π
-ππ₯)
+π π₯) =
(ππ·π¦)) |
50 | 46, 49 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π₯ +π ((ππ·π¦) +π
-ππ₯)) =
(ππ·π¦)) |
51 | 30 | xrleidd 13077 |
. . . . . . . . . . . . . . 15
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (ππ·π¦) β€ (ππ·π¦)) |
52 | 50, 51 | eqbrtrd 5128 |
. . . . . . . . . . . . . 14
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π₯ +π ((ππ·π¦) +π
-ππ₯))
β€ (ππ·π¦)) |
53 | | bldisj 23767 |
. . . . . . . . . . . . . 14
β’ (((π· β (βMetβπ) β§ π β π β§ π¦ β π) β§ (π₯ β β* β§ ((ππ·π¦) +π
-ππ₯)
β β* β§ (π₯ +π ((ππ·π¦) +π
-ππ₯))
β€ (ππ·π¦))) β ((π(ballβπ·)π₯) β© (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))) =
β
) |
54 | 28, 44, 29, 32, 34, 52, 53 | syl33anc 1386 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β ((π(ballβπ·)π₯) β© (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))) =
β
) |
55 | 43, 54 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β ((π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β© (π(ballβπ·)π₯)) = β
) |
56 | | blssm 23787 |
. . . . . . . . . . . . . 14
β’ ((π· β (βMetβπ) β§ π¦ β π β§ ((ππ·π¦) +π
-ππ₯)
β β*) β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β π) |
57 | 28, 29, 34, 56 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β π) |
58 | | reldisj 4412 |
. . . . . . . . . . . . 13
β’ ((π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β π β (((π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β© (π(ballβπ·)π₯)) = β
β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π β (π(ballβπ·)π₯)))) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (((π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β© (π(ballβπ·)π₯)) = β
β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π β (π(ballβπ·)π₯)))) |
60 | 55, 59 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π β (π(ballβπ·)π₯))) |
61 | 6 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π
β
β*) |
62 | | simprrl 780 |
. . . . . . . . . . . . 13
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π
< π₯) |
63 | 1, 16 | blsscls2 23876 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π₯ β β*
β§ π
< π₯)) β π β (π(ballβπ·)π₯)) |
64 | 28, 44, 61, 32, 62, 63 | syl23anc 1378 |
. . . . . . . . . . . 12
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β π β (π(ballβπ·)π₯)) |
65 | 64 | sscond 4102 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π β (π(ballβπ·)π₯)) β (π β π)) |
66 | 60, 65 | sstrd 3955 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π β π)) |
67 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π€ = (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π¦ β π€ β π¦ β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯)))) |
68 | | sseq1 3970 |
. . . . . . . . . . . 12
β’ (π€ = (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π€ β (π β π) β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π β π))) |
69 | 67, 68 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π€ = (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β ((π¦ β π€ β§ π€ β (π β π)) β (π¦ β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β§ (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π β π)))) |
70 | 69 | rspcev 3580 |
. . . . . . . . . 10
β’ (((π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β ran (ballβπ·)
β§ (π¦ β (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β§ (π¦(ballβπ·)((ππ·π¦) +π
-ππ₯))
β (π β π))) β βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π))) |
71 | 36, 42, 66, 70 | syl12anc 836 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ (π₯ β β β§ (π
< π₯ β§ π₯ < (ππ·π¦)))) β βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π))) |
72 | 71 | expr 458 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ π₯ β β) β ((π
< π₯ β§ π₯ < (ππ·π¦)) β βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π)))) |
73 | 27, 72 | sylan2 594 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β§ π₯ β β) β ((π
< π₯ β§ π₯ < (ππ·π¦)) β βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π)))) |
74 | 73 | rexlimdva 3149 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β (βπ₯ β β (π
< π₯ β§ π₯ < (ππ·π¦)) β βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π)))) |
75 | 26, 74 | mpd 15 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π¦ β (π β π)) β βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π))) |
76 | 75 | ralrimiva 3140 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β
βπ¦ β (π β π)βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π))) |
77 | 1 | elmopn 23811 |
. . . . 5
β’ (π· β (βMetβπ) β ((π β π) β π½ β ((π β π) β π β§ βπ¦ β (π β π)βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π))))) |
78 | 77 | 3ad2ant1 1134 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β ((π β π) β π½ β ((π β π) β π β§ βπ¦ β (π β π)βπ€ β ran (ballβπ·)(π¦ β π€ β§ π€ β (π β π))))) |
79 | 5, 76, 78 | mpbir2and 712 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π β π) β π½) |
80 | 4, 79 | eqeltrrd 2835 |
. 2
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (βͺ π½
β π) β π½) |
81 | 1 | mopntop 23809 |
. . . 4
β’ (π· β (βMetβπ) β π½ β Top) |
82 | 81 | 3ad2ant1 1134 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β π½ β Top) |
83 | 16 | ssrab3 4041 |
. . . 4
β’ π β π |
84 | 83, 3 | sseqtrid 3997 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β π β βͺ π½) |
85 | | eqid 2733 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
86 | 85 | iscld2 22395 |
. . 3
β’ ((π½ β Top β§ π β βͺ π½)
β (π β
(Clsdβπ½) β
(βͺ π½ β π) β π½)) |
87 | 82, 84, 86 | syl2anc 585 |
. 2
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π β (Clsdβπ½) β (βͺ π½
β π) β π½)) |
88 | 80, 87 | mpbird 257 |
1
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β π β (Clsdβπ½)) |