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 )