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	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
7	6	birani	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to J \in TopOn (X)$
8		simprll	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to z \in X$
9	8	snssd	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{z\} \subseteq X$
10	8	snn0d	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{z\} \neq \emptyset$
11		neifil	$⊢ (J \in TopOn (X) \land \{z\} \subseteq X \land \{z\} \neq \emptyset) \to nei (J) (\{z\}) \in Fil (X)$
12	7 9 10 11	syl3anc	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \in Fil (X)$
13		filfbas	$⊢ nei (J) (\{z\}) \in Fil (X) \to nei (J) (\{z\}) \in fBas (X)$
14	12 13	syl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \in fBas (X)$
15		simprlr	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to w \in X$
16	15	snssd	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{w\} \subseteq X$
17	15	snn0d	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to \{w\} \neq \emptyset$
18		neifil	$⊢ (J \in TopOn (X) \land \{w\} \subseteq X \land \{w\} \neq \emptyset) \to nei (J) (\{w\}) \in Fil (X)$
19	7 16 17 18	syl3anc	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{w\}) \in Fil (X)$
20		filfbas	$⊢ nei (J) (\{w\}) \in Fil (X) \to nei (J) (\{w\}) \in fBas (X)$
21	19 20	syl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{w\}) \in fBas (X)$
22		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)$
23	14 21 22	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)$
24	1	neisspw	$⊢ J \in Top \to nei (J) (\{z\}) \subseteq 𝒫 X$
25	1	neisspw	$⊢ J \in Top \to nei (J) (\{w\}) \subseteq 𝒫 X$
26	24 25	unssd	$⊢ J \in Top \to nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq 𝒫 X$
27	26	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$
28	27	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)$
29		ssun1	$⊢ nei (J) (\{z\}) \subseteq nei (J) (\{z\}) \cup nei (J) (\{w\})$
30		filn0	$⊢ nei (J) (\{z\}) \in Fil (X) \to nei (J) (\{z\}) \neq \emptyset$
31	12 30	syl	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to nei (J) (\{z\}) \neq \emptyset$
32		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$
33	29 31 32	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$
34	33	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)$
35		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\})))$
36	28 34 35	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\}))))$
37	1	topopn	$⊢ J \in Top \to X \in J$
38	37	adantr	$⊢ (J \in Top \land ((z \in X \land w \in X) \land z \neq w)) \to X \in J$
39		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\}))))$
40	38 39	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\}))))$
41		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)$
42	41	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)$
43		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$
44	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 z \in X$
45	15	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$
46		fvex	$⊢ nei (J) (\{z\}) \in V$
47		fvex	$⊢ nei (J) (\{w\}) \in V$
48	46 47	unex	$⊢ nei (J) (\{z\}) \cup nei (J) (\{w\}) \in V$
49		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\}))$
50	48 49	ax-mp	$⊢ nei (J) (\{z\}) \cup nei (J) (\{w\}) \subseteq fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
51		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\}))$
52	51	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\}))$
53	50 52	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\}))$
54	29 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\}) \subseteq X filGen fi (nei (J) (\{z\}) \cup nei (J) (\{w\}))$
55	7	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)$
56		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\}))))$
57	55 42 56	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\}))))$
58	44 54 57	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\}))))$
59	53	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\}))$
60		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\}))))$
61	55 42 60	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\}))))$
62	45 59 61	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\}))))$
63		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\})))))$
64		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\})))))$
65	63 64	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$
66	65	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$
67	66	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)$
68	44 45 58 62 67	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)$
69	68	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\})))))$
70	43 69	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\}))))$
71		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\})))$
72	71	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\})))))$
73	72	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\})))))$
74	73	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\})))))$
75	74	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)$
76	42 70 75	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)$
77	76	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))$
78	40 77	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))$
79	36 78	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))$
80	23 79	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))$
81		df-ne	$⊢ u \cap v \neq \emptyset \leftrightarrow \neg u \cap v = \emptyset$
82	81	ralbii	$⊢ \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset \leftrightarrow \forall v \in nei (J) (\{w\}) \neg u \cap v = \emptyset$
83		ralnex	$⊢ \forall v \in nei (J) (\{w\}) \neg u \cap v = \emptyset \leftrightarrow \neg \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
84	82 83	bitri	$⊢ \forall v \in nei (J) (\{w\}) u \cap v \neq \emptyset \leftrightarrow \neg \exists v \in nei (J) (\{w\}) u \cap v = \emptyset$
85	84	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$
86		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$
87	85 86	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$
88		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)$
89	80 87 88	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))$
90	89	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)$
91	90	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$
92	91	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$
93	92	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)$
94	93	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)$
95	6	birani	$⊢ (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to J \in TopOn (X)$
96		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))$
97	95 96	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))$
98	94 97	mpbird	$⊢ (J \in Top \land \forall f \in Fil (X) \exists^{*} x x \in (J fLim f)) \to J \in Haus$
99	5 98	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