ordtt1

Description: The order topology is T_1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Assertion	ordtt1	$⊢ R \in PosetRel \to ordTop (R) \in Fre$

Proof

Step	Hyp	Ref	Expression
1		ordttop	$⊢ R \in PosetRel \to ordTop (R) \in Top$
2		snssi	$⊢ x \in dom R \to \{x\} \subseteq dom R$
3	2	adantl	$⊢ (R \in PosetRel \land x \in dom R) \to \{x\} \subseteq dom R$
4		sseqin2	$⊢ \{x\} \subseteq dom R \leftrightarrow dom R \cap \{x\} = \{x\}$
5	3 4	sylib	$⊢ (R \in PosetRel \land x \in dom R) \to dom R \cap \{x\} = \{x\}$
6		velsn	$⊢ y \in \{x\} \leftrightarrow y = x$
7		eqid	$⊢ dom R = dom R$
8	7	psref	$⊢ (R \in PosetRel \land x \in dom R) \to x R x$
9	8	adantr	$⊢ ((R \in PosetRel \land x \in dom R) \land y \in dom R) \to x R x$
10	9 9	jca	$⊢ ((R \in PosetRel \land x \in dom R) \land y \in dom R) \to (x R x \land x R x)$
11		breq2	$⊢ y = x \to (x R y \leftrightarrow x R x)$
12		breq1	$⊢ y = x \to (y R x \leftrightarrow x R x)$
13	11 12	anbi12d	$⊢ y = x \to ((x R y \land y R x) \leftrightarrow (x R x \land x R x))$
14	10 13	syl5ibrcom	$⊢ ((R \in PosetRel \land x \in dom R) \land y \in dom R) \to (y = x \to (x R y \land y R x))$
15		psasym	$⊢ (R \in PosetRel \land x R y \land y R x) \to x = y$
16	15	equcomd	$⊢ (R \in PosetRel \land x R y \land y R x) \to y = x$
17	16	3expib	$⊢ R \in PosetRel \to ((x R y \land y R x) \to y = x)$
18	17	ad2antrr	$⊢ ((R \in PosetRel \land x \in dom R) \land y \in dom R) \to ((x R y \land y R x) \to y = x)$
19	14 18	impbid	$⊢ ((R \in PosetRel \land x \in dom R) \land y \in dom R) \to (y = x \leftrightarrow (x R y \land y R x))$
20	6 19	bitrid	$⊢ ((R \in PosetRel \land x \in dom R) \land y \in dom R) \to (y \in \{x\} \leftrightarrow (x R y \land y R x))$
21	20	rabbi2dva	$⊢ (R \in PosetRel \land x \in dom R) \to dom R \cap \{x\} = \{y \in dom R \| (x R y \land y R x)\}$
22	5 21	eqtr3d	$⊢ (R \in PosetRel \land x \in dom R) \to \{x\} = \{y \in dom R \| (x R y \land y R x)\}$
23	7	ordtcld3	$⊢ (R \in PosetRel \land x \in dom R \land x \in dom R) \to \{y \in dom R \| (x R y \land y R x)\} \in Clsd (ordTop (R))$
24	23	3anidm23	$⊢ (R \in PosetRel \land x \in dom R) \to \{y \in dom R \| (x R y \land y R x)\} \in Clsd (ordTop (R))$
25	22 24	eqeltrd	$⊢ (R \in PosetRel \land x \in dom R) \to \{x\} \in Clsd (ordTop (R))$
26	25	ralrimiva	$⊢ R \in PosetRel \to \forall x \in dom R \{x\} \in Clsd (ordTop (R))$
27	7	ordttopon	$⊢ R \in PosetRel \to ordTop (R) \in TopOn (dom R)$
28		toponuni	$⊢ ordTop (R) \in TopOn (dom R) \to dom R = ⋃ ordTop (R)$
29	27 28	syl	$⊢ R \in PosetRel \to dom R = ⋃ ordTop (R)$
30	26 29	raleqtrdv	$⊢ R \in PosetRel \to \forall x \in ⋃ ordTop (R) \{x\} \in Clsd (ordTop (R))$
31		eqid	$⊢ ⋃ ordTop (R) = ⋃ ordTop (R)$
32	31	ist1	$⊢ ordTop (R) \in Fre \leftrightarrow (ordTop (R) \in Top \land \forall x \in ⋃ ordTop (R) \{x\} \in Clsd (ordTop (R)))$
33	1 30 32	sylanbrc	$⊢ R \in PosetRel \to ordTop (R) \in Fre$

Metamath Proof Explorer

Theorem ordtt1

Proof