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 ) )