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 e. ( TopOn ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> E. s e. B ( F " s ) C_ o ) ) ) )

Proof

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