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 ∈ TopOn ⁡ X ∧ L ∈ UFil ⁡ Y ∧ F : Y ⟶ X → J fClusf L ⁡ F = J fLimf L ⁡ F

Proof

Step Hyp Ref Expression
1 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
2 fmufil ⊢ X ∈ J ∧ L ∈ UFil ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ L ∈ UFil ⁡ X
3 1 2 syl3an1 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ UFil ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ L ∈ UFil ⁡ X
4 uffclsflim ⊢ X FilMap F ⁡ L ∈ UFil ⁡ X → J fClus X FilMap F ⁡ L = J fLim X FilMap F ⁡ L
5 3 4 syl ⊢ J ∈ TopOn ⁡ X ∧ L ∈ UFil ⁡ Y ∧ F : Y ⟶ X → J fClus X FilMap F ⁡ L = J fLim X FilMap F ⁡ L
6 ufilfil ⊢ L ∈ UFil ⁡ Y → L ∈ Fil ⁡ Y
7 fcfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fClusf L ⁡ F = J fClus X FilMap F ⁡ L
8 6 7 syl3an2 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ UFil ⁡ Y ∧ F : Y ⟶ X → J fClusf L ⁡ F = J fClus X FilMap F ⁡ L
9 flfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
10 6 9 syl3an2 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ UFil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
11 5 8 10 3eqtr4d ⊢ J ∈ TopOn ⁡ X ∧ L ∈ UFil ⁡ Y ∧ F : Y ⟶ X → J fClusf L ⁡ F = J fLimf L ⁡ F