hausflimi

Description: One direction of hausflim . A filter in a Hausdorff space has at most one limit. (Contributed by FL, 14-Nov-2010) (Revised by Mario Carneiro, 21-Sep-2015)

		Ref	Expression
	Assertion	hausflimi	$⊢ J \in Haus \to \exists^{*} x x \in (J fLim F)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to J \in Haus$
2		simprll	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to x \in (J fLim F)$
3		eqid	$⊢ ⋃ J = ⋃ J$
4	3	flimelbas	$⊢ x \in (J fLim F) \to x \in ⋃ J$
5	2 4	syl	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to x \in ⋃ J$
6		simprlr	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to y \in (J fLim F)$
7	3	flimelbas	$⊢ y \in (J fLim F) \to y \in ⋃ J$
8	6 7	syl	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to y \in ⋃ J$
9		simprr	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to x \neq y$
10	3	hausnei	$⊢ (J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \to \exists u \in J \exists v \in J (x \in u \land y \in v \land u \cap v = \emptyset)$
11	1 5 8 9 10	syl13anc	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to \exists u \in J \exists v \in J (x \in u \land y \in v \land u \cap v = \emptyset)$
12		df-3an	$⊢ (x \in u \land y \in v \land u \cap v = \emptyset) \leftrightarrow ((x \in u \land y \in v) \land u \cap v = \emptyset)$
13		simprl	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to (x \in (J fLim F) \land y \in (J fLim F))$
14		hausflimlem	$⊢ ((x \in (J fLim F) \land y \in (J fLim F)) \land (u \in J \land v \in J) \land (x \in u \land y \in v)) \to u \cap v \neq \emptyset$
15	14	3expa	$⊢ (((x \in (J fLim F) \land y \in (J fLim F)) \land (u \in J \land v \in J)) \land (x \in u \land y \in v)) \to u \cap v \neq \emptyset$
16	13 15	sylanl1	$⊢ (((J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \land (u \in J \land v \in J)) \land (x \in u \land y \in v)) \to u \cap v \neq \emptyset$
17	16	a1d	$⊢ (((J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \land (u \in J \land v \in J)) \land (x \in u \land y \in v)) \to (x \neq y \to u \cap v \neq \emptyset)$
18	17	necon4d	$⊢ (((J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \land (u \in J \land v \in J)) \land (x \in u \land y \in v)) \to (u \cap v = \emptyset \to x = y)$
19	18	expimpd	$⊢ ((J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \land (u \in J \land v \in J)) \to (((x \in u \land y \in v) \land u \cap v = \emptyset) \to x = y)$
20	12 19	biimtrid	$⊢ ((J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \land (u \in J \land v \in J)) \to ((x \in u \land y \in v \land u \cap v = \emptyset) \to x = y)$
21	20	rexlimdvva	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to (\exists u \in J \exists v \in J (x \in u \land y \in v \land u \cap v = \emptyset) \to x = y)$
22	11 21	mpd	$⊢ (J \in Haus \land ((x \in (J fLim F) \land y \in (J fLim F)) \land x \neq y)) \to x = y$
23	22	expr	$⊢ (J \in Haus \land (x \in (J fLim F) \land y \in (J fLim F))) \to (x \neq y \to x = y)$
24	23	necon1bd	$⊢ (J \in Haus \land (x \in (J fLim F) \land y \in (J fLim F))) \to (\neg x = y \to x = y)$
25	24	pm2.18d	$⊢ (J \in Haus \land (x \in (J fLim F) \land y \in (J fLim F))) \to x = y$
26	25	ex	$⊢ J \in Haus \to ((x \in (J fLim F) \land y \in (J fLim F)) \to x = y)$
27	26	alrimivv	$⊢ J \in Haus \to \forall x \forall y ((x \in (J fLim F) \land y \in (J fLim F)) \to x = y)$
28		eleq1w	$⊢ x = y \to (x \in (J fLim F) \leftrightarrow y \in (J fLim F))$
29	28	mo4	$⊢ \exists^{*} x x \in (J fLim F) \leftrightarrow \forall x \forall y ((x \in (J fLim F) \land y \in (J fLim F)) \to x = y)$
30	27 29	sylibr	$⊢ J \in Haus \to \exists^{*} x x \in (J fLim F)$

Metamath Proof Explorer

Theorem hausflimi

Proof