haust1

Description: A Hausdorff space is a T_1 space. (Contributed by FL, 11-Jun-2007) (Proof shortened by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Assertion	haust1	$⊢ J \in Haus \to J \in Fre$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	hausnei	$⊢ (J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \to \exists z \in J \exists w \in J (x \in z \land y \in w \land z \cap w = \emptyset)$
3		simprr1	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to x \in z$
4		noel	$⊢ \neg y \in \emptyset$
5		simprr3	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to z \cap w = \emptyset$
6	5	eleq2d	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to (y \in (z \cap w) \leftrightarrow y \in \emptyset)$
7	4 6	mtbiri	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to \neg y \in (z \cap w)$
8		simprr2	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to y \in w$
9		elin	$⊢ y \in (z \cap w) \leftrightarrow (y \in z \land y \in w)$
10	9	simplbi2com	$⊢ y \in w \to (y \in z \to y \in (z \cap w))$
11	8 10	syl	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to (y \in z \to y \in (z \cap w))$
12	7 11	mtod	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to \neg y \in z$
13	3 12	jca	$⊢ (((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \land (w \in J \land (x \in z \land y \in w \land z \cap w = \emptyset))) \to (x \in z \land \neg y \in z)$
14	13	rexlimdvaa	$⊢ ((J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \land z \in J) \to (\exists w \in J (x \in z \land y \in w \land z \cap w = \emptyset) \to (x \in z \land \neg y \in z))$
15	14	reximdva	$⊢ (J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \to (\exists z \in J \exists w \in J (x \in z \land y \in w \land z \cap w = \emptyset) \to \exists z \in J (x \in z \land \neg y \in z))$
16	2 15	mpd	$⊢ (J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \to \exists z \in J (x \in z \land \neg y \in z)$
17		rexanali	$⊢ \exists z \in J (x \in z \land \neg y \in z) \leftrightarrow \neg \forall z \in J (x \in z \to y \in z)$
18	16 17	sylib	$⊢ (J \in Haus \land (x \in ⋃ J \land y \in ⋃ J \land x \neq y)) \to \neg \forall z \in J (x \in z \to y \in z)$
19	18	3exp2	$⊢ J \in Haus \to (x \in ⋃ J \to (y \in ⋃ J \to (x \neq y \to \neg \forall z \in J (x \in z \to y \in z))))$
20	19	imp32	$⊢ (J \in Haus \land (x \in ⋃ J \land y \in ⋃ J)) \to (x \neq y \to \neg \forall z \in J (x \in z \to y \in z))$
21	20	necon4ad	$⊢ (J \in Haus \land (x \in ⋃ J \land y \in ⋃ J)) \to (\forall z \in J (x \in z \to y \in z) \to x = y)$
22	21	ralrimivva	$⊢ J \in Haus \to \forall x \in ⋃ J \forall y \in ⋃ J (\forall z \in J (x \in z \to y \in z) \to x = y)$
23		haustop	$⊢ J \in Haus \to J \in Top$
24		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
25	23 24	sylib	$⊢ J \in Haus \to J \in TopOn (⋃ J)$
26		ist1-2	$⊢ J \in TopOn (⋃ J) \to (J \in Fre \leftrightarrow \forall x \in ⋃ J \forall y \in ⋃ J (\forall z \in J (x \in z \to y \in z) \to x = y))$
27	25 26	syl	$⊢ J \in Haus \to (J \in Fre \leftrightarrow \forall x \in ⋃ J \forall y \in ⋃ J (\forall z \in J (x \in z \to y \in z) \to x = y))$
28	22 27	mpbird	$⊢ J \in Haus \to J \in Fre$

Metamath Proof Explorer

Theorem haust1

Proof