Metamath Proof Explorer

Theorem hausflf

Description: If a function has its values in a Hausdorff space, then it has at most one limit value. (Contributed by FL, 14-Nov-2010) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis hausflf.x ⊢ X = ⋃ J
Assertion hausflf ⊢ J ∈ Haus ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → ∃* x x ∈ J fLimf L ⁡ F

Proof

Step Hyp Ref Expression
1 hausflf.x ⊢ X = ⋃ J
2 hausflimi ⊢ J ∈ Haus → ∃* x x ∈ J fLim X FilMap F ⁡ L
3 2 3ad2ant1 ⊢ J ∈ Haus ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → ∃* x x ∈ J fLim X FilMap F ⁡ L
4 haustop ⊢ J ∈ Haus → J ∈ Top
5 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
6 4 5 sylib ⊢ J ∈ Haus → J ∈ TopOn ⁡ X
7 flfval ⊢ J ∈ TopOn ⁡ X ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
8 6 7 syl3an1 ⊢ J ∈ Haus ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → J fLimf L ⁡ F = J fLim X FilMap F ⁡ L
9 8 eleq2d ⊢ J ∈ Haus ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → x ∈ J fLimf L ⁡ F ↔ x ∈ J fLim X FilMap F ⁡ L
10 9 mobidv ⊢ J ∈ Haus ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → ∃* x x ∈ J fLimf L ⁡ F ↔ ∃* x x ∈ J fLim X FilMap F ⁡ L
11 3 10 mpbird ⊢ J ∈ Haus ∧ L ∈ Fil ⁡ Y ∧ F : Y ⟶ X → ∃* x x ∈ J fLimf L ⁡ F