dishaus

Description: A discrete topology is Hausdorff. Morris, Topology without tears, p.72, ex. 13. (Contributed by FL, 24-Jun-2007) (Proof shortened by Mario Carneiro, 8-Apr-2015)

		Ref	Expression
	Assertion	dishaus	$⊢ A \in V \to 𝒫 A \in Haus$

Proof

Step	Hyp	Ref	Expression
1		distop	$⊢ A \in V \to 𝒫 A \in Top$
2		simplrl	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to x \in A$
3	2	snssd	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to \{x\} \subseteq A$
4		snex	$⊢ \{x\} \in V$
5	4	elpw	$⊢ \{x\} \in 𝒫 A \leftrightarrow \{x\} \subseteq A$
6	3 5	sylibr	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to \{x\} \in 𝒫 A$
7		simplrr	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to y \in A$
8	7	snssd	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to \{y\} \subseteq A$
9		snex	$⊢ \{y\} \in V$
10	9	elpw	$⊢ \{y\} \in 𝒫 A \leftrightarrow \{y\} \subseteq A$
11	8 10	sylibr	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to \{y\} \in 𝒫 A$
12		vsnid	$⊢ x \in \{x\}$
13	12	a1i	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to x \in \{x\}$
14		vsnid	$⊢ y \in \{y\}$
15	14	a1i	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to y \in \{y\}$
16		disjsn2	$⊢ x \neq y \to \{x\} \cap \{y\} = \emptyset$
17	16	adantl	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to \{x\} \cap \{y\} = \emptyset$
18		eleq2	$⊢ u = \{x\} \to (x \in u \leftrightarrow x \in \{x\})$
19		ineq1	$⊢ u = \{x\} \to u \cap v = \{x\} \cap v$
20	19	eqeq1d	$⊢ u = \{x\} \to (u \cap v = \emptyset \leftrightarrow \{x\} \cap v = \emptyset)$
21	18 20	3anbi13d	$⊢ u = \{x\} \to ((x \in u \land y \in v \land u \cap v = \emptyset) \leftrightarrow (x \in \{x\} \land y \in v \land \{x\} \cap v = \emptyset))$
22		eleq2	$⊢ v = \{y\} \to (y \in v \leftrightarrow y \in \{y\})$
23		ineq2	$⊢ v = \{y\} \to \{x\} \cap v = \{x\} \cap \{y\}$
24	23	eqeq1d	$⊢ v = \{y\} \to (\{x\} \cap v = \emptyset \leftrightarrow \{x\} \cap \{y\} = \emptyset)$
25	22 24	3anbi23d	$⊢ v = \{y\} \to ((x \in \{x\} \land y \in v \land \{x\} \cap v = \emptyset) \leftrightarrow (x \in \{x\} \land y \in \{y\} \land \{x\} \cap \{y\} = \emptyset))$
26	21 25	rspc2ev	$⊢ (\{x\} \in 𝒫 A \land \{y\} \in 𝒫 A \land (x \in \{x\} \land y \in \{y\} \land \{x\} \cap \{y\} = \emptyset)) \to \exists u \in 𝒫 A \exists v \in 𝒫 A (x \in u \land y \in v \land u \cap v = \emptyset)$
27	6 11 13 15 17 26	syl113anc	$⊢ ((A \in V \land (x \in A \land y \in A)) \land x \neq y) \to \exists u \in 𝒫 A \exists v \in 𝒫 A (x \in u \land y \in v \land u \cap v = \emptyset)$
28	27	ex	$⊢ (A \in V \land (x \in A \land y \in A)) \to (x \neq y \to \exists u \in 𝒫 A \exists v \in 𝒫 A (x \in u \land y \in v \land u \cap v = \emptyset))$
29	28	ralrimivva	$⊢ A \in V \to \forall x \in A \forall y \in A (x \neq y \to \exists u \in 𝒫 A \exists v \in 𝒫 A (x \in u \land y \in v \land u \cap v = \emptyset))$
30		unipw	$⊢ ⋃ 𝒫 A = A$
31	30	eqcomi	$⊢ A = ⋃ 𝒫 A$
32	31	ishaus	$⊢ 𝒫 A \in Haus \leftrightarrow (𝒫 A \in Top \land \forall x \in A \forall y \in A (x \neq y \to \exists u \in 𝒫 A \exists v \in 𝒫 A (x \in u \land y \in v \land u \cap v = \emptyset)))$
33	1 29 32	sylanbrc	$⊢ A \in V \to 𝒫 A \in Haus$

Metamath Proof Explorer

Theorem dishaus

Proof