Metamath Proof Explorer

Theorem uffcfflf

Description: If the domain filter is an ultrafilter, the cluster points of the function are the limit points. (Contributed by Jeff Hankins, 12-Dec-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion uffcfflf 
|- ( ( J e. ( TopOn ` X ) /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( ( J fLimf L ) ` F ) )

Proof

Step Hyp Ref Expression
1 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
2 fmufil 
 |-  ( ( X e. J /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( UFil ` X ) )
3 1 2 syl3an1 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( UFil ` X ) )
4 uffclsflim 
 |-  ( ( ( X FilMap F ) ` L ) e. ( UFil ` X ) -> ( J fClus ( ( X FilMap F ) ` L ) ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
5 3 4 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( J fClus ( ( X FilMap F ) ` L ) ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
6 ufilfil 
 |-  ( L e. ( UFil ` Y ) -> L e. ( Fil ` Y ) )
7 fcfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )
8 6 7 syl3an2 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )
9 flfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
10 6 9 syl3an2 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
11 5 8 10 3eqtr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( UFil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( ( J fLimf L ) ` F ) )