Metamath Proof Explorer


Theorem flftg

Description: Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypothesis flftg.l
|- J = ( topGen ` B )
Assertion flftg
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )

Proof

Step Hyp Ref Expression
1 flftg.l
 |-  J = ( topGen ` B )
2 isflf
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) ) ) )
3 1 raleqi
 |-  ( A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) )
4 simpl1
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> J e. ( TopOn ` X ) )
5 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
6 4 5 syl
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> J e. Top )
7 1 6 eqeltrrid
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( topGen ` B ) e. Top )
8 tgclb
 |-  ( B e. TopBases <-> ( topGen ` B ) e. Top )
9 7 8 sylibr
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> B e. TopBases )
10 bastg
 |-  ( B e. TopBases -> B C_ ( topGen ` B ) )
11 eleq2w
 |-  ( u = o -> ( A e. u <-> A e. o ) )
12 sseq2
 |-  ( u = o -> ( ( F " s ) C_ u <-> ( F " s ) C_ o ) )
13 12 rexbidv
 |-  ( u = o -> ( E. s e. L ( F " s ) C_ u <-> E. s e. L ( F " s ) C_ o ) )
14 11 13 imbi12d
 |-  ( u = o -> ( ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
15 14 cbvralvw
 |-  ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. o e. ( topGen ` B ) ( A e. o -> E. s e. L ( F " s ) C_ o ) )
16 ssralv
 |-  ( B C_ ( topGen ` B ) -> ( A. o e. ( topGen ` B ) ( A e. o -> E. s e. L ( F " s ) C_ o ) -> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
17 15 16 syl5bi
 |-  ( B C_ ( topGen ` B ) -> ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) -> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
18 9 10 17 3syl
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) -> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
19 tg2
 |-  ( ( u e. ( topGen ` B ) /\ A e. u ) -> E. o e. B ( A e. o /\ o C_ u ) )
20 r19.29
 |-  ( ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ E. o e. B ( A e. o /\ o C_ u ) ) -> E. o e. B ( ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ ( A e. o /\ o C_ u ) ) )
21 simpl
 |-  ( ( A e. o /\ o C_ u ) -> A e. o )
22 simpr
 |-  ( ( A e. o /\ o C_ u ) -> o C_ u )
23 sstr2
 |-  ( ( F " s ) C_ o -> ( o C_ u -> ( F " s ) C_ u ) )
24 22 23 syl5com
 |-  ( ( A e. o /\ o C_ u ) -> ( ( F " s ) C_ o -> ( F " s ) C_ u ) )
25 24 reximdv
 |-  ( ( A e. o /\ o C_ u ) -> ( E. s e. L ( F " s ) C_ o -> E. s e. L ( F " s ) C_ u ) )
26 21 25 embantd
 |-  ( ( A e. o /\ o C_ u ) -> ( ( A e. o -> E. s e. L ( F " s ) C_ o ) -> E. s e. L ( F " s ) C_ u ) )
27 26 impcom
 |-  ( ( ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ ( A e. o /\ o C_ u ) ) -> E. s e. L ( F " s ) C_ u )
28 27 rexlimivw
 |-  ( E. o e. B ( ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ ( A e. o /\ o C_ u ) ) -> E. s e. L ( F " s ) C_ u )
29 20 28 syl
 |-  ( ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ E. o e. B ( A e. o /\ o C_ u ) ) -> E. s e. L ( F " s ) C_ u )
30 29 ex
 |-  ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) -> ( E. o e. B ( A e. o /\ o C_ u ) -> E. s e. L ( F " s ) C_ u ) )
31 19 30 syl5
 |-  ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) -> ( ( u e. ( topGen ` B ) /\ A e. u ) -> E. s e. L ( F " s ) C_ u ) )
32 31 expdimp
 |-  ( ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) /\ u e. ( topGen ` B ) ) -> ( A e. u -> E. s e. L ( F " s ) C_ u ) )
33 32 ralrimiva
 |-  ( A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) -> A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) )
34 18 33 impbid1
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. u e. ( topGen ` B ) ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
35 3 34 syl5bb
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ A e. X ) -> ( A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) <-> A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
36 35 pm5.32da
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( A e. X /\ A. u e. J ( A e. u -> E. s e. L ( F " s ) C_ u ) ) <-> ( A e. X /\ A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )
37 2 36 bitrd
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> ( A e. X /\ A. o e. B ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )