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 e. Reg -> ( KQ ` J ) e. Haus )

Proof

Step	Hyp	Ref	Expression
1		regtop	|- ( J e. Reg -> J e. Top )
2		toptopon2	|- ( J e. Top <-> J e. ( TopOn ` U. J ) )
3	1 2	sylib	|- ( J e. Reg -> J e. ( TopOn ` U. J ) )
4		eqid	|- ( x e. U. J |-> { y e. J | x e. y } ) = ( x e. U. J |-> { y e. J | x e. y } )
5	4	regr1lem2	|- ( ( J e. ( TopOn ` U. J ) /\ J e. Reg ) -> ( KQ ` J ) e. Haus )
6	3 5	mpancom	|- ( J e. Reg -> ( KQ ` J ) e. Haus )