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 ) ) ) )