This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem regr1

Description: A regular space is R_1, which means that any two topologically distinct points can be separated by neighborhoods. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	regr1	$⊢ J \in Reg \to KQ (J) \in Haus$

Proof

Step	Hyp	Ref	Expression
1		regtop	$⊢ J \in Reg \to J \in Top$
2		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
3	1 2	sylib	$⊢ J \in Reg \to J \in TopOn (⋃ J)$
4		eqid	$⊢ (x \in ⋃ J ⟼ \{y \in J \| x \in y\}) = (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
5	4	regr1lem2	$⊢ (J \in TopOn (⋃ J) \land J \in Reg) \to KQ (J) \in Haus$
6	3 5	mpancom	$⊢ J \in Reg \to KQ (J) \in Haus$