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 = ⋃ J$
	Assertion	hausflf2	$⊢ ((J \in Haus \land L \in Fil (Y) \land F : Y ⟶ X) \land (J fLimf L) (F) \neq \emptyset) \to (J fLimf L) (F) \approx 1_{𝑜}$

Proof

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