Metamath Proof Explorer


Theorem flffbas

Description: Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis flffbas.l L = Y filGen B
Assertion flffbas J TopOn X B fBas Y F : Y X A J fLimf L F A X o J A o s B F s o

Proof

Step Hyp Ref Expression
1 flffbas.l L = Y filGen B
2 fgcl B fBas Y Y filGen B Fil Y
3 1 2 eqeltrid B fBas Y L Fil Y
4 isflf J TopOn X L Fil Y F : Y X A J fLimf L F A X o J A o t L F t o
5 3 4 syl3an2 J TopOn X B fBas Y F : Y X A J fLimf L F A X o J A o t L F t o
6 1 eleq2i t L t Y filGen B
7 elfg B fBas Y t Y filGen B t Y s B s t
8 7 3ad2ant2 J TopOn X B fBas Y F : Y X t Y filGen B t Y s B s t
9 sstr2 F s F t F t o F s o
10 imass2 s t F s F t
11 9 10 syl11 F t o s t F s o
12 11 adantl J TopOn X B fBas Y F : Y X F t o s t F s o
13 12 reximdv J TopOn X B fBas Y F : Y X F t o s B s t s B F s o
14 13 ex J TopOn X B fBas Y F : Y X F t o s B s t s B F s o
15 14 com23 J TopOn X B fBas Y F : Y X s B s t F t o s B F s o
16 15 adantld J TopOn X B fBas Y F : Y X t Y s B s t F t o s B F s o
17 8 16 sylbid J TopOn X B fBas Y F : Y X t Y filGen B F t o s B F s o
18 17 adantr J TopOn X B fBas Y F : Y X A X t Y filGen B F t o s B F s o
19 6 18 syl5bi J TopOn X B fBas Y F : Y X A X t L F t o s B F s o
20 19 rexlimdv J TopOn X B fBas Y F : Y X A X t L F t o s B F s o
21 ssfg B fBas Y B Y filGen B
22 21 1 sseqtrrdi B fBas Y B L
23 22 sselda B fBas Y s B s L
24 23 3ad2antl2 J TopOn X B fBas Y F : Y X s B s L
25 24 ad2ant2r J TopOn X B fBas Y F : Y X A X s B F s o s L
26 simprr J TopOn X B fBas Y F : Y X A X s B F s o F s o
27 imaeq2 t = s F t = F s
28 27 sseq1d t = s F t o F s o
29 28 rspcev s L F s o t L F t o
30 25 26 29 syl2anc J TopOn X B fBas Y F : Y X A X s B F s o t L F t o
31 30 rexlimdvaa J TopOn X B fBas Y F : Y X A X s B F s o t L F t o
32 20 31 impbid J TopOn X B fBas Y F : Y X A X t L F t o s B F s o
33 32 imbi2d J TopOn X B fBas Y F : Y X A X A o t L F t o A o s B F s o
34 33 ralbidv J TopOn X B fBas Y F : Y X A X o J A o t L F t o o J A o s B F s o
35 34 pm5.32da J TopOn X B fBas Y F : Y X A X o J A o t L F t o A X o J A o s B F s o
36 5 35 bitrd J TopOn X B fBas Y F : Y X A J fLimf L F A X o J A o s B F s o