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 ( 𝐽 ∈ Reg → ( KQ ‘ 𝐽 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 regtop ( 𝐽 ∈ Reg → 𝐽 ∈ Top )
2 toptopon2 ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
3 1 2 sylib ( 𝐽 ∈ Reg → 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
4 eqid ( 𝑥 𝐽 ↦ { 𝑦𝐽𝑥𝑦 } ) = ( 𝑥 𝐽 ↦ { 𝑦𝐽𝑥𝑦 } )
5 4 regr1lem2 ( ( 𝐽 ∈ ( TopOn ‘ 𝐽 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ Haus )
6 3 5 mpancom ( 𝐽 ∈ Reg → ( KQ ‘ 𝐽 ) ∈ Haus )