hausnei2

Description: The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009)

		Ref	Expression
	Assertion	hausnei2	$⊢ J \in TopOn (X) \to (J \in Haus \leftrightarrow \forall x \in X \forall y \in X (x \neq y \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		ishaus2	$⊢ J \in TopOn (X) \to (J \in Haus \leftrightarrow \forall x \in X \forall y \in X (x \neq y \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)))$
2		topontop	$⊢ J \in TopOn (X) \to J \in Top$
3		simp1	$⊢ (J \in Top \land m \in J \land n \in J) \to J \in Top$
4		simp2	$⊢ (J \in Top \land m \in J \land n \in J) \to m \in J$
5		simp1	$⊢ (x \in m \land y \in n \land m \cap n = \emptyset) \to x \in m$
6		opnneip	$⊢ (J \in Top \land m \in J \land x \in m) \to m \in nei (J) (\{x\})$
7	3 4 5 6	syl2an3an	$⊢ ((J \in Top \land m \in J \land n \in J) \land (x \in m \land y \in n \land m \cap n = \emptyset)) \to m \in nei (J) (\{x\})$
8		simp3	$⊢ (J \in Top \land m \in J \land n \in J) \to n \in J$
9		simp2	$⊢ (x \in m \land y \in n \land m \cap n = \emptyset) \to y \in n$
10		opnneip	$⊢ (J \in Top \land n \in J \land y \in n) \to n \in nei (J) (\{y\})$
11	3 8 9 10	syl2an3an	$⊢ ((J \in Top \land m \in J \land n \in J) \land (x \in m \land y \in n \land m \cap n = \emptyset)) \to n \in nei (J) (\{y\})$
12		simpr3	$⊢ ((J \in Top \land m \in J \land n \in J) \land (x \in m \land y \in n \land m \cap n = \emptyset)) \to m \cap n = \emptyset$
13		ineq1	$⊢ u = m \to u \cap v = m \cap v$
14	13	eqeq1d	$⊢ u = m \to (u \cap v = \emptyset \leftrightarrow m \cap v = \emptyset)$
15		ineq2	$⊢ v = n \to m \cap v = m \cap n$
16	15	eqeq1d	$⊢ v = n \to (m \cap v = \emptyset \leftrightarrow m \cap n = \emptyset)$
17	14 16	rspc2ev	$⊢ (m \in nei (J) (\{x\}) \land n \in nei (J) (\{y\}) \land m \cap n = \emptyset) \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset$
18	7 11 12 17	syl3anc	$⊢ ((J \in Top \land m \in J \land n \in J) \land (x \in m \land y \in n \land m \cap n = \emptyset)) \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset$
19	18	ex	$⊢ (J \in Top \land m \in J \land n \in J) \to ((x \in m \land y \in n \land m \cap n = \emptyset) \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset)$
20	19	3expib	$⊢ J \in Top \to ((m \in J \land n \in J) \to ((x \in m \land y \in n \land m \cap n = \emptyset) \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset))$
21	20	rexlimdvv	$⊢ J \in Top \to (\exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset) \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset)$
22		neii2	$⊢ (J \in Top \land u \in nei (J) (\{x\})) \to \exists m \in J (\{x\} \subseteq m \land m \subseteq u)$
23	22	ex	$⊢ J \in Top \to (u \in nei (J) (\{x\}) \to \exists m \in J (\{x\} \subseteq m \land m \subseteq u))$
24		neii2	$⊢ (J \in Top \land v \in nei (J) (\{y\})) \to \exists n \in J (\{y\} \subseteq n \land n \subseteq v)$
25	24	ex	$⊢ J \in Top \to (v \in nei (J) (\{y\}) \to \exists n \in J (\{y\} \subseteq n \land n \subseteq v))$
26		vex	$⊢ x \in V$
27	26	snss	$⊢ x \in m \leftrightarrow \{x\} \subseteq m$
28	27	anbi1i	$⊢ (x \in m \land m \subseteq u) \leftrightarrow (\{x\} \subseteq m \land m \subseteq u)$
29		vex	$⊢ y \in V$
30	29	snss	$⊢ y \in n \leftrightarrow \{y\} \subseteq n$
31	30	anbi1i	$⊢ (y \in n \land n \subseteq v) \leftrightarrow (\{y\} \subseteq n \land n \subseteq v)$
32		simp1l	$⊢ ((x \in m \land m \subseteq u) \land (y \in n \land n \subseteq v) \land u \cap v = \emptyset) \to x \in m$
33		simp2l	$⊢ ((x \in m \land m \subseteq u) \land (y \in n \land n \subseteq v) \land u \cap v = \emptyset) \to y \in n$
34		ss2in	$⊢ (m \subseteq u \land n \subseteq v) \to m \cap n \subseteq u \cap v$
35		ssn0	$⊢ (m \cap n \subseteq u \cap v \land m \cap n \neq \emptyset) \to u \cap v \neq \emptyset$
36	35	ex	$⊢ m \cap n \subseteq u \cap v \to (m \cap n \neq \emptyset \to u \cap v \neq \emptyset)$
37	36	necon4d	$⊢ m \cap n \subseteq u \cap v \to (u \cap v = \emptyset \to m \cap n = \emptyset)$
38	34 37	syl	$⊢ (m \subseteq u \land n \subseteq v) \to (u \cap v = \emptyset \to m \cap n = \emptyset)$
39	38	ad2ant2l	$⊢ ((x \in m \land m \subseteq u) \land (y \in n \land n \subseteq v)) \to (u \cap v = \emptyset \to m \cap n = \emptyset)$
40	39	3impia	$⊢ ((x \in m \land m \subseteq u) \land (y \in n \land n \subseteq v) \land u \cap v = \emptyset) \to m \cap n = \emptyset$
41	32 33 40	3jca	$⊢ ((x \in m \land m \subseteq u) \land (y \in n \land n \subseteq v) \land u \cap v = \emptyset) \to (x \in m \land y \in n \land m \cap n = \emptyset)$
42	41	3exp	$⊢ (x \in m \land m \subseteq u) \to ((y \in n \land n \subseteq v) \to (u \cap v = \emptyset \to (x \in m \land y \in n \land m \cap n = \emptyset)))$
43	31 42	syl5bir	$⊢ (x \in m \land m \subseteq u) \to ((\{y\} \subseteq n \land n \subseteq v) \to (u \cap v = \emptyset \to (x \in m \land y \in n \land m \cap n = \emptyset)))$
44	43	com3r	$⊢ u \cap v = \emptyset \to ((x \in m \land m \subseteq u) \to ((\{y\} \subseteq n \land n \subseteq v) \to (x \in m \land y \in n \land m \cap n = \emptyset)))$
45	44	imp	$⊢ (u \cap v = \emptyset \land (x \in m \land m \subseteq u)) \to ((\{y\} \subseteq n \land n \subseteq v) \to (x \in m \land y \in n \land m \cap n = \emptyset))$
46	45	3adant1	$⊢ (J \in Top \land u \cap v = \emptyset \land (x \in m \land m \subseteq u)) \to ((\{y\} \subseteq n \land n \subseteq v) \to (x \in m \land y \in n \land m \cap n = \emptyset))$
47	46	reximdv	$⊢ (J \in Top \land u \cap v = \emptyset \land (x \in m \land m \subseteq u)) \to (\exists n \in J (\{y\} \subseteq n \land n \subseteq v) \to \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
48	47	3exp	$⊢ J \in Top \to (u \cap v = \emptyset \to ((x \in m \land m \subseteq u) \to (\exists n \in J (\{y\} \subseteq n \land n \subseteq v) \to \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))))$
49	48	com34	$⊢ J \in Top \to (u \cap v = \emptyset \to (\exists n \in J (\{y\} \subseteq n \land n \subseteq v) \to ((x \in m \land m \subseteq u) \to \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))))$
50	49	3imp	$⊢ (J \in Top \land u \cap v = \emptyset \land \exists n \in J (\{y\} \subseteq n \land n \subseteq v)) \to ((x \in m \land m \subseteq u) \to \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
51	28 50	syl5bir	$⊢ (J \in Top \land u \cap v = \emptyset \land \exists n \in J (\{y\} \subseteq n \land n \subseteq v)) \to ((\{x\} \subseteq m \land m \subseteq u) \to \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
52	51	reximdv	$⊢ (J \in Top \land u \cap v = \emptyset \land \exists n \in J (\{y\} \subseteq n \land n \subseteq v)) \to (\exists m \in J (\{x\} \subseteq m \land m \subseteq u) \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
53	52	3exp	$⊢ J \in Top \to (u \cap v = \emptyset \to (\exists n \in J (\{y\} \subseteq n \land n \subseteq v) \to (\exists m \in J (\{x\} \subseteq m \land m \subseteq u) \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))))$
54	53	com24	$⊢ J \in Top \to (\exists m \in J (\{x\} \subseteq m \land m \subseteq u) \to (\exists n \in J (\{y\} \subseteq n \land n \subseteq v) \to (u \cap v = \emptyset \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))))$
55	54	impd	$⊢ J \in Top \to ((\exists m \in J (\{x\} \subseteq m \land m \subseteq u) \land \exists n \in J (\{y\} \subseteq n \land n \subseteq v)) \to (u \cap v = \emptyset \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)))$
56	23 25 55	syl2and	$⊢ J \in Top \to ((u \in nei (J) (\{x\}) \land v \in nei (J) (\{y\})) \to (u \cap v = \emptyset \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)))$
57	56	rexlimdvv	$⊢ J \in Top \to (\exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
58	21 57	impbid	$⊢ J \in Top \to (\exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset) \leftrightarrow \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset)$
59	58	imbi2d	$⊢ J \in Top \to ((x \neq y \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)) \leftrightarrow (x \neq y \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset))$
60	59	2ralbidv	$⊢ J \in Top \to (\forall x \in X \forall y \in X (x \neq y \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)) \leftrightarrow \forall x \in X \forall y \in X (x \neq y \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset))$
61	2 60	syl	$⊢ J \in TopOn (X) \to (\forall x \in X \forall y \in X (x \neq y \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)) \leftrightarrow \forall x \in X \forall y \in X (x \neq y \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset))$
62	1 61	bitrd	$⊢ J \in TopOn (X) \to (J \in Haus \leftrightarrow \forall x \in X \forall y \in X (x \neq y \to \exists u \in nei (J) (\{x\}) \exists v \in nei (J) (\{y\}) u \cap v = \emptyset))$

Metamath Proof Explorer

Theorem hausnei2

Proof