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=\bigcup J$$
Assertion	hausflf2	$$⊢\left(\left(J\in \mathrm{Haus}\wedge L\in \mathrm{Fil}\left(Y\right)\wedge F:Y⟶X\right)\wedge \left(J\mathrm{fLimf}L\right)\left(F\right)\ne \varnothing \right)\to \left(J\mathrm{fLimf}L\right)\left(F\right)\approx 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		hausflf.x	$$⊢X=\bigcup J$$
2		n0	$$⊢\left(J\mathrm{fLimf}L\right)\left(F\right)\ne \varnothing \leftrightarrow \exists xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)$$
3	2	biimpi	$$⊢\left(J\mathrm{fLimf}L\right)\left(F\right)\ne \varnothing \to \exists xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)$$
4	1	hausflf	$$⊢\left(J\in \mathrm{Haus}\wedge L\in \mathrm{Fil}\left(Y\right)\wedge F:Y⟶X\right)\to {\exists }^{*}xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)$$
5		euen1b	$$⊢\left(J\mathrm{fLimf}L\right)\left(F\right)\approx 1_{𝑜}\leftrightarrow \exists !xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)$$
6		df-eu	$$⊢\exists !xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)\leftrightarrow \left(\exists xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)\wedge {\exists }^{*}xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)\right)$$
7	5 6	sylbbr	$$⊢\left(\exists xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)\wedge {\exists }^{*}xx\in \left(J\mathrm{fLimf}L\right)\left(F\right)\right)\to \left(J\mathrm{fLimf}L\right)\left(F\right)\approx 1_{𝑜}$$
8	3 4 7	syl2anr	$$⊢\left(\left(J\in \mathrm{Haus}\wedge L\in \mathrm{Fil}\left(Y\right)\wedge F:Y⟶X\right)\wedge \left(J\mathrm{fLimf}L\right)\left(F\right)\ne \varnothing \right)\to \left(J\mathrm{fLimf}L\right)\left(F\right)\approx 1_{𝑜}$$