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 JRegKQJHaus

Proof

Step Hyp Ref Expression
1 regtop JRegJTop
2 toptopon2 JTopJTopOnJ
3 1 2 sylib JRegJTopOnJ
4 eqid xJyJ|xy=xJyJ|xy
5 4 regr1lem2 JTopOnJJRegKQJHaus
6 3 5 mpancom JRegKQJHaus