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