Step | Hyp | Ref
| Expression |
1 | | mopni.1 |
. . . . 5
β’ π½ = (MetOpenβπ·) |
2 | 1 | mopntop 23946 |
. . . 4
β’ (π· β (βMetβπ) β π½ β Top) |
3 | 2 | adantr 482 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π) β π½ β Top) |
4 | 1 | mopnuni 23947 |
. . . . 5
β’ (π· β (βMetβπ) β π = βͺ π½) |
5 | 4 | eleq2d 2820 |
. . . 4
β’ (π· β (βMetβπ) β (π β π β π β βͺ π½)) |
6 | 5 | biimpa 478 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π) β π β βͺ π½) |
7 | | eqid 2733 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
8 | 7 | isneip 22609 |
. . 3
β’ ((π½ β Top β§ π β βͺ π½)
β (π β
((neiβπ½)β{π}) β (π β βͺ π½ β§ βπ¦ β π½ (π β π¦ β§ π¦ β π)))) |
9 | 3, 6, 8 | syl2anc 585 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β (π β ((neiβπ½)β{π}) β (π β βͺ π½ β§ βπ¦ β π½ (π β π¦ β§ π¦ β π)))) |
10 | 4 | sseq2d 4015 |
. . . 4
β’ (π· β (βMetβπ) β (π β π β π β βͺ π½)) |
11 | 10 | adantr 482 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π) β (π β π β π β βͺ π½)) |
12 | 11 | anbi1d 631 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β ((π β π β§ βπ¦ β π½ (π β π¦ β§ π¦ β π)) β (π β βͺ π½ β§ βπ¦ β π½ (π β π¦ β§ π¦ β π)))) |
13 | 1 | mopni2 24002 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π¦ β π½ β§ π β π¦) β βπ β β+ (π(ballβπ·)π) β π¦) |
14 | | sstr2 3990 |
. . . . . . . . . . 11
β’ ((π(ballβπ·)π) β π¦ β (π¦ β π β (π(ballβπ·)π) β π)) |
15 | 14 | com12 32 |
. . . . . . . . . 10
β’ (π¦ β π β ((π(ballβπ·)π) β π¦ β (π(ballβπ·)π) β π)) |
16 | 15 | reximdv 3171 |
. . . . . . . . 9
β’ (π¦ β π β (βπ β β+ (π(ballβπ·)π) β π¦ β βπ β β+ (π(ballβπ·)π) β π)) |
17 | 13, 16 | syl5com 31 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π¦ β π½ β§ π β π¦) β (π¦ β π β βπ β β+ (π(ballβπ·)π) β π)) |
18 | 17 | 3exp 1120 |
. . . . . . 7
β’ (π· β (βMetβπ) β (π¦ β π½ β (π β π¦ β (π¦ β π β βπ β β+ (π(ballβπ·)π) β π)))) |
19 | 18 | imp4a 424 |
. . . . . 6
β’ (π· β (βMetβπ) β (π¦ β π½ β ((π β π¦ β§ π¦ β π) β βπ β β+ (π(ballβπ·)π) β π))) |
20 | 19 | ad2antrr 725 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ π β π) β (π¦ β π½ β ((π β π¦ β§ π¦ β π) β βπ β β+ (π(ballβπ·)π) β π))) |
21 | 20 | rexlimdv 3154 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ π β π) β (βπ¦ β π½ (π β π¦ β§ π¦ β π) β βπ β β+ (π(ballβπ·)π) β π)) |
22 | | rpxr 12983 |
. . . . . . . . 9
β’ (π β β+
β π β
β*) |
23 | 1 | blopn 24009 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) β π½) |
24 | 22, 23 | syl3an3 1166 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β (π(ballβπ·)π) β π½) |
25 | | blcntr 23919 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β π β (π(ballβπ·)π)) |
26 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π¦ = (π(ballβπ·)π) β (π β π¦ β π β (π(ballβπ·)π))) |
27 | | sseq1 4008 |
. . . . . . . . . . 11
β’ (π¦ = (π(ballβπ·)π) β (π¦ β π β (π(ballβπ·)π) β π)) |
28 | 26, 27 | anbi12d 632 |
. . . . . . . . . 10
β’ (π¦ = (π(ballβπ·)π) β ((π β π¦ β§ π¦ β π) β (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π))) |
29 | 28 | rspcev 3613 |
. . . . . . . . 9
β’ (((π(ballβπ·)π) β π½ β§ (π β (π(ballβπ·)π) β§ (π(ballβπ·)π) β π)) β βπ¦ β π½ (π β π¦ β§ π¦ β π)) |
30 | 29 | expr 458 |
. . . . . . . 8
β’ (((π(ballβπ·)π) β π½ β§ π β (π(ballβπ·)π)) β ((π(ballβπ·)π) β π β βπ¦ β π½ (π β π¦ β§ π¦ β π))) |
31 | 24, 25, 30 | syl2anc 585 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π β β+) β ((π(ballβπ·)π) β π β βπ¦ β π½ (π β π¦ β§ π¦ β π))) |
32 | 31 | 3expia 1122 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π) β (π β β+ β ((π(ballβπ·)π) β π β βπ¦ β π½ (π β π¦ β§ π¦ β π)))) |
33 | 32 | rexlimdv 3154 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π) β (βπ β β+ (π(ballβπ·)π) β π β βπ¦ β π½ (π β π¦ β§ π¦ β π))) |
34 | 33 | adantr 482 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ π β π) β (βπ β β+ (π(ballβπ·)π) β π β βπ¦ β π½ (π β π¦ β§ π¦ β π))) |
35 | 21, 34 | impbid 211 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ π β π) β (βπ¦ β π½ (π β π¦ β§ π¦ β π) β βπ β β+ (π(ballβπ·)π) β π)) |
36 | 35 | pm5.32da 580 |
. 2
β’ ((π· β (βMetβπ) β§ π β π) β ((π β π β§ βπ¦ β π½ (π β π¦ β§ π¦ β π)) β (π β π β§ βπ β β+ (π(ballβπ·)π) β π))) |
37 | 9, 12, 36 | 3bitr2d 307 |
1
β’ ((π· β (βMetβπ) β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ βπ β β+ (π(ballβπ·)π) β π))) |