hausflim

Description: A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Hypothesis	flimcf.1	$⊢ X = ⋃ J$
	Assertion	hausflim	$⊢ J \in Haus \leftrightarrow (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f))$

Proof

Step	Hyp	Ref	Expression
1		flimcf.1	$⊢ X = ⋃ J$
2		haustop	$⊢ J \in Haus \to J \in Top$
3		hausflimi	$⊢ J \in Haus \to \exists^{*} x x \in (J fLim f)$
4	3	ralrimivw	$⊢ J \in Haus \to \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)$
5	2 4	jca	$⊢ J \in Haus \to (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f))$
6		simpl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to J \in Top$
7	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
8	6 7	sylib	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to J \in TopOn (X)$
9		simprll	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to z \in X$
10	9	snssd	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{z\} \subseteq X$
11	9	snn0d	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{z\} \neq \emptyset$
12		neifil	$⊢ (J \in TopOn (X) \land \{z\} \subseteq X \land \{z\} \neq \emptyset) \to nei (J) (\{z\}) \in Fil (X)$
13	8 10 11 12	syl3anc	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \in Fil (X)$
14		filfbas	$⊢ nei (J) (\{z\}) \in Fil (X) \to nei (J) (\{z\}) \in fBas (X)$
15	13 14	syl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \in fBas (X)$
16		simprlr	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to w \in X$
17	16	snssd	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{w\} \subseteq X$
18	16	snn0d	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{w\} \neq \emptyset$
19		neifil	$⊢ (J \in TopOn (X) \land \{w\} \subseteq X \land \{w\} \neq \emptyset) \to nei (J) (\{w\}) \in Fil (X)$
20	8 17 18 19	syl3anc	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{w\}) \in Fil (X)$
21		filfbas	$⊢ nei (J) (\{w\}) \in Fil (X) \to nei (J) (\{w\}) \in fBas (X)$
22	20 21	syl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{w\}) \in fBas (X)$
23		fbunfip	$⊢ (nei (J) (\{z\}) \in fBas (X) \land nei (J) (\{w\}) \in fBas (X)) \to (\neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \leftrightarrow \forall u \in nei (J) (\{z\}) \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset)$
24	15 22 23	syl2anc	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \leftrightarrow \forall u \in nei (J) (\{z\}) \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset)$
25	1	neisspw	$⊢ J \in Top \to nei (J) (\{z\}) \subseteq 𝒫 X$
26	1	neisspw	$⊢ J \in Top \to nei (J) (\{w\}) \subseteq 𝒫 X$
27	25 26	unssd	$⊢ J \in Top \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X$
28	27	adantr	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X$
29	28	a1d	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X)$
30		ssun1	$⊢ nei (J) (\{z\}) \subseteq nei (J) (\{z\}) \cup nei (J) (\{w\})$
31		filn0	$⊢ nei (J) (\{z\}) \in Fil (X) \to nei (J) (\{z\}) \neq \emptyset$
32	13 31	syl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \neq \emptyset$
33		ssn0	$⊢ (nei (J) (\{z\}) \subseteq nei (J) (\{z\}) \cup nei (J) (\{w\}) \land nei (J) (\{z\}) \neq \emptyset) \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \neq \emptyset$
34	30 32 33	sylancr	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \neq \emptyset$
35	34	a1d	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \neq \emptyset)$
36		idd	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to \neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))$
37	29 35 36	3jcad	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to (nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X \land nei (J) (\{z\}) \cup nei (J) (\{w\}) \neq \emptyset \land \neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
38	1	topopn	$⊢ J \in Top \to X \in J$
39	38	adantr	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to X \in J$
40		fsubbas	$⊢ X \in J \to (fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X) \leftrightarrow (nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X \land nei (J) (\{z\}) \cup nei (J) (\{w\}) \neq \emptyset \land \neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
41	39 40	syl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X) \leftrightarrow (nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X \land nei (J) (\{z\}) \cup nei (J) (\{w\}) \neq \emptyset \land \neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
42		fgcl	$⊢ fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X) \to X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in Fil (X)$
43	42	adantl	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in Fil (X)$
44		simplrr	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to z \neq w$
45	9	adantr	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to z \in X$
46	16	adantr	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to w \in X$
47		fvex	$⊢ nei (J) (\{z\}) \in V$
48		fvex	$⊢ nei (J) (\{w\}) \in V$
49	47 48	unex	$⊢ nei (J) (\{z\}) \cup nei (J) (\{w\}) \in V$
50		ssfii	$⊢ nei (J) (\{z\}) \cup nei (J) (\{w\}) \in V \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
51	49 50	ax-mp	$⊢ nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
52		ssfg	$⊢ fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X) \to fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
53	52	adantl	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
54	51 53	sstrid	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
55	30 54	sstrid	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to nei (J) (\{z\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
56	8	adantr	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to J \in TopOn (X)$
57		elflim	$⊢ (J \in TopOn (X) \land X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in Fil (X)) \to (z \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \leftrightarrow (z \in X \land nei (J) (\{z\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
58	56 43 57	syl2anc	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to (z \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \leftrightarrow (z \in X \land nei (J) (\{z\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
59	45 55 58	mpbir2and	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to z \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
60	54	unssbd	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to nei (J) (\{w\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
61		elflim	$⊢ (J \in TopOn (X) \land X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in Fil (X)) \to (w \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \leftrightarrow (w \in X \land nei (J) (\{w\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
62	56 43 61	syl2anc	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to (w \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \leftrightarrow (w \in X \land nei (J) (\{w\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
63	46 60 62	mpbir2and	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to w \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
64		eleq1w	$⊢ x = z \to (x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \leftrightarrow z \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))$
65		eleq1w	$⊢ x = w \to (x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \leftrightarrow w \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))$
66	64 65	moi	$⊢ ((z \in X \land w \in X) \land \exists^{*} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \land (z \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \land w \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))) \to z = w$
67	66	3com23	$⊢ ((z \in X \land w \in X) \land (z \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \land w \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))) \land \exists^{*} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))) \to z = w$
68	67	3expia	$⊢ ((z \in X \land w \in X) \land (z \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \land w \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))) \to (\exists^{*} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \to z = w)$
69	45 46 59 63 68	syl22anc	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to (\exists^{*} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))) \to z = w)$
70	69	necon3ad	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to (z \neq w \to \neg \exists^{*} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))$
71	44 70	mpd	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to \neg \exists^{*} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))$
72		oveq2	$⊢ f = X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to J fLim f = J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))$
73	72	eleq2d	$⊢ f = X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to (x \in (J fLim f) \leftrightarrow x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))$
74	73	mobidv	$⊢ f = X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to (\exists^{} x x \in (J fLim f) \leftrightarrow \exists^{} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))$
75	74	notbid	$⊢ f = X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to (\neg \exists^{} x x \in (J fLim f) \leftrightarrow \neg \exists^{} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})))))$
76	75	rspcev	$⊢ (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in Fil (X) \land \neg \exists^{} x x \in (J fLim (X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))))) \to \exists f \in Fil (X) \neg \exists^{} x x \in (J fLim f)$
77	43 71 76	syl2anc	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X)) \to \exists f \in Fil (X) \neg \exists^{*} x x \in (J fLim f)$
78	77	ex	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \in fBas (X) \to \exists f \in Fil (X) \neg \exists^{*} x x \in (J fLim f))$
79	41 78	sylbird	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to ((nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X \land nei (J) (\{z\}) \cup nei (J) (\{w\}) \neq \emptyset \land \neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))) \to \exists f \in Fil (X) \neg \exists^{*} x x \in (J fLim f))$
80	37 79	syld	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\neg \emptyset \in fi (nei (J) (\{z\}) \cup nei (J) (\{w\})) \to \exists f \in Fil (X) \neg \exists^{*} x x \in (J fLim f))$
81	24 80	sylbird	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\forall u \in nei (J) (\{z\}) \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset \to \exists f \in Fil (X) \neg \exists^{*} x x \in (J fLim f))$
82		df-ne	$⊢ u \cap v \neq \emptyset \leftrightarrow \neg u \cap v = \emptyset$
83	82	ralbii	$⊢ \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset \leftrightarrow \forall v \in nei (J) (\{w\}) \neg u \cap v = \emptyset$
84		ralnex	$⊢ \forall v \in nei (J) (\{w\}) \neg u \cap v = \emptyset \leftrightarrow \neg \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
85	83 84	bitri	$⊢ \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset \leftrightarrow \neg \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
86	85	ralbii	$⊢ \forall u \in nei (J) (\{z\}) \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset \leftrightarrow \forall u \in nei (J) (\{z\}) \neg \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
87		ralnex	$⊢ \forall u \in nei (J) (\{z\}) \neg \exists v \in nei (J) (\{w\}) u \cap v = \emptyset \leftrightarrow \neg \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
88	86 87	bitri	$⊢ \forall u \in nei (J) (\{z\}) \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset \leftrightarrow \neg \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
89		rexnal	$⊢ \exists f \in Fil (X) \neg \exists^{} x x \in (J fLim f) \leftrightarrow \neg \forall f \in Fil (X) \exists^{} x x \in (J fLim f)$
90	81 88 89	3imtr3g	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\neg \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset \to \neg \forall f \in Fil (X) \exists^{*} x x \in (J fLim f))$
91	90	con4d	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to (\forall f \in Fil (X) \exists^{*} x x \in (J fLim f) \to \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset)$
92	91	imp	$⊢ ((J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
93	92	an32s	$⊢ ((J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \land ((z \in X \land w \in X) \land z \neq w)) \to \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
94	93	expr	$⊢ ((J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \land (z \in X \land w \in X)) \to (z \neq w \to \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset)$
95	94	ralrimivva	$⊢ (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to \forall z \in X \forall w \in X (z \neq w \to \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset)$
96		simpl	$⊢ (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to J \in Top$
97	96 7	sylib	$⊢ (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to J \in TopOn (X)$
98		hausnei2	$⊢ J \in TopOn (X) \to (J \in Haus \leftrightarrow \forall z \in X \forall w \in X (z \neq w \to \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset))$
99	97 98	syl	$⊢ (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to (J \in Haus \leftrightarrow \forall z \in X \forall w \in X (z \neq w \to \exists u \in nei (J) (\{z\}) \exists v \in nei (J) (\{w\}) u \cap v = \emptyset))$
100	95 99	mpbird	$⊢ (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to J \in Haus$
101	5 100	impbii	$⊢ J \in Haus \leftrightarrow (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f))$

Metamath Proof Explorer

Theorem hausflim

Proof