ordthaus

Description: The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015)

		Ref	Expression
	Assertion	ordthaus	$⊢ R \in TosetRel \to ordTop (R) \in Haus$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ dom R = dom R$
2	1	ordthauslem	$⊢ (R \in TosetRel \land x \in dom R \land y \in dom R) \to (x R y \to (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)))$
3	1	ordthauslem	$⊢ (R \in TosetRel \land y \in dom R \land x \in dom R) \to (y R x \to (y \neq x \to \exists n \in ordTop (R) \exists m \in ordTop (R) (y \in n \land x \in m \land n \cap m = \emptyset)))$
4		necom	$⊢ y \neq x \leftrightarrow x \neq y$
5		3ancoma	$⊢ (y \in n \land x \in m \land n \cap m = \emptyset) \leftrightarrow (x \in m \land y \in n \land n \cap m = \emptyset)$
6		incom	$⊢ n \cap m = m \cap n$
7	6	eqeq1i	$⊢ n \cap m = \emptyset \leftrightarrow m \cap n = \emptyset$
8	7	3anbi3i	$⊢ (x \in m \land y \in n \land n \cap m = \emptyset) \leftrightarrow (x \in m \land y \in n \land m \cap n = \emptyset)$
9	5 8	bitri	$⊢ (y \in n \land x \in m \land n \cap m = \emptyset) \leftrightarrow (x \in m \land y \in n \land m \cap n = \emptyset)$
10	9	2rexbii	$⊢ \exists n \in ordTop (R) \exists m \in ordTop (R) (y \in n \land x \in m \land n \cap m = \emptyset) \leftrightarrow \exists n \in ordTop (R) \exists m \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)$
11		rexcom	$⊢ \exists n \in ordTop (R) \exists m \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset) \leftrightarrow \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)$
12	10 11	bitri	$⊢ \exists n \in ordTop (R) \exists m \in ordTop (R) (y \in n \land x \in m \land n \cap m = \emptyset) \leftrightarrow \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)$
13	4 12	imbi12i	$⊢ (y \neq x \to \exists n \in ordTop (R) \exists m \in ordTop (R) (y \in n \land x \in m \land n \cap m = \emptyset)) \leftrightarrow (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset))$
14	3 13	syl6ib	$⊢ (R \in TosetRel \land y \in dom R \land x \in dom R) \to (y R x \to (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)))$
15	14	3com23	$⊢ (R \in TosetRel \land x \in dom R \land y \in dom R) \to (y R x \to (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)))$
16	1	tsrlin	$⊢ (R \in TosetRel \land x \in dom R \land y \in dom R) \to (x R y \lor y R x)$
17	2 15 16	mpjaod	$⊢ (R \in TosetRel \land x \in dom R \land y \in dom R) \to (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset))$
18	17	3expb	$⊢ (R \in TosetRel \land (x \in dom R \land y \in dom R)) \to (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset))$
19	18	ralrimivva	$⊢ R \in TosetRel \to \forall x \in dom R \forall y \in dom R (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset))$
20	1	ordttopon	$⊢ R \in TosetRel \to ordTop (R) \in TopOn (dom R)$
21		ishaus2	$⊢ ordTop (R) \in TopOn (dom R) \to (ordTop (R) \in Haus \leftrightarrow \forall x \in dom R \forall y \in dom R (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)))$
22	20 21	syl	$⊢ R \in TosetRel \to (ordTop (R) \in Haus \leftrightarrow \forall x \in dom R \forall y \in dom R (x \neq y \to \exists m \in ordTop (R) \exists n \in ordTop (R) (x \in m \land y \in n \land m \cap n = \emptyset)))$
23	19 22	mpbird	$⊢ R \in TosetRel \to ordTop (R) \in Haus$

Metamath Proof Explorer

Theorem ordthaus

Proof