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

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 = U. J
Assertion hausflf 
|- ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( ( J fLimf L ) ` F ) )

Proof

Step Hyp Ref Expression
1 hausflf.x 
 |-  X = U. J
2 hausflimi 
 |-  ( J e. Haus -> E* x x e. ( J fLim ( ( X FilMap F ) ` L ) ) )
3 2 3ad2ant1 
 |-  ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( J fLim ( ( X FilMap F ) ` L ) ) )
4 haustop 
 |-  ( J e. Haus -> J e. Top )
5 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
6 4 5 sylib 
 |-  ( J e. Haus -> J e. ( TopOn ` X ) )
7 flfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
8 6 7 syl3an1 
 |-  ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fLimf L ) ` F ) = ( J fLim ( ( X FilMap F ) ` L ) ) )
9 8 eleq2d 
 |-  ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( x e. ( ( J fLimf L ) ` F ) <-> x e. ( J fLim ( ( X FilMap F ) ` L ) ) ) )
10 9 mobidv 
 |-  ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( E* x x e. ( ( J fLimf L ) ` F ) <-> E* x x e. ( J fLim ( ( X FilMap F ) ` L ) ) ) )
11 3 10 mpbird 
 |-  ( ( J e. Haus /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> E* x x e. ( ( J fLimf L ) ` F ) )