Metamath Proof Explorer

Theorem flfval

Description: Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flfval 
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )

Proof

Step Hyp Ref Expression
1 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
2 filtop 
 |-  ( L e. ( Fil ` Y ) -> Y e. L )
3 elmapg 
 |-  ( ( X e. J /\ Y e. L ) -> ( F e. ( X ^m Y ) <-> F : Y --> X ) )
4 1 2 3 syl2an 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( F e. ( X ^m Y ) <-> F : Y --> X ) )
5 4 biimpar 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ F : Y --> X ) -> F e. ( X ^m Y ) )
6 flffval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fLimf L ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) )
7 6 fveq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( ( J fLimf L ) ` F ) = ( ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) ` F ) )
8 oveq2 
 |-  ( f = F -> ( X FilMap f ) = ( X FilMap F ) )
9 8 fveq1d 
 |-  ( f = F -> ( ( X FilMap f ) ` L ) = ( ( X FilMap F ) ` L ) )
10 9 oveq2d 
 |-  ( f = F -> ( J fLim ( ( X FilMap f ) ` L ) ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
11 eqid 
 |-  ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) )
12 ovex 
 |-  ( J fLim ( ( X FilMap F ) ` L ) ) e. _V
13 10 11 12 fvmpt 
 |-  ( F e. ( X ^m Y ) -> ( ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
14 7 13 sylan9eq 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ F e. ( X ^m Y ) ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
15 5 14 syldan 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
16 15 3impa 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )