This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hausflf2

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

Ref Expression
Hypothesis hausflf.x 
|- X = U. J
Assertion hausflf2 
|- ( ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( ( J fLimf L ) ` F ) =/= (/) ) -> ( ( J fLimf L ) ` F ) ~~ 1o )

Proof

Step Hyp Ref Expression
1 hausflf.x 
 |-  X = U. J
2 n0 
 |-  ( ( ( J fLimf L ) ` F ) =/= (/) <-> E. x x e. ( ( J fLimf L ) ` F ) )
3 2 biimpi 
 |-  ( ( ( J fLimf L ) ` F ) =/= (/) -> E. x x e. ( ( J fLimf L ) ` F ) )
4 1 hausflf 
 |-  ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( ( J fLimf L ) ` F ) )
5 euen1b 
 |-  ( ( ( J fLimf L ) ` F ) ~~ 1o <-> E! x x e. ( ( J fLimf L ) ` F ) )
6 df-eu 
 |-  ( E! x x e. ( ( J fLimf L ) ` F ) <-> ( E. x x e. ( ( J fLimf L ) ` F ) /\ E* x x e. ( ( J fLimf L ) ` F ) ) )
7 5 6 sylbbr 
 |-  ( ( E. x x e. ( ( J fLimf L ) ` F ) /\ E* x x e. ( ( J fLimf L ) ` F ) ) -> ( ( J fLimf L ) ` F ) ~~ 1o )
8 3 4 7 syl2anr 
 |-  ( ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ ( ( J fLimf L ) ` F ) =/= (/) ) -> ( ( J fLimf L ) ` F ) ~~ 1o )