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=J
Assertion hausflf2 JHausLFilYF:YXJfLimfLFJfLimfLF1𝑜

Proof

Step Hyp Ref Expression
1 hausflf.x X=J
2 n0 JfLimfLFxxJfLimfLF
3 2 biimpi JfLimfLFxxJfLimfLF
4 1 hausflf JHausLFilYF:YX*xxJfLimfLF
5 euen1b JfLimfLF1𝑜∃!xxJfLimfLF
6 df-eu ∃!xxJfLimfLFxxJfLimfLF*xxJfLimfLF
7 5 6 sylbbr xxJfLimfLF*xxJfLimfLFJfLimfLF1𝑜
8 3 4 7 syl2anr JHausLFilYF:YXJfLimfLFJfLimfLF1𝑜