Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
2 | 1 | flimfil 23828 |
. . . 4
β’ (π΄ β (π½ fLim πΉ) β πΉ β (Filββͺ π½)) |
3 | 2 | adantl 481 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β πΉ β (Filββͺ π½)) |
4 | | lmcau.1 |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
5 | 4 | mopnuni 24302 |
. . . . 5
β’ (π· β (βMetβπ) β π = βͺ π½) |
6 | 5 | adantr 480 |
. . . 4
β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β π = βͺ π½) |
7 | 6 | fveq2d 6889 |
. . 3
β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β (Filβπ) = (Filββͺ
π½)) |
8 | 3, 7 | eleqtrrd 2830 |
. 2
β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β πΉ β (Filβπ)) |
9 | 1 | flimelbas 23827 |
. . . . . 6
β’ (π΄ β (π½ fLim πΉ) β π΄ β βͺ π½) |
10 | 9 | ad2antlr 724 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π΄ β βͺ π½) |
11 | 5 | ad2antrr 723 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π = βͺ
π½) |
12 | 10, 11 | eleqtrrd 2830 |
. . . 4
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π΄ β π) |
13 | | simplr 766 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π΄ β (π½ fLim πΉ)) |
14 | 4 | mopntop 24301 |
. . . . . . 7
β’ (π· β (βMetβπ) β π½ β Top) |
15 | 14 | ad2antrr 723 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π½ β Top) |
16 | | simpll 764 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π· β (βMetβπ)) |
17 | | rpxr 12989 |
. . . . . . . 8
β’ (π₯ β β+
β π₯ β
β*) |
18 | 17 | adantl 481 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π₯ β
β*) |
19 | 4 | blopn 24364 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π₯ β β*) β (π΄(ballβπ·)π₯) β π½) |
20 | 16, 12, 18, 19 | syl3anc 1368 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β (π΄(ballβπ·)π₯) β π½) |
21 | | simpr 484 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π₯ β
β+) |
22 | | blcntr 24274 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π₯ β β+) β π΄ β (π΄(ballβπ·)π₯)) |
23 | 16, 12, 21, 22 | syl3anc 1368 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β π΄ β (π΄(ballβπ·)π₯)) |
24 | | opnneip 22978 |
. . . . . 6
β’ ((π½ β Top β§ (π΄(ballβπ·)π₯) β π½ β§ π΄ β (π΄(ballβπ·)π₯)) β (π΄(ballβπ·)π₯) β ((neiβπ½)β{π΄})) |
25 | 15, 20, 23, 24 | syl3anc 1368 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β (π΄(ballβπ·)π₯) β ((neiβπ½)β{π΄})) |
26 | | flimnei 23826 |
. . . . 5
β’ ((π΄ β (π½ fLim πΉ) β§ (π΄(ballβπ·)π₯) β ((neiβπ½)β{π΄})) β (π΄(ballβπ·)π₯) β πΉ) |
27 | 13, 25, 26 | syl2anc 583 |
. . . 4
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β (π΄(ballβπ·)π₯) β πΉ) |
28 | | oveq1 7412 |
. . . . . 6
β’ (π¦ = π΄ β (π¦(ballβπ·)π₯) = (π΄(ballβπ·)π₯)) |
29 | 28 | eleq1d 2812 |
. . . . 5
β’ (π¦ = π΄ β ((π¦(ballβπ·)π₯) β πΉ β (π΄(ballβπ·)π₯) β πΉ)) |
30 | 29 | rspcev 3606 |
. . . 4
β’ ((π΄ β π β§ (π΄(ballβπ·)π₯) β πΉ) β βπ¦ β π (π¦(ballβπ·)π₯) β πΉ) |
31 | 12, 27, 30 | syl2anc 583 |
. . 3
β’ (((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β§ π₯ β β+) β
βπ¦ β π (π¦(ballβπ·)π₯) β πΉ) |
32 | 31 | ralrimiva 3140 |
. 2
β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β βπ₯ β β+ βπ¦ β π (π¦(ballβπ·)π₯) β πΉ) |
33 | | iscfil3 25156 |
. . 3
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β π (π¦(ballβπ·)π₯) β πΉ))) |
34 | 33 | adantr 480 |
. 2
β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β π (π¦(ballβπ·)π₯) β πΉ))) |
35 | 8, 32, 34 | mpbir2and 710 |
1
β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β πΉ β (CauFilβπ·)) |