Metamath Proof Explorer

Theorem isflf

Description: The property of being a limit point of a function. (Contributed by Jeff Hankins, 8-Nov-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

Ref Expression
Assertion 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. s e. L ( F " s ) C_ o ) ) ) )

Proof

Step Hyp Ref Expression
1 flfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
2 1 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fLimf L ) ` F ) <-> A e. ( J fLim ( ( X FilMap F ) ` L ) ) ) )
3 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> J e. ( TopOn ` X ) )
4 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
5 4 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> X e. J )
6 filfbas 
 |-  ( L e. ( Fil ` Y ) -> L e. ( fBas ` Y ) )
7 6 3ad2ant2 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> L e. ( fBas ` Y ) )
8 simp3 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> F : Y --> X )
9 fmfil 
 |-  ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
10 5 7 8 9 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
11 flimopn 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) -> ( A e. ( J fLim ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> o e. ( ( X FilMap F ) ` L ) ) ) ) )
12 3 10 11 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( J fLim ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> o e. ( ( X FilMap F ) ` L ) ) ) ) )
13 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ o e. J ) -> o C_ X )
14 3 13 sylan 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> o C_ X )
15 elfm 
 |-  ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( o e. ( ( X FilMap F ) ` L ) <-> ( o C_ X /\ E. s e. L ( F " s ) C_ o ) ) )
16 5 7 8 15 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( o e. ( ( X FilMap F ) ` L ) <-> ( o C_ X /\ E. s e. L ( F " s ) C_ o ) ) )
17 16 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( o e. ( ( X FilMap F ) ` L ) <-> ( o C_ X /\ E. s e. L ( F " s ) C_ o ) ) )
18 14 17 mpbirand 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( o e. ( ( X FilMap F ) ` L ) <-> E. s e. L ( F " s ) C_ o ) )
19 18 imbi2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( ( A e. o -> o e. ( ( X FilMap F ) ` L ) ) <-> ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
20 19 ralbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A. o e. J ( A e. o -> o e. ( ( X FilMap F ) ` L ) ) <-> A. o e. J ( A e. o -> E. s e. L ( F " s ) C_ o ) ) )
21 20 anbi2d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( A e. X /\ A. o e. J ( A e. o -> o e. ( ( X FilMap F ) ` L ) ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> E. s e. L ( F " s ) C_ o ) ) ) )
22 2 12 21 3bitrd 
 |-  ( ( 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. s e. L ( F " s ) C_ o ) ) ) )